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" ]} ]
VARIABLE nodes
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 ==
LET
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 |->
LET
nodeServers == nodes[sid].servers
serverCount == Cardinality(servers)
serverSequence == SetToSeq(servers)
IN
LET
serversAfterFailure ==
{ IF
/\ serverSequence[x].server = serverToFail
/\ serverSequence[x].state = "Available"
THEN
[serverSequence[x] EXCEPT !.state = "Failed"]
ELSE
serverSequence[x]
: x \in 1..serverCount }
IN [servers[sid] EXCEPT !.servers = serversAfterFailure]
]