Semantic of TLC constraints

[Ognjen Maric]

Hi,

Reading "Specifying Systems", specifying a "CONSTRAINT c" adds an "always c" conjunct to the spec. However, the following TLA model and TLC config yield an error while model checking:

---- MODULE Constraint ----
EXTENDS TLC, Naturals

VARIABLE i
MAX_I == 2

Init == i = 1
Next == i' = i + 1

Constraint == i <= MAX_I
Invariant == Constraint
====

INIT Init
NEXT Next

CONSTRAINT
    Constraint

INVARIANT
    Invariant

However, changing the invariant to "i <= MAX_I + 1" makes TLC happy. Are the semantics of CONSTRAINT c then to add an "always previously c" conjunct to the spec, rather than "always c"? Is this intentional?

FWIW I used the latest GH release:
TLC2 Version 2.17 of 02 February 2022 (rev: 3c7caa5)

Thanks,
Ognjen

[Stephan Merz]

Hi Ognjen,

the Toolbox help says the following about state constraints:

When computing the set of reachable states, TLC will not explore successor states of any state it finds that does not satisfy the state constraint.

TLC will still evaluate the invariant on every state that it finds, even if that state does not satisfy the state constraint.

Cheers,

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/efdcafa4-7ff7-464f-9b13-5e3c2f93e0e5n%40googlegroups.com.

[Ognjen Maric]

Hi Stephan,

thanks, that's in line with what I observed then, and I can work with it for my use case (limiting the number of messages sent in a model).

I also now realize that my characterization with "always previously" doesn't really make sense, given stuttering.