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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Thu, 10 Jan 2019 05:35:55 -0800 (PST)*References*: <eb0feee2-c52c-470f-8779-b9f086f836a5@googlegroups.com> <BB16E78E-91B6-4788-8462-2E7E3E3FC9FD@gmail.com>

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

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

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 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]_<<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 .

**Follow-Ups**:**Re: [tlaplus] Variable to replace constant***From:*Jack Vanlightly

**References**:**Variable to replace constant***From:*Jack Vanlightly

**Re: [tlaplus] Variable to replace constant***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Variable to replace constant** - Next by Date:
**Re: [tlaplus] Variable to replace constant** - Previous by thread:
**Re: [tlaplus] Variable to replace constant** - Next by thread:
**Re: [tlaplus] Variable to replace constant** - Index(es):