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

Question

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

NNodes == 3
Nodes == 1..NNodes

然后，在 Pluscal 算法中：

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

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

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

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

Answer 1

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

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

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

Answer 2

配置元素的顺序重要吗？否则我建议用 set 替换它config = {1,2,3}。您可以轻松地将集合过滤为集合差异config \ {2}。