Manipulating states of a set without turning into a sequence

[tlalearner]

Hello,

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]

    ]

Thanks