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

Re: [tlaplus] Variable to replace constant

I added a RemoveRecord action as follows:

RemoveRecord(r) ==
  /\ rec' = rec \ {r}
  /\ record' = [x \in DOMAIN record \ {r} |-> record[x]]

This is just a toy example but it is a precursor to me understanding how to model a cluster of nodes that can come and go and coordinate their state. I needed to understand first how to be able to add and remove nodes and modify their state. I understand that I could also avoid the addition/removal completely by using NULL or setting some value indicating that the item is no longer around.


On Thursday, January 10, 2019 at 2:48:58 PM UTC+1, Jack Vanlightly wrote:
Hi Stephen,

Thanks a lot it works great, and thanks for showing both versions of AddRecord. I'm going to try and write a RemoveRecord now.


On Thursday, January 10, 2019 at 2:35:55 PM UTC+1, Stephan Merz wrote:
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)


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,

------------------------------ MODULE Records ------------------------------
EXTENDS Integers, FiniteSets, TLC
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 <vanl...@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

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

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 tlaplu...@xxxxxxxxxxxxxxxx.
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.