Re: [tlaplus] Semantic of TLC constraints

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

On 17 Mar 2022, at 13:04, 'Ognjen Maric' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

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

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

--
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/EE707C12-CE50-4870-BAE7-8E3A82310648%40gmail.com.