[tlaplus] Initial state doesn't satisfy type invariant

[Tim Leonard <tim@xxxxxxxxxxxxxx>]

I'm starting to use the TLA+ toolkit after a decades-long hiatus in my use of TLA+ and TLC, and am struggling with the basics. My spec's type invariant is failing on the initial state, and I don't see why. Here are the spec, the model configuration, and the error:

--------------------------------------------------------------------------------

(* The relevant part of the spec.                                             *)

--------------------------------------------------------------------------------

CONSTANT  Nodes,

          Labels,

          StartNodes

VARIABLE  node_stack,

          edges_stack

Init ==   /\ node_stack = EMPTY

          /\ edges_stack = Push( EMPTY, StartNodes )

TypeOK == /\ node_stack \in Seq(Nodes)

          /\ edges_stack \in Seq([SUBSET(Labels) -> Nodes])

--------------------------------------------------------------------------------

(* The relevant part of the model configuration.                              *)

--------------------------------------------------------------------------------

Nodes <- { "A", "B", "C", "D", "E", "F" }

Labels <- 1..Cardinality(Nodes)

StartNodes <- << "A" >>

--------------------------------------------------------------------------------

(* The error.                                                                 *)

--------------------------------------------------------------------------------

Invariant TypeOK is violated by the initial state:

/\ edges_stack = <<<<"A">>>>

/\ node_stack = <<>>

I assume that node_stack is satisfying the type invariant, so the problem is

with edges_stack. As I read it, its initial value is a sequence of length one,

with the only element being a function with a domain of { 1 } that maps 1 to "A".

I thought that would also satisfy the type invariant. What am I misunderstanding?

-- 
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/cac57bb6-3d36-433e-a1f9-b3747211fe56n%40googlegroups.com.