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

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.