Variable to replace constant

[Jack Vanlightly <vanli...@xxxxxxxxx>]

Hi all,

I have been struggling to achieve something that I thought would be pretty simple. For a learning exercise I have a set of records which have a "number" and a "parity" field. In each step, a record has its number incremented and its parity updated until it reaches the number 4.

EXTENDS Integers, FiniteSets, TLC
CONSTANTS R
VARIABLES record

Record == [number : Nat, parity : {"odd","even"}]

Init == record \in [R -> {[number |-> 0, parity |-> "even"]}]
                                   
BecomeOdd(r) == /\ record[r].number < 4
                /\ record[r].number % 2 = 0
                /\ record' = [record EXCEPT ![r].parity = "odd",
                                            ![r].number = record[r].number + 1]
                                  
BecomeEven(r) == /\ record[r].number < 4
                 /\ record[r].number % 2 = 1
                 /\ record' = [record EXCEPT ![r].parity = "even",
                                             ![r].number = record[r].number + 1]

Next == \E r \in R : BecomeOdd(r) \/ BecomeEven(r)
        
Spec == Init /\ [][Next]_<<record>>

I run it with R as { 1, 2, 3} and it deadlocks on step 13 once all 3 by 4 increments have been performed, as expected.

My question is this: how can I make R a variable "rec" and change the number of records dynamically? I can initialize "rec" to {} and add new elements using a union operator and incrementing a counter for the value. But I can't work out how to add new elements to "record" that correspond to new elements in "rec".

I want my Next step to look something like:

Next == AddRecord \/ \E r \in rec : BecomeOdd(r) \/ BecomeEven(r)

Any help would be greatly appreciated
Jack