| Hi Jack, welcome to this group! Below is a possible solution (I combined the two actions BecomeOdd and BecomeEven into a single one just to make the spec a bit shorter). As for the initialization, note that the empty sequence is also the function with empty domain, I could instead have written record \in [rec -> Record] which would perhaps have been a little less obscure. Hope this helps, Stephan ------------------------------ MODULE Records ------------------------------ EXTENDS Integers, FiniteSets, TLC CONSTANTS R VARIABLES rec, record Record == [number : Nat, parity : {"odd","even"}] Init == /\ rec = {} /\ record = << >> Inv == /\ rec \subseteq R /\ record \in [rec -> Record] AddRecord(r) == /\ rec' = rec \cup {r} /\ LET newR == [number |-> 0, parity |-> "even"] IN record' = [rr \in rec' |-> IF rr \in rec THEN record[rr] ELSE newR] ChangeParity(r) == /\ record[r].number < 4 /\ record' = [record EXCEPT ![r].parity = IF record[r].number % 2 = 0 THEN "odd" ELSE "even", ![r].number = @ + 1] /\ UNCHANGED rec Next == \/ \E r \in R \ rec : AddRecord(r) \/ \E r \in rec : ChangeParity(r) Spec == Init /\ [][Next]_<<rec,record>> =============================================================================
|