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