fix(main): report transition-assertion failures on the inbound link (#362)

CheckTransitionInvariants stores its failure metadata on the *inbound
link* (node.Inbound[0].FailedInvariants) rather than on the node's
Process.FailedInvariants — see processor.go where the write happens.
The failure-reporting branch in modelCheckSingleSpec only looked at
the Process field, with these wrong consequences:

- Simulation mode: a transition-assertion failure fell through to
  "FAILED: Model checker failed. Deadlock/stuttering detected", which
  is misleading (deadlock_detection: false in the spec confirms it
  was not a deadlock).
- Model-checking mode: nothing about the failure was printed at all,
  only the raw trace dump from dumpFailedNode.

Now: if the node has no Process.FailedInvariants, check the inbound
link. Print "Transition Invariant: <name>" if found. Add a generic
"Model checker failed (no failed-invariant metadata...)" fallback for
model-checking mode so silence never happens.

Reproducer: a spec with a `transition assertion` that the model
checker finds violating — previously misreported. Confirmed both
modes now print the assertion name (TerminalStatesRemainTerminal in
the test spec).

Co-authored-by: jayaprabhakar <jayaprabhakar@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: 3 people

main.go

@@ -870,10 +870,21 @@ func modelCheckSingleSpec(f *ast.File, stateConfig *ast.StateSpaceOptions, dirPa
 
 		} else if failedNode != nil {
 			clearProgressLine()
+			// Always-assertion failures live on the node's Process.FailedInvariants.
+			// Transition-assertion failures live on the *inbound link* — see
+			// processor.go where CheckTransitionInvariants writes to
+			// node.Inbound[0].FailedInvariants. Without checking the link, a
+			// transition-assertion failure in simulation falls through to the
+			// misleading "Deadlock/stuttering" message, and in model-checking
+			// mode nothing about the failure is printed at all.
 			if failedNode.FailedInvariants != nil && len(failedNode.FailedInvariants) > 0 && len(failedNode.FailedInvariants[0]) > 0 {
 				fmt.Println("FAILED: Model checker failed. Invariant: ", f.Invariants[failedNode.FailedInvariants[0][0]].Name)
+			} else if len(failedNode.Inbound) > 0 && failedNode.Inbound[0].FailedInvariants != nil && len(failedNode.Inbound[0].FailedInvariants[0]) > 0 {
+				fmt.Println("FAILED: Model checker failed. Transition Invariant:", f.Invariants[failedNode.Inbound[0].FailedInvariants[0][0]].Name)
 			} else if simulation {
 				fmt.Println("FAILED: Model checker failed. Deadlock/stuttering detected")
+			} else {
+				fmt.Println("FAILED: Model checker failed (no failed-invariant metadata on the failing node; see trace below).")
 			}
 			if simulation {
 				fmt.Println("seed:", p1.Seed)