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

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

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


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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ba819ea0-ec73-4ccc-8898-96dce5543999n%40googlegroups.com.