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

# Re: [tlaplus] Variable to replace constant

 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 writtenrecord \in [rec -> Record]which would perhaps have been a little less obscure.Hope this helps,Stephan------------------------------ MODULE Records ------------------------------EXTENDS Integers, FiniteSets, TLCCONSTANTS RVARIABLES rec, recordRecord == [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 recNext ==  \/ \E r \in R \ rec : AddRecord(r)  \/ \E r \in rec : ChangeParity(r)Spec == Init /\ [][Next]_<>=============================================================================On 10 Jan 2019, at 12:35, Jack Vanlightly 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, TLCCONSTANTS RVARIABLES recordRecord == [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]_<>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 appreciatedJack-- 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+u...@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.