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

[tlaplus] Manipulating states of a set without turning into a sequence


I'm very new to TLA+, I apologize in advance if the question isn't too clear.

I have a list of nodes that lives in a server. What I'm trying to do model is a server failure -- when a server fails, all nodes tied to that server fails at the same time. 

Here is a function representation of the nodes variable:

\*nodeId |-> 0..total number of nodes (server * nodesPerServer)
\*servers |-> Set of servers. Each element is also a function of:
\*    server |-> Server that the node lives in
\*    state |-> Failed, Available
\* Example: [nodeId |-> 1, servers |-> {[server |-> S1, state |-> "Available" ]} ]

The following is how I initialize the nodes variable, followed by a definition of simulating a server failure. I can do all this by turning the set into sequences, but that seems very wasteful. Is there a way to keep them as sets while accomplishing the same thing? I'm asking because ordering of how servers fail does not really matter.

\* SetToSeq is a Helper method from https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla  

serverINIT ==
        serverCount == Cardinality(servers)
        nodesPerServer == 4
        nodeCount == serverCount * nodesPerServer 
        serverSequence == SetToSeq(servers) 
    IN nodes 
        = [nid \in 0..(nodeCount) |->
                [nodeId |-> nid, servers |-> {[server |-> serverSequence[1 + (nid \div nodeCount)], state |-> "Available"]}]

failServer(serverToFail) ==
    nodes' = [sid \in DOMAIN nodes |-> 
                nodeServers == nodes[sid].servers
                serverCount == Cardinality(servers)
                serverSequence == SetToSeq(servers)
                    serversAfterFailure ==
                        { IF
                         /\ serverSequence[x].server = serverToFail
                         /\ serverSequence[x].state = "Available" 
                            [serverSequence[x] EXCEPT !.state = "Failed"]
                         : x \in 1..serverCount }   
                IN [servers[sid] EXCEPT !.servers = serversAfterFailure]


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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/aa8f59c2-f884-4347-b451-bde28b897e96n%40googlegroups.com.