Как утверждать, что данное состояние приводит к другому состоянию с переменными в TLA+?

Question

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

variables Requests = {}, Outcomes = {};

У меня есть один набор работников, добавляющих запросы, и другой набор или работников, выполняющих их и пишущих Outcomes, Каждый запрос имеет уникальный Id, который соответствует Outcome запись будет также содержать.

Я хочу гарантировать, что любой запрос добавлен в Requests набор в конечном итоге соответствует структуре с тем же Id в Outcomes задавать. Я пытался сделать это с помощью "приводит к", ~>, оператор, но не могу понять, как решить Id соответствующая часть.

Я наивно пробовал что-то вроде:

RequestsAreFulfilled == \E req \in Requests: TRUE 
                        ~> \E outcome \in Outcomes : outcome.id = req.id

Но это явно ломается, так как req не определяется во втором выражении. Я рассмотрел что-то вроде второго выражения: "Тогда есть состояние, когда все элементы запроса совпадают с элементами результата", но это не работает, так как система никогда не завершается - вполне может быть, всегда будет больше запросов в Requests установить, так как Outcomes всегда играет в догонялки.

Как я могу утверждать, что запрос в конечном итоге совпадает с результатом с тем же идентификатором?

Answer 1

TLC имеет некоторые проблемы с доказательством свойств живучести с помощью непостоянных множеств. Давайте начнем с фиксированного случая, когда у вас есть конечный, фиксированный набор идентификаторов. Тогда мы можем указать отношение как

\A id \in Ids: (\E r \in req: r.id = id) ~> (\E o \in out: o.id = id)

В этом случае, однако, нам лучше использовать структуры, так как их легче понять и лучше выразить общие отношения.

requested = [i \in Ids |-> FALSE];
processed = [i \in Ids |-> FALSE];

\A id \in Ids: requested[i] ~> processed[i]

или же

messages = [i \in Ids |-> [requested |-> FALSE, processed |-> FALSE]]
\A id \in Ids: 
   LET m == messages[i]
   IN  m.requested ~> m.processed

Если вам нужно бесконечное количество сообщений, один из способов заставить TLC обрабатывать проверки живучести - это использовать фиксированный набор идентификаторов, а затем добавить логику для "рециркуляции" готовых сообщений - установить оба requested а также processed ЛОЖЬ. Тогда мы можем использовать оператор всегда-в конце концов, []<>, чтобы выразить это:

\A id \in Ids: []<>(requested[i] => processed[i])