Model-Guided Code Repair
Overview
This skill enables automatic repair of code that violates temporal properties by analyzing model-checking counterexamples. It reasons about the root cause of violations at the model level, proposes minimal and semantically justified code modifications, and validates repairs through re-verification or test generation.
Repair Workflow
Follow this sequential process when repairing temporal property violations:
1. Analyze Input
Gather and understand three required inputs:
- Program source code: The code containing the violation
- Violated temporal property: The formal specification (LTL, CTL, or natural language description)
- Counterexample trace: The execution path demonstrating the violation
Read all inputs carefully. If the temporal property is in natural language, formalize it first.
2. Understand the Counterexample
Trace through the counterexample step-by-step:
- Identify the sequence of states and transitions
- Map counterexample states to program locations (line numbers, function calls)
- Identify variable values at each step
- Pinpoint the exact moment the property is violated
Output: A clear narrative of the execution path leading to the violation.
3. Identify Root Cause
Analyze why the violation occurs:
- Missing guards: Are conditions missing that should prevent certain transitions?
- Incorrect ordering: Are operations executed in the wrong sequence?
- Race conditions: Are there synchronization issues in concurrent code?
- Missing state updates: Are variables not being updated correctly?
- Incorrect logic: Are conditional expressions wrong?
Output: A precise diagnosis of the model-level cause.
4. Propose Repair Strategy
Design a minimal repair that:
- Directly addresses the root cause
- Preserves intended program behavior
- Minimizes code changes
- Maintains code readability
Common repair strategies:
- Add guards: Insert conditional checks to prevent invalid transitions
- Reorder operations: Adjust execution sequence to satisfy temporal ordering
- Add synchronization: Insert locks, semaphores, or barriers for concurrent code
- Update state management: Fix variable assignments or state transitions
- Strengthen preconditions: Add assertions or input validation
Output: A clear repair plan with justification.
5. Generate Repaired Code
Implement the repair:
- Make minimal, targeted changes to the source code
- Clearly mark what was changed (comments or annotations)
- Ensure the repair is syntactically correct
- Preserve existing code style and conventions
Output: Modified source code with changes clearly indicated.
6. Validate the Repair
Verify that the repair resolves the violation:
Option A: Re-run Model Checker
- Execute the model checker on the repaired code
- Verify the temporal property now holds
- Check that no new violations were introduced
Option B: Generate and Run Tests
- Create test cases based on the counterexample
- Generate additional tests for edge cases
- Execute tests and verify they pass
- Ensure existing tests still pass (regression testing)
Output: Validation results showing the property is satisfied.
7. Document the Repair
Provide a comprehensive explanation:
- Root cause: What caused the violation
- Repair strategy: Why this approach was chosen
- Minimality justification: Why this is the smallest necessary change
- Behavior preservation: How intended functionality is maintained
- Validation results: Evidence that the repair works
Output Format
Structure the final output as follows:
## Repaired Code [Modified source code with changes clearly marked] ## Changes Made - [Line X]: [Description of change] - [Line Y]: [Description of change] ## Root Cause Analysis [Explanation of what caused the violation] ## Repair Strategy [Why this repair approach was chosen] [Why it is minimal and semantically justified] ## Behavior Preservation [How the repair maintains intended program behavior] ## Validation Results [Model checking results OR test execution results] [Confirmation that the property now holds]
Common Scenarios
Safety Property Violations
Example: "The system must never enter an error state"
- Look for missing error checks or exception handling
- Add guards to prevent invalid state transitions
- Validate with assertions or model checking
Liveness Property Violations
Example: "Every request must eventually be processed"
- Look for deadlocks, infinite loops, or missing progress conditions
- Add fairness constraints or progress guarantees
- Validate with liveness checking or timeout tests
Synchronization Issues
Example: "Shared resources must be accessed atomically"
- Look for race conditions or missing locks
- Add synchronization primitives (mutexes, semaphores)
- Validate with concurrency testing or model checking
State Machine Violations
Example: "State transitions must follow the specified protocol"
- Look for missing state checks or incorrect transition logic
- Add state validation or fix transition conditions
- Validate with state machine verification
Tips for Effective Repairs
- Start simple: Try the minimal fix first before complex refactoring
- Preserve structure: Maintain the original code architecture when possible
- Consider side effects: Ensure repairs don't break other properties
- Document assumptions: Note any assumptions made during repair
- Test thoroughly: Validate beyond just the violated property
- Iterate if needed: If the first repair doesn't work, analyze why and adjust
Integration with Model Checkers
This skill works with various model checking tools:
- SPIN: For Promela models and LTL properties
- NuSMV/nuXmv: For SMV models and CTL/LTL properties
- CBMC: For C programs with assertions
- Java PathFinder: For Java programs
- TLA+: For TLA+ specifications
When counterexamples are provided in tool-specific formats, translate them into a clear execution trace before analysis.
