2

对不起，标题有点神秘。我有一个 TLA+ 规范，它定义了两组：

variables Requests = {}, Outcomes = {};

我有一组工人添加请求，另一组或工人满足它们并写信给Outcomes. 每个请求都有一个唯一Id的，匹配的Outcome条目也将包含它。

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

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

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

但这显然会中断，因为req在第二个表达式中没有定义。我已经考虑过第二个表达的内容是“然后有一个状态，所有请求项都与结果项匹配”，但这不起作用，因为系统永远不会终止 - 很可能总是有更多的请求中Requests盘，自是Outcomes一直在追赶。

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

4

1 回答 1

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，然后添加逻辑以“回收”已完成的消息 - 同时设置requested和设置processed为 FALSE。然后我们可以使用 always-eventually 运算符[]<>, 来表达：

\A id \in Ids: []<>(requested[i] => processed[i])
于 2017-10-11T18:53:09.560 回答