AW: Re: [tlaplus] Do Constraints Confuse Properties? Sources

["'sbublitz24' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

Hello Stephan,

thank you very much, this is indeed helpful.

TLC gives a warning when combining liveness with symmetry of model values.

Does it make sense to display a warning when combining liveness with constraints?

Best,

Siegfried

Stephan Merz <stephan.merz@xxxxxxxxx> schrieb am Montag, 5. Oktober 2026 um 08:43:

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.

-- 
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/NOSYAcxxv2F1B3EtQ43yqHYa-c9Ryc7gY80qoChTA7OQqU_YOVO9WKhXLx9BPR2DaNbgTB8UKXvM71YXdjamf-GUOsyl6mmJfUihq3NvCFQ%3D%40pm.me.