[tlaplus] Checking Invariants vs Properties

[jack malkovick <sillymouse333@xxxxxxxxx>]

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.  

-- 
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.