[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Variable to replace constant

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