tla+ - 在 TLA+ 中保留顺序的同时过滤元组

Question

我正在为 TLA+ 中的主-备份协议(protocol)建模，并在元组中进行复制配置。一些设置 TLA+:

NNodes == 3
Nodes == 1..NNodes

然后，在 Pluscal 算法中:

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

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

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

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

Answer 1

Sequences 模块包含 SelectSeq 运算符，可解决您的确切用例。它看起来像

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

请参阅指定系统的第 341 页。