Adding to Andrew’s answer, TLC expects the first occurrence of a primed variable v’ in an action to be of the form
v’ = exp or v’ \in exp
where exp only contains primed variables that have been introduced earlier. For this reason you cannot just write t’ * t’ = 4 in your action but have to restrict its value by a constraint such as t’ \in -10 .. 10. Your TypeOK predicate serves this purpose.
Stephan On 16 Jan 2026, at 23:49, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
Are you just trying to restrict the state space to the range where t is in 1 .. 100? If so, you can use state constraints, which are defined in the model file. You can see an example here.
TypeOK is not a reserved word, but usually people use it as an invariant rather than incorporating it into their next-state relation. If you use it as an invariant then the model-checker will check that every state generated by Next satisfies TypeOK, then produce an error trace if it finds a state which does not.
In general if you want to use primed variables in an invariant, it needs to be boxed into an action-level formula like [][TypeOK_unprimed /\ TypeOK_primed]_<<t>>. This is to ensure something called stuttering insensitivity. Priming is also quite powerful in that it affects all unprimed variables within a definition, so you can rewrite the property as [][TypeOK_unprimed /\ TypeOK_unprimed']_<<t>>.
Andrew Hi,
I tried running a simple model in TLA+:
---- MODULE m ---- EXTENDS Integers, FiniteSets VARIABLES t TypeOK_unprimed == t \in 1..100 TypeOK_primed == t' \in 1..100 TypeOK == TypeOK_unprimed /\ TypeOK_primed _Init == TypeOK_unprimed /\ t \in {0,1} _Next == TypeOK /\ t' * t' = 4 ====
When I used TypeOK only using primed variables, TLC produced an error. To get the model to work, I had to use TypeOK in the unprimed form for Init, and both forms of TypeOK for Next. I thought that the convention was to always write TypeOK only for unprimed variables, and use it as an invariant. I intend 1..100 to be a constraint on both t and t'. My questions are:
1) Is there a better way to write this spec?
2) Is the name "TypeOK" meant to be used for this sort of formula, in idiomatic TLA+?
--
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/448f17c6-f775-4910-b6ed-bfd0b1630cebn%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 visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUWZ1Dvxk5xtEzXK95kjPcHqgubO5F6P%3DO5ODG1f97hBBg%40mail.gmail.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/3DB6E75F-72FC-4015-A398-6BD32F509F90%40gmail.com.
|