Overhaul PeasyAI validation pipeline and improve code generation quality

- Replace ad-hoc code review with unified 4-stage validation pipeline:
  Stage 1: PCodePostProcessor (deterministic regex auto-fixes)
  Stage 2: Structured validator chain (13 validators with auto-fix)
  Stage 3: LLM wiring review for test files (circular deps, init order)
  Stage 4: LLM spec correctness review (observes completeness, assertions)
- Add NamedTupleConstructionValidator for cross-file type checking
- Add extraneous-semicolon auto-fix in SyntaxValidator
- Fix ValidationPipeline context merging for preview-time cross-file validation
- Update Timer template with bounded delays for liveness property support
- Update FailureDetector design doc: liveness property, hot states, Timer as component
- Add review_test_wiring and review_spec_correctness LLM review prompts
- Improve generation prompts: named tuples, circular dependency patterns, helper fns
- Fix streamlit lazy-import issue for non-UI contexts
- Remove stale tools (simulator, trace_explorer) and dead code
- Increase PChecker per-test timeout from 20s to 300s
- Update CLAUDE.md with pipeline architecture docs and fix stale .env references
- Add regression test support for wiring_fixes and spec_fixes

Made-with: Cursor

Author: ankushdesai

CLAUDE.md

@@ -23,4 +23,23 @@ Write the enums, types, and events required for each of the state machines. If m
 
 4. **Do NOT declare config init events** (like eProposerInit, eAcceptorInit) unless the design explicitly uses the init-event pattern. Most machines use the constructor payload pattern where config is passed via `new Machine(config)`.
 
+5. **Named tuple construction must match the type definition exactly.** Every ``type`` you define here will be used in ``new Machine(...)`` and ``send ..., eEvent, ...`` call sites throughout the project. The field names you choose become the API contract:
+   ```
+   // Given this type definition:
+   type tNodeConfig = (failureDetector: machine);
+   // ALL construction sites MUST use the exact field name:
+   new Node((failureDetector = fd,));          // CORRECT
+   new Node((fd,));                            // WRONG — anonymous tuple
+   new Node(fd);                               // WRONG — bare value
+   ```
+   Choose field names carefully — they cannot be changed later without updating every call site.
+
+6. **Event payload types define the send-site contract.** When you declare ``event eFoo: tBarPayload;``, every ``send target, eFoo, ...`` in the project must construct a ``tBarPayload`` with named fields:
+   ```
+   // Given: event eNodeSuspected: tNodeSuspectedPayload;
+   //        type tNodeSuspectedPayload = (suspectedNode: machine);
+   send client, eNodeSuspected, (suspectedNode = node,);   // CORRECT
+   send client, eNodeSuspected, (node);                     // WRONG
+   ```
+
 Return only the generated P code without any explanation attached. Return the P code enclosed in <Enums_Types_Events.p></Enums_Types_Events.p>.

Src/PeasyAI/resources/instructions/generate_enums_types_events.txt

@@ -36,6 +36,18 @@ When the Enums_Types_Events.p file is provided as context, you MUST use the EXAC
   WRONG:   fun HandlePromise(msg: tPromise) {{ ... msg.propNum ... msg.value ... }}
 The function parameter type annotation MUST match the event's payload type exactly as declared.
 
+## File-scope helper functions:
+Some machines provide convenience helper functions declared OUTSIDE the machine body (at file scope). For example, a Timer machine may provide:
+```
+fun CreateTimer(client: machine) : Timer {{
+  return new Timer(client);
+}}
+fun StartTimer(timer: Timer) {{
+  send timer, eStartTimer;
+}}
+```
+If the design document specifies helper functions for this machine, include them after the machine's closing brace.
+
 ## Checklist before returning code:
 - Every state has handlers, defer, or ignore for EVERY event this machine could receive.
 - The start state entry correctly unpacks the constructor payload (if parameterized).
@@ -44,5 +56,6 @@ The function parameter type annotation MUST match the event's payload type exact
 - Single-field named tuple VALUES always have a trailing comma: ``(field = value,)``. But type annotations do NOT: ``fun Foo(x: tMyType)`` or ``fun Foo(x: (field: int))``.
 - All type names in function signatures match EXACTLY what is declared in Enums_Types_Events.p.
 - All field names in payload access (e.g., payload.fieldName) and construction (e.g., (fieldName = value,)) match EXACTLY what is declared in the type definition.
+- If the design doc specifies file-scope helper functions, they are included after the machine body.
 
 Verify that the generated code strictly follows all the P syntax rules before considering it final. Return only the generated P code without any explanation attached. Return the P code enclosed in XML tags where the tag name is the filename.

