如何解决如何将 CONSTANT 值定义为函数,使其域是模型值,而不是字符串?
考虑我有一组节点的情况,我想对它们声明一些排序。最简单的方法是将节点集及其排名声明为常量:
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
模型值作为其域?
解决方法
如果你扩展 TLC
,你可以把它写成 n1 :> 1 @@ n2 :> 2
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。