Update PChatBot: improved design doc, RAG examples, checker fixers, and generation pipeline

Author: ankushdesai

Src/PChatBot/resources/context_files/modular/p_machines_guide.txt

@@ -20,29 +20,35 @@ Do NOT access functions contained inside of other machines.
 
 <machine_file_example>
 ```
-// Standalone functions (if needed)
-fun UtilityFunction(param: int): bool {
-  // Implementation
-  return param > 0;
-}
-
-// Machine definitions - no events/types/enums
+// Machine definitions - no events/types/enums (they come from Enums_Types_Events.p)
 machine TaskManager {
-  var tasks: seq[Task];  // Task type comes from context
-  
-  start state Idle {
-    on eStart goto Processing;  // eStart event comes from context
+  var workers: seq[machine];  // receive from constructor or config event
+  var tasks: seq[Task];       // Task type comes from context
+
+  // Start state receives configuration via constructor payload
+  start state Init {
+    entry InitEntry;
+    on eNewTask goto Processing;
   }
-  
+
   state Processing {
-    on eTask do HandleTask;     // eTask event comes from context
+    on eTask do HandleTask;
+    defer eNewTask;           // queue new tasks while busy
+    ignore eStatusRequest;    // drop status pings while processing
   }
-  
+
+  // Entry function receives the constructor payload
+  fun InitEntry(config: (workers: seq[machine],)) {
+    workers = config.workers;
+  }
+
   fun HandleTask(task: Task) {
     // Implementation using contextual types and events
   }
 }
 ```
+
+Created by test driver as: `new TaskManager((workers = workerList,));`
 </machine_file_example>
 
 <state_machine_grammar>

Src/PChatBot/resources/instructions/generate_machine.txt

@@ -15,4 +15,16 @@ For each function:
 5. EVERY event that can be received by this machine in a given state MUST be handled in that state. If an event is not relevant in a state, add `ignore eEventName;` to that state. If it should be processed later, add `defer eEventName;`. PChecker will flag unhandled events as bugs.
 6. Think about which events could arrive late or out-of-order. For example, if a machine transitions from PhaseA to PhaseB, events from PhaseA may still be in the queue — add `ignore` for those stale events in PhaseB.
 
-Before finalizing the implementation, identify all attributes and events that would be needed to properly setup and initialize this machine in test cases later. 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.
+## Initialization:
+If this machine has a start-state entry function with a parameter, that parameter carries the machine's constructor config (e.g., references to other machines, IDs, sizes). The implementation MUST:
+- Store every field from the config payload into the corresponding local variable.
+- Compute derived values (e.g., majoritySize = sizeof(acceptors) / 2 + 1).
+- If using the init-event pattern instead, the configuration handler function must similarly store all fields and then `goto` the first operational state.
+
+## 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).
+- All `send` targets are machine-typed variables (never null/default).
+- No events, types, or enums are declared in this file.
+
+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/PChatBot/resources/instructions/generate_machine_structure.txt

@@ -18,7 +18,75 @@ Write the structure of P code for the state machine {machineName}. Include all v
 5. Defer and ignore statements
 6. Function declarations with proper parameters and return types, but EMPTY bodies, do add COMMENTS for future stages of code generation.
 
+## CRITICAL: Machine Configuration / Initialization
 