Src/PeasyAI/resources/instructions/generate_machine.txt

@@ -94,6 +94,9 @@ When the Enums_Types_Events.p file is provided as context, you MUST use the EXAC
   CORRECT: on ePromise do HandlePromise;  ...  fun HandlePromise(msg: tPromisePayload) {{ ... }}
   WRONG:   on ePromise do HandlePromise;  ...  fun HandlePromise(msg: tPromise) {{ ... }}
 
+## File-scope helper functions:
+If the design document specifies helper functions for this machine (e.g., CreateTimer, StartTimer), include their declarations (with empty bodies) AFTER the machine's closing brace. These are convenience wrappers declared at file scope.
+
 The machine file should NOT contain:
 
 1. Specification monitors (spec keyword)

Src/PeasyAI/resources/instructions/generate_machine_structure.txt

@@ -105,12 +105,63 @@ test tcBasicPaxos [main=Scenario1_BasicPaxos]:
     {{ Proposer, Acceptor, Learner, Client, Scenario1_BasicPaxos }};
 ```
 
+## CRITICAL — Resolving Circular Dependencies in Machine Wiring
+
+Sometimes there is a circular dependency: Machine A's constructor needs a reference to Machine B, and Machine B's constructor needs a collection of Machine A instances. You MUST resolve this correctly.
+
+Strategy: break the cycle by using an initialization event for one side.
+
+Example — FailureDetector needs a `seq[Node]`, but each Node needs the FD reference:
+```
+// Step 1: Create nodes WITHOUT the FD reference (they'll get it via an init event)
+node1 = new Node();
+node2 = new Node();
+nodes += (0, node1);
+nodes += (1, node2);
+
+// Step 2: Create the FD with the node list
+fd = new FailureDetector((nodes = nodes,));
+
+// Step 3: Send the FD reference to each node via an init event
+send node1, eNodeInit, (failureDetector = fd,);
+send node2, eNodeInit, (failureDetector = fd,);
+```
+
+Alternative: if the Node machine accepts its config via constructor payload and has no circular dependency, simply create machines in the right order:
+```
+// If FD doesn't need node references at construction time:
+fd = new FailureDetector();
+node1 = new Node((failureDetector = fd,));
+node2 = new Node((failureDetector = fd,));
+```
+
+The key rule: every machine reference passed in a constructor or event payload must point to an already-created machine that will correctly handle the events sent to it.
+
+## CRITICAL — Named Tuple Construction
+
+When a machine's entry function expects a named-tuple type like ``tConfig = (field1: T1, field2: T2)``, you MUST construct it with named fields:
+```
+CORRECT: new Machine((field1 = val1, field2 = val2));
+WRONG:   new Machine((val1, val2));          // anonymous tuple — type mismatch!
+WRONG:   new Machine(val1);                  // bare value — type mismatch!
+```
+For single-field types, include a trailing comma: ``new Machine((field = value,));``
+
+Similarly for ``send``: if ``event eFoo: tPayload;`` and ``type tPayload = (bar: int);``, then:
+```
+CORRECT: send target, eFoo, (bar = 42,);
+WRONG:   send target, eFoo, (42);            // anonymous — type mismatch!
+WRONG:   send target, eFoo, (this);          // bare value — type mismatch!
+```
+
 ## Checklist before returning code:
 - Every scenario machine is matched by a `test` declaration.
 - Every `test` declaration includes `assert SpecName in` referencing the spec monitors from PSpec. Without `assert`, PChecker won't verify any properties.
 - All machines used in the scenario are listed inside the braces `{{ ... }}`.
 - No events, types, or machines from PSrc are redeclared.
 - Machine creation order respects dependencies.
 - Single-field named tuples have trailing commas: `(field = value,)`.
+- Every machine reference in a constructor payload points to a real, already-created machine that handles the expected events.
+- Every `new Machine(...)` and `send ..., eEvent, ...` uses named tuple syntax matching the type definition.
 
 Verify that the generated code strictly follows all the P syntax rules before considering it final. Return only the generated P code without any explanation attached. Return the P code enclosed in XML tags where the tag name is the filename.

Src/PeasyAI/resources/instructions/generate_test_files.txt

@@ -0,0 +1,107 @@
+You are reviewing a P specification monitor file for correctness against the design document's safety properties.
+
+You are given:
+1. The generated spec monitor code.
+2. All machine source files (showing events each machine sends/handles).
+3. The Enums_Types_Events.p file (showing all events and their payload types).
+4. The design document (showing the intended safety properties).
+
+Your job is to check the following and return a FIXED version of the spec file:
+
+## CHECK 1: Observes Clause Completeness
+The spec must observe ALL events it needs to verify the safety property.
+
+Think step-by-step:
+- Read the safety property from the design document.
+- Identify which events carry information relevant to that property.
+- Verify the `observes` clause includes all of them.
+
+Example — "If a node crashes, it must eventually be suspected":
+- Needs `eCrash` (to know which node crashed)
+- Needs `eNodeSuspected` (to know which node was suspected)
+- Needs `eHeartbeat` (to know a crashed node stopped sending heartbeats)
+
+BAD: `spec ReliableDetection observes eNodeSuspected { ... }`
+GOOD: `spec ReliableDetection observes eCrash, eHeartbeat, eNodeSuspected { ... }`
+
+## CHECK 2: Correct Event-to-Machine Tracking
+The spec must correctly track which machine an event refers to. Events carry payload with machine references — the spec must use the payload to identify the specific machine.
+
+BAD (tracks nothing specific):
+```
+on eCrash do {
+    crashCount = crashCount + 1;
+}
+```
+
+GOOD (tracks which machine crashed):
+```
+on eCrash goto CrashHandling with HandleCrash;
+```
+But wait — `eCrash` has no payload in many designs. If `eCrash` is sent to a specific node, the spec sees the event but doesn't know WHICH node received it. In that case, the spec needs a different strategy.
+
+KEY INSIGHT: Spec monitors observe events globally. `on eCrash do ...` fires for EVERY `eCrash` event in the system. If `eCrash` has no payload, the spec cannot know which machine was the target. The spec must use other observable events (like the absence of heartbeats from a specific node) to infer crashes.
+
+If an event has a payload (e.g., `event eNodeSuspected: tNodeSuspectedPayload;` with `type tNodeSuspectedPayload = (suspectedNode: machine);`), the handler MUST accept the payload parameter and use it:
+
+BAD:
+```
+on eNodeSuspected do {
+    suspectedCount = suspectedCount + 1;
+}
+```
+
+GOOD:
+```
+on eNodeSuspected do (payload: tNodeSuspectedPayload) {
+    suspectedNodes += (payload.suspectedNode);
+}
+```
+
+## CHECK 3: Assertion Logic Matches the Safety Property
+The assertions must actually verify what the design document says. Read the property carefully and check that the assert conditions are correct.
+
+Example property: "If a node crashes, it must eventually be suspected"
+- This means: after eCrash for node X, eventually eNodeSuspected for node X should fire.
+- The spec should track crashed nodes and suspected nodes, and assert consistency.
+
+BAD assertion (checks something unrelated):
+```
+assert !(node in heartbeatAfterSuspicion),
+    "Node sent heartbeat after suspicion";
+```
+
+GOOD assertion (checks the actual property):
+```
+// Track that a crashed node was indeed suspected
+on eNodeSuspected do (payload: tNodeSuspectedPayload) {
+    if (payload.suspectedNode in crashedNodes) {
+        detectedCrashes += (payload.suspectedNode);
+    }
+}
+```
+
+## CHECK 4: No Forbidden Keywords
+Spec monitors CANNOT use: `this`, `new`, `send`, `announce`, `receive`, `$`, `$$`, `pop`.
+These are illegal in monitors and will cause compilation errors.
+
+## CHECK 5: Payload Type Names Match Exactly
+All event handler parameter types must match the types declared in Enums_Types_Events.p exactly.
+
+## RESPONSE FORMAT
+
+Return your response in this exact format:
+
+<analysis>
+Brief description of what was wrong and how you fixed it.
+List each issue found as a bullet point.
+</analysis>
+
+<fixed_files>
+<Specification.p>
+... fixed spec code ...
+</Specification.p>
+</fixed_files>
+
+Use the ACTUAL filename of the spec file (e.g., Safety.p, Spec.p, Specification.p).
+Only include files that changed. If the spec is already correct, return it unchanged.

Src/PeasyAI/resources/instructions/review_spec_correctness.txt

@@ -0,0 +1,106 @@
+You are reviewing a P test driver file for correctness of machine wiring and initialization.
+
+You are given:
+1. The generated test driver code.
+2. All machine source files (showing each machine's constructor signature).
+3. The Enums_Types_Events.p file (showing all types and events).
+
+Your job is to check ONLY the following and return a FIXED version of the test driver:
+
+## CHECK 1: Dependency Order
+Every `new Machine(config)` call must happen AFTER all machines referenced in `config` have been created.
+
+BAD:
+```
+fd = new FailureDetector((nodes = nodeSet,));  // nodeSet is empty here!
+node1 = new Node((failureDetector = fd,));
+nodeSet += (node1);
+```
+
+GOOD:
+```
+node1 = new Node((failureDetector = fd,));
+nodeSet += (node1);
+fd = new FailureDetector((nodes = nodeSet,));  // nodeSet has node1
+```
+
+## CHECK 2: Circular Dependencies Must Be Resolved
+If Machine A's constructor needs Machine B, and Machine B's constructor needs Machine A, one side MUST use the init-event pattern to break the cycle.
+
+BAD (circular — impossible to satisfy both constructors):
+```
+fd = new FailureDetector((nodes = nodeSet,));  // needs nodes
+node1 = new Node((failureDetector = fd,));     // needs fd
+// But fd was created with empty nodeSet!
+```
+
+GOOD (break cycle with init-event):
+```
+// Create FD first with empty nodes (it will get them via registration)
+fd = new FailureDetector();
+// Create nodes with FD reference
+node1 = new Node((failureDetector = fd,));
+nodeSet += (node1);
+// Send nodes to FD via init event
+send fd, eFDInit, (nodes = nodeSet,);
+```
+
+ALTERNATIVE GOOD (if the machine supports it — create nodes first, then FD):
+```
+// If Node can be created without FD and configured later:
+node1 = new Node();
+nodeSet += (node1);
+fd = new FailureDetector((nodes = nodeSet,));
+send node1, eNodeInit, (failureDetector = fd,);
+```
+
+When resolving a circular dependency:
+- Look at which machine's constructor is SIMPLER (fewer fields, or has fields that are easier to provide later).
+- Break the cycle on that side by removing the problematic field from its constructor config type and adding an init event instead.
+- You MUST also update the machine's code to handle the init event if it doesn't already.
+- If the machine already handles an init event pattern (start state waits for a config event), use that.
+
+## CHECK 3: No Empty Collections Passed as Config
+If a machine's constructor expects `set[machine]` or `seq[machine]`, the collection MUST contain the actual machines, not be empty or default.
+
+BAD:
+```
+fdConfig = (nodes = default(set[machine]),);
+fd = new FailureDetector(fdConfig);
+```
+
+GOOD:
+```
+nodeSet += (node1);
+nodeSet += (node2);
+fd = new FailureDetector((nodes = nodeSet,));
+```
+
+## CHECK 4: Named Tuple Construction
+Every `new Machine(...)` and `send ..., eEvent, ...` must use named tuple syntax matching the type definition exactly.
+
+## RESPONSE FORMAT
+
+If the test driver is correct, return it unchanged.
+
+If there are issues, return the FIXED test driver code. If fixing requires changes to machine files (e.g., adding an init event handler), also return those changed files.
+
+Return your response in this exact format:
+
+<analysis>
+Brief description of what was wrong and how you fixed it.
+</analysis>
+
+<fixed_files>
+<TestDriver.p>
+... fixed test driver code ...
+</TestDriver.p>
+<Enums_Types_Events.p>
+... only if you needed to add new init events ...
+</Enums_Types_Events.p>
+<MachineName.p>
+... only if you needed to add init event handlers ...
+</MachineName.p>
+</fixed_files>
+
+Only include files that changed. If nothing changed, include only the original TestDriver.p.

Src/PeasyAI/resources/instructions/review_test_wiring.txt

@@ -11,8 +11,8 @@ event eTimeOut;
 event eDelayedTimeOut;
 
 machine Timer {
-  // user/client of the timer
   var client: machine;
+  var numDelays: int;
 
   start state Init {
     entry (_client : machine) {
@@ -22,18 +22,22 @@ machine Timer {
   }
 
   state WaitForTimerRequests {
-    on eStartTimer goto TimerStarted;
+    on eStartTimer goto TimerStarted with {
+      numDelays = 0;
+    };
 
     ignore eCancelTimer, eDelayedTimeOut;
   }
 
   state TimerStarted {
     entry {
-      // Only fire the timer with a chance of 1/10 to avoid livelocks
-      if(choose(10) == 0) {
+      // Bound the number of delays so the timer is guaranteed to
+      // eventually fire (required for liveness properties).
+      if (numDelays >= 3 || choose(10) == 0) {
         send client, eTimeOut;
         goto WaitForTimerRequests;
       } else {
+        numDelays = numDelays + 1;
         send this, eDelayedTimeOut;
       }
     }