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

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

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.