+If this machine depends on references to other machines (e.g., a list of acceptors, a server reference, learner machines) or any configuration, it MUST receive them through one of these two patterns:
+
+### Pattern A — Constructor payload (preferred when all deps are known at creation time)
+
+The start state entry function receives configuration directly from the `new` call:
+
+```
+machine ExampleServer {{
+    var workers: seq[machine];
+    var serverId: int;
+
+    start state Init {{
+        entry InitEntry;       // receives config from new ExampleServer(config)
+        on eRequest goto Serving;
+    }}
+
+    fun InitEntry(config: (workers: seq[machine], id: int)) {{
+        workers = config.workers;
+        serverId = config.id;
+    }}
+    ...
+}}
+```
+Test driver creates it as: `new ExampleServer((workers = workerList, id = 1));`
+
+### Pattern B — Initialization event (when config arrives after creation)
+
+The machine blocks in its start state waiting for a configuration event, then transitions to its core logic:
+
+```
+machine ExampleWorker {{
+    var coordinator: machine;
+
+    start state WaitForConfig {{
+        on eWorkerConfig goto Ready with Configure;
+        defer eTask;     // defer work events until configured
+    }}
+
+    state Ready {{
+        on eTask do HandleTask;
+    }}
+
+    fun Configure(config: tWorkerConfig) {{
+        coordinator = config.coordinator;
+    }}
+    ...
+}}
+```
+Test driver creates and configures it as:
+```
+worker1 = new ExampleWorker();
+send worker1, eWorkerConfig, (coordinator = coord,);
+```
+
+### Rules
+- Pick ONE pattern per machine and be consistent.
+- Do NOT use ad-hoc event names like eStart or eInit that carry no typed payload. If using Pattern B, define a proper typed config event with a named-tuple payload in Enums_Types_Events.p.
+- If a machine has no external dependencies, its entry function can take no parameters.
+
+## Event Handling Completeness
+
+For EVERY state, think about which events could arrive in that state (including events from prior states still in the queue) and add:
+- `on eX do Handler;` — if the event should be processed
+- `defer eX;` — if the event should be queued for a later state
+- `ignore eX;` — if the event should be silently dropped
+
+PChecker will report an unhandled-event bug for any event that arrives in a state without a handler, defer, or ignore.
 
 The machine file should NOT contain:
 

Src/PChatBot/resources/instructions/generate_test_files.txt

@@ -1,43 +1,108 @@
 Write P code for the {filename} file.
 
 CRITICAL REQUIREMENTS:
+
 1. For EACH scenario in <possible_scenarios>, create a dedicated scenario machine (e.g., Scenario1_XXX) with a start state that instantiates the system.
 2. For EACH scenario machine, you MUST write a `test` declaration. Without test declarations, PChecker cannot discover or run any tests. The format is:
    test tcScenarioName [main=ScenarioMachine]:
      assert SpecName1, SpecName2 in
      {{ MachineA, MachineB, ..., ScenarioMachine }};
    Use the spec/monitor names from the PSpec files in the assert clause. List ALL machines that participate in the scenario inside the braces.
-3. Always create all dependent machines before initializing machines that will send events/messages to them; never use default/null machine references in initialization.
-4. The test driver file MUST contain BOTH the scenario machines AND the test declarations. Do NOT put them in separate files.
-5. Do NOT re-declare or re-define machines that already exist in PSrc (Broker, Producer, etc.). Only define NEW test-specific machines here (scenario drivers and test_component machines like Consumer if it was listed under <test_components>).
-6. You MUST only use events that are already defined in Enums_Types_Events.p. Do NOT invent new events (e.g., eStartProducing, eStartConsuming). If a machine needs to start doing work, trigger it via its constructor payload or entry action — not a custom start event.
-7. Scenario machines must be SIMPLE launchers. They create all system components in the correct order and then stop. They should NOT handle any protocol events (no `on eXxx` handlers). If a component like Timer needs a `client: machine` reference, pass the actual component that uses the timer (e.g., the Coordinator), NOT the scenario machine itself (`this`).
-8. Ensure every machine is fully initialized before other machines send events to it. Create machines in dependency order: infrastructure first (Timer), then core (Coordinator, Broker), then clients (Client, Producer, Consumer). Pass all required references via constructor payloads — do not leave machine references uninitialized.
+3. The test driver file MUST contain BOTH the scenario machines AND the test declarations. Do NOT put them in separate files.
+4. Do NOT re-declare or re-define machines that already exist in PSrc. Only define NEW scenario-driver machines here.
+5. You MUST only use events that are already defined in Enums_Types_Events.p. Do NOT invent new events.
+6. Scenario machines must be SIMPLE launchers. They create all system components in the correct order and then stop. They should NOT handle any protocol events (no `on eXxx` handlers).
 
-Example structure for a file with 2 scenarios:
+## CRITICAL: Machine Wiring — Read the Machine Entry Signatures
 
