TypeOK for primed variables

[Mathew Kuthur James]

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+?

[Andrew Helwer]

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

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/448f17c6-f775-4910-b6ed-bfd0b1630cebn%40googlegroups.com.

[Stephan Merz]

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...@gmail.com> wrote:



To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUWZ1Dvxk5xtEzXK95kjPcHqgubO5F6P%3DO5ODG1f97hBBg%40mail.gmail.com.