Re: [tlaplus] Need help to update the state with EXCEPT.

[Stephan Merz <stepha...@xxxxxxxxx>]

An EXCEPT construct updates a function / record at a fixed number of positions, so it is not suitable by itself to perform an update on a number of positions that is determined by a variable or parameter. Also, the deep nesting of records will make the notation a little heavy-handed.

You could write the following

inMemoryState' = 

 LET hks(ims,m) == ims.hkState[m]  \* retrieve the hkState component for a machine from an inMemoryState

 IN  [p \in RMs |-> 

        [inMemoryState[p] 

           EXCEPT !.hkState = [m \in 1 .. MachinesInRing |-> 

                                 [hks(@,m) EXCEPT !.state = "working"]]]]

Alternatively, you can encapsulate the update in a suitable operator definition and use it in your action, such as

SetToWorking(ims) ==

   [ims EXCEPT !.hkState = [m \in 1 .. MachinesInRing |-> [@[m] EXCEPT !.state = "working"]]]

\* within the action definition:

...

/\ inMemoryState' = [p \in RMs |-> SetToWorking(inMemoryState[p])]

...

Note that "@" in the definition of SetToWorking refers to ims.hkState.

Hope this helps,

Stephan

On 12 Dec 2017, at 21:49, gajera...@xxxxxxxxx wrote:

rslInitState == [machine \in 1..MachinesInRing |->
[scaleUnit |-> machine,
 isNodeUp |-> TRUE,
 isPrimary |-> FALSE]]

hkInitState == [machine \in 1..MachinesInRing |->
  [state |-> "init",
retryCount |-> 1]]

inMemoryState = [p \in RMs |->
[rslState |-> rslInitState,
hkState |-> hkInitState ,
isDriver |-> FALSE]]

I have one "inMemoryState", show above is the init state.

Now in one of the function I want to change the inMemoryState of All RMs and all machines, hkState.state to "working" while rest I want to keep it same.
Example, inMemoryState[r].hkState[1..MachinesInRing].state = "working"

I can do something like below.
/\ inMemoryState' = [lp \in RMs |->
                            [m \in 1..MachinesInRing |->
                               IF p = lp
                                   THEN []
                               ELSE []]]

But is there an easy way where I can use EXCEPT and do the same in one line ?

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