[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Initial state doesn't satisfy type invariant

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:

  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.