[SOLVED] How do I define a CONSTANT value as a function so its domain is model values, not strings?

How do I define a CONSTANT value as a function so its domain is model values, not strings?

Consider the case where I have a set of nodes, and I want to declare some ordering over them. The easiest way to do this is to declare both the set of nodes and their ranking as constants:

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

Now it comes time to assign model values to these constants. Node is easy enough, I just define it as a set of model values in the toolbox:

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

I try to do something similar with NodeRank with ordinary assignment:

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

However, when I run TLC the ASSUME statements are violated. Further examination reveals this is because in the ordinary assignment of NodeRank, n1 and n2 are treated as strings instead of model values. This makes sense, because that is the usual method of defining records (which use strings as their domain). How do I define NodeRank such that it uses the n1 and n2 model values as its domain?

Solution

If you extend TLC, you can write this as n1 :> 1 @@ n2 :> 2.