Re: [tlaplus] Variable to replace constant

P.S.: Using operators defined in the TLC module, I could have defined AddRecord more succinctly as

AddRecord(r) ==

/\ rec' = rec \cup {r}

/\ LET newR == [number |-> 0, parity |-> "even"]

IN record' = record @@ (r :> newR)

Best,

Stephan

On Thursday, January 10, 2019 at 2:29:08 PM UTC+1, Stephan Merz wrote:

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>>

=============================================================================

On 10 Jan 2019, at 12:35, Jack Vanlightly <vanli...@xxxxxxxxx> wrote:

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

--
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@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.