| An update resulting from experience: I was able to define a set of partial functions as I hoped, but found that in non-trivial models, the cardinality of sets of partial functions quickly exceeded the size that TLC was willing to enumerate. Instead, I wound up using this as a type constraint to achieve the same goal while keeping TLC happy: CONSTANT
-- Nodes, \* The set of nodes in the graph. Labels, \* The set of edge labels. EdgesOf, \* The labeled out edges of each node. StartEdges, \* The labeled starting points. IsGoal \* Whether a node is a goal node. ConstantTypeOK == /\ Nodes # {} /\ DOMAIN(EdgesOf) = Nodes /\ \A node \in Nodes : \A label \in DOMAIN(EdgesOf[node]) : /\ label \in Labels /\ EdgesOf[node][label] \in Nodes /\ \A label \in DOMAIN(StartEdges) : /\ label \in Labels /\ StartEdges[label] \in Nodes /\ DOMAIN(StartEdges) # {} /\ IsGoal \in [Nodes -> BOOLEAN] You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0EE6B21F-EEC3-4345-9B25-A521F017F96E%40RyanLeonard.us. |