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

49 views
Skip to first unread message

Andrew Helwer

unread,
Feb 21, 2021, 11:21:41 AM2/21/21
to tlaplus
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?

Stephan Merz

unread,
Feb 21, 2021, 11:34:27 AM2/21/21
to tla...@googlegroups.com
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

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

Andrew Helwer

unread,
Feb 21, 2021, 12:21:29 PM2/21/21
to tlaplus
Ah yes that's right, because of stuttering steps. Of course! Thank you Stephan.
Reply all
Reply to author
Forward
0 new messages