[Fix] Commands stay Running when user closes their terminal

docs/architecture/task-lifecycle-model.md

@@ -6,14 +6,15 @@ Zoo Code checks task lifecycle protocols through one compositional verification
 pnpm lifecycle:model-check
 ```
 
-The command runs six independent bounded submodels in sequence:
+The command runs seven independent bounded submodels in sequence:
 
 1. the persisted task delegation lifecycle;
 2. shared-store concurrency across task-history hosts;
 3. production-backed provider handoff and scheduler ordering;
 4. the task cleanup protocol;
-5. request-stream parser scoping; and
-6. completion persistence.
+5. request-stream parser scoping;
+6. completion persistence; and
+7. the terminal command lifecycle.
 
 This umbrella command is the single model-check entry point in the `compile` CI job after type checking. Command-level composition does not merge the submodels' state spaces: each checker retains its own bounds, transitions, invariant ownership, reachability requirements, and counterexample format. In particular, parser state is not part of the persisted lifecycle graph. The focused parser checker remains directly runnable with `pnpm parser-scope:model-check` for debugging.
 
@@ -50,6 +51,12 @@ The model has three fixed task slots, enough to cover competing siblings and a n
 
 Production completion also accepts a recovery-compatible `active` parent that still awaits the returning child, then clears the stale pointers. Normal model transitions never create that intermediate state, so it is covered by a focused reducer test rather than admitted as a generally valid reachable state.
 
+## Terminal command lifecycle model
+
+The same command runs a bounded terminal lifecycle explorer for issue #1362. It models command startup, shell activation, one representative buffered output chunk, normal completion, startup or stream failure, concurrent shell-integration waits, tracked superseded processes, and terminal closure. Process registration is atomic with command startup, normal completion and failure release the current process, and a superseded process can only be introduced while a current process exists. Bounding output presence keeps the reachable state space finite without weakening the cleanup property. Its invariants require completion to remain at-most-once, every attached current process to remain tracked, closure to detach the current process and settle every pending wait and tracked process, buffered output to be delivered, and an active stream iterator to be released. Named landmarks retain the important interleavings: closure before command submission, closure after output, closure after a normal end event, closure after an error without a late completion, a superseded process failing without clearing the current owner, duplicate closure, closure with two pending waits, and closure with a superseded process. The checker fails rather than reporting success if the depth boundary still has an unseen enabled successor.
+
+This terminal model is intentionally separate from persisted task delegation state because VS Code terminal events are an extension-host adapter protocol rather than `HistoryItem` transitions. Focused `TerminalRegistry` tests bind the abstract properties to production behavior, including omitted `onDidEndTerminalShellExecution` events and an undefined `exitStatus` during the close callback.
+
 ## Shared-store concurrency model
 
 The same `pnpm lifecycle:model-check` command also runs a second bounded explorer over two `TaskHistoryStore` hosts. It imports the production `computeHistoryDelta` and `mergeHistoryDelta` functions, so its semantics match the store rather than assuming coherent caches or transactional pair writes:

package.json

@@ -13,7 +13,7 @@
 		"check-types": "turbo check-types --log-order grouped --output-logs new-only",
 		"test": "turbo test --log-order grouped --output-logs new-only",
 		"test:mutation-ci": "node --test scripts/stryker-diff.test.mjs",
-		"lifecycle:model-check": "tsx scripts/check-task-lifecycle.ts && tsx scripts/check-task-store-concurrency.ts && tsx scripts/check-provider-handoff-scheduler.ts && pnpm cleanup-protocol:model-check && pnpm parser-scope:model-check && tsx scripts/check-completion-persistence.ts",
+		"lifecycle:model-check": "tsx scripts/check-task-lifecycle.ts && tsx scripts/check-task-store-concurrency.ts && tsx scripts/check-provider-handoff-scheduler.ts && pnpm cleanup-protocol:model-check && pnpm parser-scope:model-check && tsx scripts/check-completion-persistence.ts && tsx scripts/check-terminal-lifecycle.ts",
 		"cleanup-protocol:model-check": "tsx scripts/check-task-cleanup-protocol.ts",
 		"parser-scope:model-check": "node scripts/run-native-tool-call-parser-scoping.mjs",
 		"mcp:integration-check": "tsx scripts/check-mcp-oauth-integration.ts",

scripts/check-terminal-lifecycle.ts

@@ -0,0 +1,269 @@
+type Phase = "idle" | "waiting" | "running" | "completed" | "failed" | "closed"
+type Action = "run" | "wait" | "track-process" | "activate" | "output" | "end" | "error" | "error-superseded" | "close"
+
+interface ModelState {
+	phase: Phase
+	processAttached: boolean
+	commandSubmitted: boolean
+	completionCount: number
+	output: string
+	deliveredOutput: string
+	iteratorReleased: boolean
+	waitsCreated: number
+	pendingWaits: number
+	settledWaits: number
+	processesCreated: number
+	trackedProcesses: number
+	settledProcesses: number
+}
+
+interface TraceStep {
+	action: Action | "initial"
+	state: ModelState
+}
+
+const actions: Action[] = [
+	"run",
+	"wait",
+	"track-process",
+	"activate",
+	"output",
+	"end",
+	"error",
+	"error-superseded",
+	"close",
+]
+const MAX_DEPTH = 9
+const MAX_STATES = 500
+
+function initialState(): ModelState {
+	return {
+		phase: "idle",
+		processAttached: false,
+		commandSubmitted: false,
+		completionCount: 0,
+		output: "",
+		deliveredOutput: "",
+		iteratorReleased: false,
+		waitsCreated: 0,
+		pendingWaits: 0,
+		settledWaits: 0,
+		processesCreated: 0,
+		trackedProcesses: 0,
+		settledProcesses: 0,
+	}
+}
+
+function complete(state: ModelState, phase: "completed" | "closed"): ModelState {
+	return {
+		...state,
+		phase,
+		processAttached: false,
+		completionCount: state.processAttached ? state.completionCount + 1 : state.completionCount,
+		deliveredOutput: state.output,
+		iteratorReleased: state.iteratorReleased || state.phase === "running",
+	}
+}
+
+function transition(state: ModelState, action: Action): ModelState {
+	switch (action) {
+		case "run":
+			return state.phase === "idle"
+				? {
+						...state,
+						phase: "waiting",
+						processAttached: true,
+						processesCreated: state.processesCreated + 1,
+						trackedProcesses: state.trackedProcesses + 1,
+					}
+				: state
+		case "wait":
+			return state.phase !== "closed" && state.waitsCreated < 2
+				? { ...state, waitsCreated: state.waitsCreated + 1, pendingWaits: state.pendingWaits + 1 }
+				: state
+		case "track-process":
+			return state.processAttached && state.processesCreated < 2
+				? {
+						...state,
+						processesCreated: state.processesCreated + 1,
+						trackedProcesses: state.trackedProcesses + 1,
+					}
+				: state
+		case "activate":
+			return state.phase === "waiting"
+				? {
+						...state,
+						phase: "running",
+						commandSubmitted: true,
+						pendingWaits: 0,
+						settledWaits: state.settledWaits + state.pendingWaits,
+					}
+				: state
+		case "output":
+			return state.phase === "running" && state.output === "" ? { ...state, output: "chunk" } : state
+		case "end":
+			return state.phase === "waiting" || state.phase === "running"
+				? {
+						...complete(state, "completed"),
+						trackedProcesses: state.trackedProcesses - 1,
+						settledProcesses: state.settledProcesses + 1,
+					}
+				: state
+		case "error":
+			return state.phase === "waiting" || state.phase === "running"
+				? {
+						...state,
+						phase: "failed",
+						processAttached: false,
+						iteratorReleased: state.iteratorReleased || state.phase === "running",
+						pendingWaits: 0,
+						settledWaits: state.settledWaits + state.pendingWaits,
+						trackedProcesses: Math.max(0, state.trackedProcesses - 1),
+						settledProcesses: state.settledProcesses + (state.trackedProcesses > 0 ? 1 : 0),
+					}
+				: state
+		case "error-superseded":
+			return state.processAttached && state.trackedProcesses >= 2
+				? {
+						...state,
+						trackedProcesses: state.trackedProcesses - 1,
+						settledProcesses: state.settledProcesses + 1,
+					}
+				: state
+		case "close":
+			return state.phase === "closed"
+				? state
+				: {
+						...complete(state, "closed"),
+						pendingWaits: 0,
+						settledWaits: state.settledWaits + state.pendingWaits,
+						trackedProcesses: 0,
+						settledProcesses: state.settledProcesses + state.trackedProcesses,
+					}
+	}
+}
+
+function violations(state: ModelState): string[] {
+	const result: string[] = []
+	if (state.completionCount > 1) result.push("a command completed more than once")
+	if (state.phase === "closed" && state.processAttached) result.push("a closed terminal retained its process")
+	if (state.phase === "closed" && state.pendingWaits !== 0) result.push("a closed terminal retained pending waits")
+	if (state.phase === "closed" && state.trackedProcesses !== 0) {
+		result.push("a closed terminal retained tracked processes")
+	}
+	if (state.settledWaits > state.waitsCreated) result.push("more waits settled than were created")
+	if (state.settledProcesses > state.processesCreated) result.push("more processes settled than were created")
+	if (state.trackedProcesses + state.settledProcesses !== state.processesCreated) {
+		result.push("process registration and settlement accounting diverged")
+	}
+	if (state.processAttached && state.trackedProcesses === 0) result.push("the current process was not tracked")
+	if (state.phase === "closed" && state.commandSubmitted && !state.iteratorReleased) {
+		result.push("closing a submitted command did not release its stream iterator")
+	}
+	if ((state.phase === "completed" || state.phase === "closed") && state.deliveredOutput !== state.output) {
+		result.push("completion did not deliver all buffered output")
+	}
+	return result
+}
+
+function formatCounterexample(message: string, trace: TraceStep[]): string {
+	return [
+		`Terminal lifecycle invariant failed: ${message}`,
+		`Bounds: depth=${MAX_DEPTH}, states=${MAX_STATES}`,
+		...trace.map((step, index) => `${index}. ${step.action}: ${JSON.stringify(step.state)}`),
+	].join("\n")
+}
+
+const landmarks = {
+	"waiting-close-without-submit": (trace: TraceStep[]) =>
+		trace.some((step) => step.action === "run") &&
+		trace.at(-1)?.action === "close" &&
+		trace.at(-1)?.state.commandSubmitted === false &&
+		trace.at(-1)?.state.completionCount === 1,
+	"running-close-after-output": (trace: TraceStep[]) =>
+		trace.some((step) => step.action === "output") &&
+		trace.at(-1)?.action === "close" &&
+		trace.at(-1)?.state.deliveredOutput === "chunk" &&
+		trace.at(-1)?.state.iteratorReleased === true,
+	"end-then-close": (trace: TraceStep[]) =>
+		trace.some((step) => step.action === "end") &&
+		trace.at(-1)?.action === "close" &&
+		trace.at(-1)?.state.completionCount === 1,
+	"error-then-close": (trace: TraceStep[]) =>
+		trace.some((step) => step.action === "error") &&
+		trace.at(-1)?.action === "close" &&
+		trace.at(-1)?.state.processAttached === false &&
+		trace.at(-1)?.state.completionCount === 0,
+	"superseded-error-preserves-owner": (trace: TraceStep[]) =>
+		trace.at(-1)?.action === "error-superseded" &&
+		trace.at(-1)?.state.processAttached === true &&
+		trace.at(-1)?.state.phase === "running" &&
+		trace.at(-1)?.state.trackedProcesses === 1,
+	"duplicate-close": (trace: TraceStep[]) => trace.filter((step) => step.action === "close").length >= 2,
+	"concurrent-waits-close": (trace: TraceStep[]) =>
+		trace.at(-1)?.action === "close" &&
+		trace.at(-1)?.state.waitsCreated === 2 &&
+		trace.at(-1)?.state.pendingWaits === 0 &&
+		trace.at(-1)?.state.settledWaits === 2,
+	"superseded-process-close": (trace: TraceStep[]) =>
+		trace.at(-1)?.action === "close" &&
+		trace.at(-1)?.state.processesCreated === 2 &&
+		trace.at(-1)?.state.trackedProcesses === 0 &&
+		trace.at(-1)?.state.settledProcesses === 2,
+} satisfies Record<string, (trace: TraceStep[]) => boolean>
+
+const start = initialState()
+const queue: Array<{ state: ModelState; trace: TraceStep[] }> = [
+	{ state: start, trace: [{ action: "initial", state: start }] },
+]
+const visited = new Set([JSON.stringify(start)])
+const reachedActions = new Set<Action>()
+const reachedLandmarks = new Set<string>()
+const frontier: ModelState[] = []
+
+for (let index = 0; index < queue.length; index++) {
+	const node = queue[index]!
+	const stateViolations = violations(node.state)
+	if (stateViolations.length) throw new Error(formatCounterexample(stateViolations.join("; "), node.trace))
+	for (const [name, predicate] of Object.entries(landmarks)) {
+		if (predicate(node.trace)) reachedLandmarks.add(name)
+	}
+	if (node.trace.length - 1 === MAX_DEPTH) {
+		frontier.push(node.state)
+		continue
+	}
+
+	for (const action of actions) {
+		const next = transition(node.state, action)
+		const trace = [...node.trace, { action, state: next }]
+		for (const [name, predicate] of Object.entries(landmarks)) {
+			if (predicate(trace)) reachedLandmarks.add(name)
+		}
+		if (next === node.state) continue
+		reachedActions.add(action)
+		const key = JSON.stringify(next)
+		if (visited.has(key)) continue
+		visited.add(key)
+		queue.push({ state: next, trace })
+		if (visited.size > MAX_STATES) throw new Error(`Terminal lifecycle exceeded its ${MAX_STATES}-state budget`)
+	}
+}
+
+const unexploredSuccessor = frontier
+	.flatMap((state) => actions.map((action) => ({ action, next: transition(state, action) })))
+	.find(({ next }) => !visited.has(JSON.stringify(next)))
+if (unexploredSuccessor) {
+	throw new Error(
+		`Terminal lifecycle exploration reached depth ${MAX_DEPTH} with an unseen successor (${unexploredSuccessor.action}); increase the depth bound`,
+	)
+}
+
+const missingActions = actions.filter((action) => !reachedActions.has(action))
+if (missingActions.length) throw new Error(`Terminal lifecycle has unreachable actions: ${missingActions.join(", ")}`)
+const missingLandmarks = Object.keys(landmarks).filter((name) => !reachedLandmarks.has(name))
+if (missingLandmarks.length)
+	throw new Error(`Terminal lifecycle has unreachable landmarks: ${missingLandmarks.join(", ")}`)
+
+console.log(
+	`Terminal lifecycle model check passed: ${visited.size} reachable states, ${actions.length}/${actions.length} actions reachable, ${Object.keys(landmarks).length}/${Object.keys(landmarks).length} landmarks reached, depth <= ${MAX_DEPTH}`,
+)