I'm working on modelling a primary-backup protocol in TLA+, and have the replication configuration in a tuple. Some setup TLA+:
NNodes == 3 Nodes == 1..NNodes
Then, in a Pluscal algorithm:
config = << 1, 2, 3 >>; healthy = [ n \in Nodes |-> TRUE ];
I have a process which sets the values in healthy to FALSE, and want another process which removes the entries from config based on whether healthy is FALSE while preserving the order of the remaining entries in config.
If config was a set, removing the unhealthy entries would trivial, but I'm looking for a good way to do that with a tuple. I can use Append in a loop, but that causes a lot of extra states for TLC to deal with. Any better ways in TLA+ or Pluscal?
Ideally the solution wouldn't assume that the entries in config start off in sorted order, but I could work around that limitation.