Fix str.format() KeyError in instruction templates and improve error handling

The generate_machine tool was failing silently with an opaque ' ' error
because P code examples in instruction templates contained unescaped curly
braces that collided with Python's str.format(). Added _safe_format()
helpers that fall back to manual substitution when str.format() raises
KeyError/ValueError. Also improved all exception handlers across the
service layer (generation, compilation, fixer) to include the exception
type name and full traceback in logs, preventing opaque error messages.

Includes design doc migration from .txt to .md, post-processor
enhancements, validation updates, and a verified BasicPaxos tutorial
generated end-to-end via the MCP tools.

Co-authored-by: Cursor <cursoragent@cursor.com>

Author: ankushdesai

Src/PeasyAI/.cursorrules

@@ -1,213 +0,0 @@
-# P Language Programming Rules for Cursor
-
-## About P
-
-P is a state machine-based language for modeling and verifying concurrent systems. It compiles to C# and can be model-checked using PChecker to find concurrency bugs.
-
-## Project Structure
-
-P projects follow this structure:
-```
-ProjectName/
-├── ProjectName.pproj     # Project configuration (XML)
-├── PSrc/                  # Source files (state machines, types, events)
-│   ├── Enums_Types_Events.p
-│   └── MachineName.p
-├── PSpec/                 # Specification monitors
-│   └── SafetyMonitor.p
-└── PTst/                  # Test files
-    └── TestDriver.p
-```
-
-## Reserved Keywords
-
-DO NOT use these as identifiers:
-```
-var, type, enum, event, on, do, goto, data, send, announce, receive, case, raise, 
-machine, state, hot, cold, start, spec, module, test, main, fun, observes, entry, 
-exit, with, union, foreach, else, while, return, break, continue, ignore, defer, 
-assert, print, new, sizeof, keys, values, choose, format, if, halt, this, as, to, 
-in, default, Interface, true, false, int, bool, float, string, seq, map, set, any
-```
-
-## Essential Syntax Patterns
-
-### State Machine Declaration
-```p
-machine MachineName {
-    var localVar: int;
-    
-    start state Init {
-        entry {
-            // initialization code
-        }
-        
-        on eEvent do (payload: PayloadType) {
-            // handle event
-        }
-        
-        on eTrigger goto NextState;
-    }
-    
-    state NextState {
-        entry { ... }
-        exit { ... }
-    }
-}
-```
-
-### Event Declarations
-```p
-event eSimpleEvent;                           // No payload
-event ePayloadEvent: PayloadType;            // With payload
-```
-
-### Type Declarations
-```p
-type TRecord = (field1: int, field2: string);
-type TChoice = data | null;
-enum EnumName { Value1, Value2, Value3 }
-```
-
-### Sending Events
-```p
-send targetMachine, eEvent, payload;  // Send to specific machine
-announce eEvent, payload;              // Broadcast to monitors
-raise eEvent, payload;                 // Raise to self
-```
-
-## Common Mistakes to Avoid
-
-### 1. Variable Initialization
-```p
-// WRONG - No inline initialization
-var x: int = 0;
-
-// CORRECT - Separate declaration and assignment
-var x: int;
-x = 0;
-```
-
-### 2. Event Payload Access
-```p
-// WRONG - receive() is not valid
-var data = receive(eEvent);
-
-// CORRECT - Use handler parameters
-on eEvent do (payload: PayloadType) {
-    // use payload directly
-}
-```
-
-### 3. Sequence Operations
-```p
-var mySeq: seq[int];
-
-// WRONG
-mySeq += (value);
-
-// CORRECT - Use index-value pair
-mySeq += (sizeof(mySeq), value);
-```
-
-### 4. Set Operations
-```p
-var mySet: set[int];
-
-// CORRECT
-mySet += (value);
-mySet -= (value);
-```
-
-### 5. Map Operations
-```p
-var myMap: map[string, int];
-
-// Add/Update
-myMap[key] = value;
-
-// Check existence before access
-if (key in myMap) {
-    var v = myMap[key];
-}
-```
-
-## Compilation Commands
-
-```bash
-# Compile P project
-p compile
-
-# Run PChecker
-p check -tc TestCaseName
-```
-
-## MCP Tools Available
-
-When working with P code, you have two approaches for project generation:
-
-### Recommended: Step-by-Step Generation (use this by default)
-
-Generate files one at a time so the user can review and approve each before proceeding. This produces higher quality results because errors are caught early and the user stays in control.
-
-1. **generate_project_structure** - STEP 1: Create project skeleton (PSrc, PSpec, PTst, .pproj)
-2. **generate_types_events** - STEP 2: Generate Enums_Types_Events.p (preview, then save with save_p_file)
-3. **generate_machine** - STEP 3: Generate each state machine one at a time (preview, then save with save_p_file). Pass previously saved files as context_files.
-4. **generate_spec** - STEP 4: Generate safety specification (preview, then save with save_p_file)
-5. **generate_test** - STEP 5: Generate test driver (preview, then save with save_p_file)
-6. **p_compile** - STEP 6: Compile the project
-7. **fix_compiler_error** / **fix_iteratively** - Fix any compilation errors
-8. **p_check** - STEP 7: Run PChecker verification
-9. **fix_checker_error** / **fix_buggy_program** - Fix any PChecker errors
-
-### One-Shot: Complete Project Generation (only when explicitly requested)
-
-Use **generate_complete_project** ONLY when the user explicitly asks for fully automated, one-shot, or hands-off generation. This runs all steps without human review.
-
-### Other Useful Tools
-
-- **save_p_file** - Save previewed code to disk after user approves
-- **syntax_helper** - Get P language syntax help
-- **search_p_examples** - Find similar P code examples
-- **list_project_files** / **read_p_file** - Inspect existing P projects
-
-## Human-in-the-Loop Guidance
-
-When fixing errors, the tools will attempt up to 3 automated fixes. If all attempts fail:
-
-1. The tool returns `needs_guidance: true`
-2. You will see an `error_summary` and `suggested_questions`
-3. Ask the user for guidance based on the questions
-4. Call the fix tool again with the `user_guidance` parameter
-
-Example flow:
-```
-Tool returns: {
-    "needs_guidance": true,
-    "error_summary": "Cannot resolve type 'TData'",
-    "suggested_questions": ["What type should TData be?"]
-}
-
-Ask user: "I've tried 3 fixes but the error persists. What type should TData be?"
-User: "TData should be (x: int, y: int)"
-Call: fix_compiler_error(..., user_guidance="TData should be (x: int, y: int)")
-```
-
-## Best Practices
-
-1. **Start with types and events** - Define all shared types in Enums_Types_Events.p first
-2. **One machine per file** - Keep each state machine in its own file
-3. **Use descriptive names** - Events should start with 'e', e.g., `eRequestData`
-4. **Add specs early** - Write specification monitors alongside implementation
-5. **Test incrementally** - Compile after each machine, don't wait until the end
-6. **Keep states focused** - Each state should have a clear purpose
-
-## Resources
-
-Use these MCP resources for reference:
-- `p://guides/syntax` - Complete syntax reference
-- `p://guides/machines` - State machine patterns
-- `p://guides/types` - Type system guide
-- `p://guides/events` - Event handling
-- `p://guides/specs` - Specification monitors
-- `p://examples/fewshot` - Code examples

