Checking Invariants vs Properties

[jack malkovick]

Hello,

I'm playing around with the TLA Toolbox and I have a spec that I'm debugging.

Let's say I have a behavior that for each state var1 temporal variable is incremented by 1.

In order to see some traces, I'm forcing an making an Invariant (in Model / What to check?) like this to fail

var1 = 3 => FALSE

All is ok, it fails when a behavior that has a state where var1 is 3 and I can see the behavior.

Now, I expected to see the same thing happening when I've added the following formula as a Property 

[][var1 = 3 => FALSE]_vars

Now I run TLC and I get no error.

The strangest thing is, if I set in the above temporal formula var1 = 2, the value of a previous state in the behavior of interest, the Property fails as expected. It seems that [] (always), does not check the last state of the behavior...

I'm sure I'm wrong, but it drives me crazy.  

[Hillel Wayne]

[][var1 = 3 => FALSE]_vars is equivalent to [](var1 = 3 => FALSE \/ UNCHANGED vars). So if we're in the "last state" vars isn't changing, and the action property is trivially satisfied. If you put [](var1 = 3 => FALSE) as the property, it'd fail as expected.

You should be using action properties for checking actions. For example, you could write [](var1 = 2 /\ var1' = 3 => FALSE)_vars, which you can't write as an invariant.

H

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/107a2e4e-1136-4b52-8234-02f5b0b85a10n%40googlegroups.com.

[jack malkovick]

Ah... makes perfect sense! Thank you