[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Checking Invariants vs Properties


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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/107a2e4e-1136-4b52-8234-02f5b0b85a10n%40googlegroups.com.