Why does TLC find two initial states?

[Tim Leonard]

When I run TLC on my spec, the Model Checking Results page shows that the Init action occurred twice. But I think that Init specifies a unique initial state:

Init ==

  /\ depth_limit = 2

  /\ node_stack = Push( EMPTY, Start )

  /\ edges_tried = 0

  /\ deque = EMPTY

  /\ progress_stack = Push( EMPTY, FALSE )

  /\ deadend = {}

  /\ done = {}

(The model defines Start to be “a1”.) Why does the Init action occur twice?