[tlaplus] Do Constraints Confuse Properties? Sources

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

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.