[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.
On 12/29/2021 3:24 PM, jack malkovick wrote:
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.--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/107a2e4e-1136-4b52-8234-02f5b0b85a10n%40googlegroups.com.