Src/PeasyAI/docs/DESIGN_DOCUMENT.md

@@ -630,8 +630,8 @@ class GenerateProjectInput(BaseModel):
 
     design_doc: str = Field(
         ...,
-        description="The design document describing the P program. Should include "
-                    "<title>, <introduction>, <components>, and <interactions> sections."
+        description="The design document describing the P program in markdown format. Should include "
+                    "headings: # Title, ## Introduction, ## Components, and ## Interactions."
     )
 
     output_dir: str = Field(
@@ -685,11 +685,11 @@ This tool will:
 5. Generate test drivers (if enabled)
 6. Compile and validate the project
 
-The design document should include:
-- <title>: Project name
-- <introduction>: System description
-- <components>: List of machines/components
-- <interactions>: Events and communication patterns
+The design document should be in markdown format with these headings:
+- `# Title`: Project name
+- `## Introduction`: System description
+- `## Components`: List of machines/components
+- `## Interactions`: Events and communication patterns
 """
     )
     def generate_project(params: GenerateProjectInput) -> GenerateProjectOutput:

Src/PeasyAI/pyproject.toml

@@ -50,7 +50,7 @@ Documentation = "https://p-org.github.io/P/"
 # ---------------------------------------------------------------------------
 [tool.hatch.build.targets.wheel]
 # The installable Python code lives under src/
-packages = ["src/core", "src/ui"]
+packages = ["src/core", "src/ui", "src/utils"]
 
 [tool.hatch.build.targets.wheel.sources]
 # Map src/core → core, src/ui → ui so import paths stay the same

Src/PeasyAI/resources/instructions/generate_design_doc.txt

@@ -1,9 +1,8 @@
-Please generate a design document for the provided P code.
+Please generate a design document in markdown format for the provided P code.
 Here are the instructions on the content that must be included in each section of the design document:
-1. Title: the title of the system modeled in the given P code
-2. Overview: Brief overview of the system described in the P code
-3. Components: For each component or actor in the system, include a brief description of what the component represents and a bulleted list of actions performed by the component
-4. Interactions: For each messages/event being passed between different components/machines, include a description of the interaction, a bulleted list of the Source and Target components, payload, all possible effects of this interaction 
-5. Global Specifications: For each specification, include a bulleted list of correctness properties being checked and assertions made to check these properties
-6. Possible Scenarios: Include a bulleted list of all the possible scenarios of component/actor behaviour that could occur within the system
-7. Enclose the design document content in <design_document></design_document> tags
+1. Title: Use a top-level markdown heading (`# Title`) with the title of the system modeled in the given P code
+2. Introduction (`## Introduction`): Brief overview of the system described in the P code, followed by a numbered list of assumptions
+3. Components (`## Components`): Split into `### Source Components` and `### Test Components`. For each component or actor, include a brief description of what the component represents, its states, local state (variable names with plain English descriptions, no types), initialization (described in plain English — what information the machine needs to start and how it receives it, without code or type annotations), and a bulleted list of behaviors
+4. Interactions (`## Interactions`): For each event being passed between components/machines, include a numbered entry with Source, Target, Payload (described in plain English, no code or type annotations), Description, and Effects
+5. Specifications (`## Specifications`): For each specification, include the property name, whether it is a safety or liveness property, and a precise English statement that naturally references the relevant events by name
+6. Test Scenarios (`## Test Scenarios`): Include a numbered list of concrete test scenarios with specific machine counts and expected outcomes

Src/PeasyAI/resources/instructions/generate_enums_types_events.txt

@@ -1 +1,26 @@
-Write the enums, types, and events required for each of the state machines. If multiple state machines need the same enums, types, and event, write them only once. Do not write duplicate declarations. Return only the generated P code without any explanation attached. Return the P code enclosed in <Enums_Types_Events.p></Enums_Types_Events.p>.
+Write the enums, types, and events required for each of the state machines. If multiple state machines need the same enums, types, and events, write them only once. Do not write duplicate declarations.
+
+## CRITICAL SYNTAX RULES:
+
+1. **Type definitions do NOT use trailing commas**, even for single-field named tuples:
+   ```
+   type tLearnPayload = (learnedValue: int);              // CORRECT
+   type tAcceptorConfig = (learners: seq[machine]);        // CORRECT
+   type tProposePayload = (proposer: machine, num: int);   // CORRECT
+   ```
+   Note: Trailing commas are only used in VALUE expressions like `(field = value,)`, never in type definitions.
+
+2. **Use descriptive, unambiguous field names.** Each type's field names will be used throughout the codebase in payload construction and field access. Choose names that are specific to the type:
+   - GOOD: `(proposalNumber: int, acceptedValue: int)` — clear what each field means
+   - BAD: `(value: int)` — ambiguous, easily confused across types
+
+3. **Config types** for machine initialization should match the machine's dependencies exactly. Name them `t<MachineName>Config`:
+   ```
+   type tProposerConfig = (acceptors: seq[machine], learners: seq[machine], proposerId: int);
+   type tAcceptorConfig = (learners: seq[machine]);
+   type tLearnerConfig = (majoritySize: int);
+   ```
+
+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)`.
+
+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_machine.txt

@@ -5,7 +5,7 @@ IMPLEMENTATION INSTRUCTIONS:
 For each function:
 1. Implement the body according to the intended behavior
 2. Use proper P statements and expressions (conditionals, loops, send statements, etc.)
-3. Ensure the implementation aligns with the components in <components></components> tags and interactions in <interactions></interactions> tags
+3. Ensure the implementation aligns with the "Components" and "Interactions" sections of the design document
 
 ## Key Rules:
 1. Never use `=` in variable declarations
@@ -29,11 +29,20 @@ Named-tuple types use ``(field = value, ...)`` syntax. Always include ALL fields
   CORRECT single-field: send target, eMsg, (reqId = 42,);  // trailing comma required!
   WRONG single-field:   send target, eMsg, (reqId = 42);   // missing trailing comma → PARSE ERROR
 
+## CRITICAL — Use Exact Type and Field Names from Enums_Types_Events.p:
+When the Enums_Types_Events.p file is provided as context, you MUST use the EXACT type names and field names defined there. Do NOT invent alternative names.
+  Given: type tPromisePayload = (proposer: machine, highestProposalSeen: int, acceptedValue: int);
+  CORRECT: fun HandlePromise(msg: tPromisePayload) {{ ... msg.highestProposalSeen ... msg.acceptedValue ... }}
+  WRONG:   fun HandlePromise(msg: tPromise) {{ ... msg.propNum ... msg.value ... }}
+The function parameter type annotation MUST match the event's payload type exactly as declared.
+
 ## 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.
-- Single-field named tuples ALWAYS have a trailing comma: ``(field = value,)``.
+- 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.
 
 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_structure.txt

@@ -9,7 +9,7 @@ P supports specifying and checking both safety as well as liveness specification
 You are an expert programming assistant designed to write P programs for the given complex distributed systems. Avoid overreliance on general programming knowledge and strictly adhere to P's specific requirements. Thoroughly review the P language syntax guide before writing code. Refer the provided context files for the correct syntax while writing.
 
 
-Write the structure of P code for the state machine {machineName}. Include all variable declarations, state declarations, event handlers, and function declarations, BUT leave all function bodies empty (with just placeholder comments). Ensure that the components in <components></components> tags and the interactions in <interactions></interactions> tags are reflected in the structure. The structure should include:
+Write the structure of P code for the state machine {machineName}. Include all variable declarations, state declarations, event handlers, and function declarations, BUT leave all function bodies empty (with just placeholder comments). Ensure that the "Components" and "Interactions" sections of the design document are reflected in the structure. The structure should include:
 
 1. Machine declaration with local variable declarations
 2. All states with their annotations (start, hot, cold)
@@ -88,6 +88,12 @@ For EVERY state, think about which events could arrive in that state (including
 
 PChecker will report an unhandled-event bug for any event that arrives in a state without a handler, defer, or ignore.
 
+## CRITICAL — Use Exact Type Names from Enums_Types_Events.p:
+When the Enums_Types_Events.p file is provided as context, you MUST use the EXACT type names defined there for function parameter annotations and event handler signatures. Do NOT invent alternative names.
+  Given: event ePromise: tPromisePayload;
+  CORRECT: on ePromise do HandlePromise;  ...  fun HandlePromise(msg: tPromisePayload) {{ ... }}
+  WRONG:   on ePromise do HandlePromise;  ...  fun HandlePromise(msg: tPromise) {{ ... }}
+
 The machine file should NOT contain:
 
 1. Specification monitors (spec keyword)

Src/PeasyAI/resources/instructions/generate_spec_files.txt

@@ -1,11 +1,11 @@
-Write P code for the {filename} file. Ensure that the specifications specified in <global_specifications></global_specifications> tags are implemented.
+Write P code for the {filename} file. Ensure that the specifications described in the "Specifications" section of the design document are implemented.
 
 CRITICAL RULES FOR SPEC MONITORS:
 1. Spec monitors are declared with `spec SpecName observes event1, event2 {{ ... }}`.
 2. Spec monitors CANNOT use: `this`, `new`, `send`, `announce`, `receive`, `$`, `$$`, `pop`. These are ILLEGAL in monitors and will cause compilation errors.
 3. Monitors can ONLY observe events and maintain internal state (variables, maps, sets). They assert properties based on observed event payloads.
 4. If you need to track per-machine state (e.g., per-consumer offsets), use a `map[machine, ...]` keyed by the machine reference from the event payload — NOT `this`.
-5. Each safety property from <global_specifications> should be a separate `spec` declaration.
+5. Each safety property from the "Specifications" section should be a separate `spec` declaration.
 6. Every spec monitor MUST contain at least one `assert` statement. A spec that observes events but never asserts anything is useless — PChecker will not detect any bugs. If the property is "X must never happen", assert the negation: `assert !badCondition, "X happened";`.
 7. NEVER generate empty functions or functions with only comments. If an event handler doesn't need logic, simply don't observe that event.
 8. Only observe events that are actually defined in the Enums_Types_Events.p file. Do NOT observe events that don't exist.
@@ -33,4 +33,10 @@ spec MutualExclusion observes eLockGranted, eLockReleased {{
 
 Note: The spec uses event payloads to track state, asserts on every relevant transition, and never uses `this`/`send`/`new`.
 
+## CRITICAL — Use Exact Type and Field Names from Enums_Types_Events.p:
+When the Enums_Types_Events.p file is provided as context, you MUST use the EXACT type names and field names defined there. Do NOT invent alternative names.
+  Given: event eAccepted: tAcceptedPayload;  and  type tAcceptedPayload = (proposalNumber: int, acceptedValue: int);
+  CORRECT: on eAccepted do (payload: tAcceptedPayload) {{ ... payload.acceptedValue ... }}
+  WRONG:   on eAccepted do (payload: tAccepted) {{ ... payload.value ... }}
+
 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.