Фильтрация кортежа при сохранении порядка в TLA +

Question

Я работаю над моделированием протокола первичного резервного копирования в TLA +, и у меня есть конфигурация репликации в кортеже. Некоторые настройки TLA +:

NNodes == 3
Nodes == 1..NNodes

Затем в алгоритме Плюскала:

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

У меня есть процесс , который устанавливает значения в healthy на FALSE, и мне нужен другой процесс, который удаляет записи из config в зависимости от того, является ли исправным значение FALSE. сохраняя порядок оставшихся записей в config .

Если бы config был набором, удаление нездоровых записей было бы тривиально, но я ищу хороший способ сделать это с помощью кортежа. Я могу использовать Append в цикле, но это заставляет TLC иметь дело со многими дополнительными состояниями. Есть ли лучшие способы в TLA + или Pluscal?

В идеале решение не предполагает, что записи в конфигурации начинаются в отсортированном порядке, но я мог бы обойти это ограничение.

Answer 1

Модуль Sequences содержит оператор SelectSeq, который решает ваш конкретный вариант использования.Это будет выглядеть примерно так:

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

См. Страницу 341 из Указывающие системы .

Answer 2

Имеет ли значение порядок элементов конфигурации? В противном случае я бы предложил заменить его на набор config = {1,2,3}. Вы можете легко отфильтровать набор как разность набора config \ {2}.