在TLA+中过滤元组同时保持顺序

Question

我正在TLA+中对主备份协议进行建模，并在元组中进行复制配置。一些设置TLA+：

NNodes == 3
Nodes == 1..NNodes

然后，在Pluscal算法中：

config = << 1, 2, 3 >>;
healthy = [ n \in Nodes |-> TRUE ];

我有一个进程，它将healthy中的值设置为FALSE，并希望有另一个进程根据healthy是否为FALSE从配置中删除条目，同时保留配置中其余条目的顺序。

如果config是一个集合，那么删除不健康的条目将是微不足道的，但是我正在寻找一种用元组来实现这一点的好方法。我可以在循环中使用Append，但这会导致TLC处理许多额外的状态。在TLA+或Pluscal有更好的方法吗？

理想情况下，解决方案不会假设配置中的条目按排序顺序开始，但我可以绕过这个限制。

Answer 1

Sequences模块包含SelectSeq操作符，它解决了您的确切用例。它看起来就像

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

见“指定系统”第341页。

Answer 2

配置元素的顺序重要吗？否则，我会建议用一个集合config = {1,2,3}来替换它。您可以轻松地将设置筛选为set config \ {2}。