[tlaplus] Semantic of TLC constraints

["'Ognjen Maric' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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.