[tlaplus] TypeOK for primed variables

[Mathew Kuthur James <mathewkj2048@xxxxxxxxx>]

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.