Re: [tlaplus] Do Constraints Confuse Properties? Sources

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Hello Siegfried,

for the answer to your question please read section 14.3.5 of Specifying Systems.

In short, combining state constraints and temporal properties is tricky. In particular, adding the constraint to the config file is not equivalent to conjoining MyCons’ to Next, as you perhaps would have expected.

Hope this helps,

Stephan

On 2 Oct 2026, at 16:56, 'sbublitz24' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

Maybe the sources should be given directly here ...

---- MODULE ValidateProp ----

EXTENDS Integers

VARIABLE n

Init ≜ n = 9

Next ≜ n > 0 ∧ n' = n - 1

Spec ≜ Init ∧ □ [Next]_n ∧ WF_n(Next)

MyProp ≜ ◇ (n = 3)

MyCons ≜ n ≠ 6

====

\* ValidateProp.cfg

CHECK_DEADLOCK FALSE

SPECIFICATION Spec

PROPERTY MyProp

CONSTRAINT MyCons

--
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 visit https://groups.google.com/d/msgid/tlaplus/OBS9XOqd8i5SBK1g8y8zUAFnrsue9XpwihUDKJvE4LbBiycsrvx_VvWBpp1THttbE_GlR8w9R09SEgWr847paQ9PL9Pucu33y7bH23QchfI%3D%40pm.me.

--
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 visit https://groups.google.com/d/msgid/tlaplus/B0E3BDB4-7904-4352-B269-294C7F28C585%40gmail.com.