Re: [tlaplus] TypeOK for primed variables

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

On Fri, Jan 16, 2026 at 2:31 PM Mathew Kuthur James <mathewkj2048@xxxxxxxxx> wrote:

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.