tla+ - 如何将 CONSTANT 值定义为函数，使其域是模型值，而不是字符串？

Question

考虑一下我有一组节点的情况，我想对它们声明一些排序。最简单的方法是将节点集及其排名声明为常量：

CONSTANTS Node, NodeRank
ASSUME NodeRank \in [Node -> Nat]
ASSUME \A n, m \in Node : NodeRank[n] = NodeRank[m] <=> n = m

现在是时候为这些常量分配模型值了。Node很简单，我只是将它定义为工具箱中的一组模型值：

Node <- [ model value ] {n1, n2}

NodeRank我尝试用普通作业做类似的事情：

NodeRank <- [n1 |-> 1, n2 |-> 2]

但是，当我运行 TLC 时，这些ASSUME语句被违反了。进一步检查表明这是因为在普通赋值中NodeRank,n1和n2被视为字符串而不是模型值。这是有道理的，因为这是定义记录的常用方法（使用字符串作为域）。我如何定义NodeRank它以使用n1和n2模型值作为其域？

Answer 1

如果你扩展TLC，你可以把它写成n1 :> 1 @@ n2 :> 2.