如何在 TLA+ 中断言一个给定状态会导致另一个带有变量的状态？

Question

抱歉，标题有点隐晦。我有一个定义两组的 TLA+ 规范：

variables Requests = {}, Outcomes = {};

我有一组工作人员添加请求，另一组工作人员完成这些请求并写入 Outcomes。每个请求都有一个唯一的 Id，匹配的 Outcome 条目也将包含它。

我想保证添加到 Requests 集合的任何请求最终都与 Outcomes 集合中具有相同 Id 的结构相匹配。我一直在尝试使用 "leads to"、~> 运算符来执行此操作，但无法弄清楚如何解析 Id 匹配部分。

我曾经天真地尝试过类似的东西：

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

但这显然会中断，因为 req 未在第二个表达式中定义。我已经考虑过与第二个快递 "Then there is a state where all Request items are matched by Outcome items" 类似的东西，但这不起作用，因为系统永远不会终止 - Requests 集中可能总是有更多请求，因为 Outcomes 总是播放 catch-up.

我断言请求最终与具有相同 ID 的结果相匹配的方法是什么？

Answer 1

TLC 在使用非常量集证明活性属性时遇到了一些麻烦。让我们从固定情况开始，在这种情况下，您有一组有限的、固定的 id。然后我们可以将关系指定为

\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 处理活动检查的一种方法是使用一组固定的 ID，然后将逻辑添加到 "recycle" 已完成的消息 - 设置两者 requested processed 为 FALSE。然后我们可以使用始终最终运算符 []<> 来表示：

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

如何在 TLA+ 中断言一个给定状态会导致另一个带有变量的状态？

How to assert a given state leads to a another state with variables in TLA+?

tla+