小编Mar*_*ker的帖子

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

NNodes == 3
Nodes == 1..NNodes

然后，在 Pluscal 算法中：

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

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

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

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