CODEWITHSUNDEEP
tla+
Marc Brooker
Marc Brooker

Reputation: 473

Filtering a tuple while preserving order in TLA+

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.

Upvotes: 3

Views: 663

Answers (2)

Hovercouch
Hovercouch

Reputation: 2314

The Sequences module contains the SelectSeq operator, which solves your exact use case. It will look something like

SelectSeq(config, LAMBDA x: healthy[x])

See page 341 of Specifying Systems.

Upvotes: 5

lambda.xy.x
lambda.xy.x

Reputation: 4998

Does the order of config elements matter? Otherwise I'd propose to replace it with a set config = {1,2,3}. You can easily filter the set as set difference config \ {2}.

Upvotes: 0

Related Questions