-machine Scenario1_SingleClient {{
-    start state Init {{
-        entry {{
-            // create system components
-        }}
-    }}
+Look at every machine file provided as context. Each machine's start state has an entry function. That entry function's parameter defines EXACTLY what the machine expects when created. You MUST match it.
+
+There are two initialization patterns used by the machines:
+
+### Pattern A: Constructor payload — machine expects config via `new Machine(payload)`
+If a machine's start-state entry function has a parameter, you MUST pass a matching named-tuple payload when creating it with `new`.
+
+Example — if Proposer.p has:
+```
+start state Init {{
+    entry InitEntry;
+    ...
+}}
+fun InitEntry(config: (acceptors: seq[machine], learners: seq[machine], id: int)) {{
+    ...
 }}
+```
+Then the test driver MUST create it as:
+```
+proposer = new Proposer((acceptors = acceptorSeq, learners = learnerSeq, id = 1));
+```
 
-machine Scenario2_MultipleClients {{
+### Pattern B: Initialization event — machine blocks on a config event
+If a machine's start state waits for an event (e.g., `on eAcceptorConfig goto Ready with Configure;`), you MUST send that event after creating the machine.
+
+Example — if Acceptor.p has:
+```
+start state WaitForConfig {{
+    on eAcceptorConfig goto Ready with Configure;
+    defer ePropose, eAcceptRequest;
+}}
+fun Configure(config: tAcceptorConfig) {{
+    ...
+}}
+```
+Then the test driver MUST do:
+```
+acceptor1 = new Acceptor();
+send acceptor1, eAcceptorConfig, (learners = learnerSeq,);
+```
+
+### Wiring Rules
+- Create machines in DEPENDENCY ORDER: machines with no dependencies first (e.g., Learner), then machines that reference them (e.g., Acceptor needs learners), then machines that reference those (e.g., Proposer needs acceptors).
+- Build `seq[machine]` or `set[machine]` collections BEFORE passing them to dependent machines.
+- NEVER leave machine-typed variables uninitialized (default/null). Every machine reference must point to a created machine.
+- NEVER pass `this` (the scenario machine) as a protocol participant reference.
+- For each `new` call, verify the payload tuple field names and types match the machine's entry function parameter EXACTLY.
+
+## Complete Example
+
+Given machines with these signatures:
+- Learner: `fun InitEntry()` — no config needed
+- Acceptor: `fun InitEntry(config: (learners: seq[machine],))` — needs learners
+- Proposer: `fun InitEntry(config: (acceptors: seq[machine], learners: seq[machine], id: int))` — needs acceptors + learners
+- Client: `fun InitEntry(config: (proposer: machine, value: int))` — needs proposer
+
+The scenario machine must be:
+```
+machine Scenario1_BasicPaxos {{
     start state Init {{
         entry {{
-            // create system components
+            var learner1: machine;
+            var acceptors: seq[machine];
+            var learners: seq[machine];
+            var proposer: machine;
+            var client: machine;
+
+            // 1. Create machines with no dependencies
+            learner1 = new Learner();
+            learners += (0, learner1);
+
+            // 2. Create machines that depend on step 1
+            acceptors += (0, new Acceptor((learners = learners,)));
+            acceptors += (1, new Acceptor((learners = learners,)));
+            acceptors += (2, new Acceptor((learners = learners,)));
+
+            // 3. Create machines that depend on steps 1-2
+            proposer = new Proposer((acceptors = acceptors, learners = learners, id = 1));
+
+            // 4. Create clients that depend on proposer
+            client = new Client((proposer = proposer, value = 42));
         }}
     }}
 }}
 
-test tcSingleClient [main=Scenario1_SingleClient]:
-    assert SafetySpec in
-    {{ ComponentA, ComponentB, Scenario1_SingleClient }};
-
-test tcMultipleClients [main=Scenario2_MultipleClients]:
-    assert SafetySpec in
-    {{ ComponentA, ComponentB, Scenario2_MultipleClients }};
+test tcBasicPaxos [main=Scenario1_BasicPaxos]:
+    assert OnlyOneValueChosen in
+    {{ Proposer, Acceptor, Learner, Client, Scenario1_BasicPaxos }};
+```
 
 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/PChatBot/resources/rag_examples/BestPractices_MachineWiring/PSrc/Coordinator.p

@@ -0,0 +1,66 @@
+// ============================================================================
+// BEST PRACTICES: Coordinator with Broadcast Pattern
+// ============================================================================
+//
+// Demonstrates:
+// 1. How to properly receive a component list via setup event
+// 2. How to broadcast to all components
+// 3. How to handle/ignore broadcast responses in all states
+// ============================================================================
+
+machine Coordinator {
+    var workers: seq[machine];
+    var allComponents: seq[machine];
+    var numWorkers: int;
+
+    start state Init {
+        entry InitEntry;
+        // BEST PRACTICE: Accept setup events in the start state.
+        // These arrive from the test driver after all machines are created.
+        on eSetupComponentList do HandleSetupComponents;
+        // BEST PRACTICE: Ignore protocol events that may arrive before setup.
+        ignore eResponse, eNotifyAll;
+    }
+
+    state Ready {
+        on eRequest do HandleRequest;
+        on eResponse do HandleResponse;
+        // BEST PRACTICE: When you broadcast eNotifyAll to all components,
+        // you might also be in the component list — handle or ignore your own broadcast.
+        ignore eNotifyAll;
+    }
+
+    state Done {
+        // BEST PRACTICE: Terminal states should ignore all events still in flight.
+        ignore eRequest, eResponse, eNotifyAll, eSetupComponentList;
+    }
+
+    fun InitEntry(config: tCoordinatorConfig) {
+        numWorkers = config.numWorkers;
+        // Don't goto Ready yet — wait for setup event with component list.
+    }
+
+    fun HandleSetupComponents(components: seq[machine]) {
+        allComponents = components;
+        goto Ready;
+    }
+
+    fun HandleRequest(req: (sender: machine, data: int)) {
+        // Process request and notify all components
+        BroadcastNotification(req.data);
+    }
+
+    fun HandleResponse(resp: (receiver: machine, result: int)) {
+        // Process response from worker
+    }
+
+    // BEST PRACTICE: Factor broadcast logic into a helper function.
+    fun BroadcastNotification(value: int) {
+        var i: int;
+        i = 0;
+        while (i < sizeof(allComponents)) {
+            send allComponents[i], eNotifyAll, (value = value);
+            i = i + 1;
+        }
+    }
+}

Src/PChatBot/resources/rag_examples/BestPractices_MachineWiring/PSrc/Types_Events.p

@@ -0,0 +1,34 @@
+// ============================================================================
+// BEST PRACTICES: Types, Events, and Setup Events
+// ============================================================================
+//
+// This file demonstrates best practices for defining types, events, and
+// setup/configuration events in P programs.
+//
+// KEY PRINCIPLES:
+// 1. Separate protocol events from setup events
+// 2. Use setup events for post-creation machine wiring
+// 3. Define clear payload types for each event
+// ============================================================================
+
+// --- Protocol events (used during normal operation) ---
+event eRequest: (sender: machine, data: int);
+event eResponse: (receiver: machine, result: int);
+event eNotifyAll: (value: int);
+
+// --- Setup/configuration events (used ONLY during initialization) ---
+// BEST PRACTICE: Define dedicated setup events for post-creation wiring.
+// NEVER reuse protocol events for setup purposes.
+//
+// Common patterns:
+// 1. Broadcast list setup:  event eSetupComponents: seq[machine]
+// 2. Back-reference setup:  event eSetupOwner: machine
+// 3. Peer list setup:       event eSetupPeers: seq[machine]
+// 4. Full config setup:     event eSetupConfig: tConfigType
+
+event eSetupComponentList: seq[machine];
+event eSetupCoordinatorRef: machine;
+
+// --- Configuration types ---
+type tWorkerConfig = (coordinator: machine, workerId: int);
+type tCoordinatorConfig = (numWorkers: int);