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

Re: [tlaplus] How do I get TLC to check invariants with primed variables (action predicates)?



Ah yes that's right, because of stuttering steps. Of course! Thank you Stephan.

On Sunday, February 21, 2021 at 11:34:27 AM UTC-5 Stephan Merz wrote:
Hi Andrew,

TLC can check the temporal property [][x' > x]_x. Note that [](x' > x) is not a TLA formula, and if it were, it wouldn't hold of your specification.

Stephan

On 21 Feb 2021, at 17:21, Andrew Helwer <andrew...@xxxxxxxxx> wrote:

Suppose we have a simple spec where a variable x is repeatedly incremented, and I want to model-check the statement that x increases monotonically:

---------------------------- MODULE Error -------------------------------

EXTENDS Naturals

VARIABLES x

TypeInvariant == x \in Nat

Init == x = 0

Next == x' = x + 1

Monotonic == x' > x

Spec ==
    /\ Init
    /\ [][Next]_<<x>>

=============================================================================



When I run this spec in TLC with Monotonic as an invariant, TLC spits out the following error:

The invariant Monotonic is not a state predicate (one with no primes or temporal operators).
Note that a bug can cause TLC to incorrectly report this error.
If you believe your TLA+ or PlusCal specification to be correct,
please check if this bug described in LevelNode.java starting at line 590ff affects you.


Does TLC support checking statements like Monotonic? If not, is there a workaround? Is Monotonic what's called an inductive invariant, or is that something else?


--
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/ba819ea0-ec73-4ccc-8898-96dce5543999n%40googlegroups.com.

--
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/71385b64-b1eb-4a46-b651-383bbeafd506n%40googlegroups.com.