counterexample-to-test-generator

Counterexample To Test Generator

Overview

This skill transforms counterexample traces from model checkers into executable test cases that reliably reproduce property violations. It bridges formal verification and testing by mapping abstract states to concrete values and generating runnable tests with clear traceability from counterexample steps to test logic.

Workflow

Step 1: Analyze Inputs

Gather and understand the counterexample trace and program:

1. Identify the model checker format: Determine which tool produced the counterexample (SPIN, CBMC, NuSMV, TLA+, JPF, etc.). See references/model_checker_formats.md for format details.

2. Extract key information:

   • Initial state values
   • Sequence of transitions/steps
   • Variable values at each step
   • Property violation point
   • Error condition or assertion failure

3. Understand the program structure:

   • Entry points and function signatures
   • Input parameters and their types
   • State variables involved in the trace
   • Control flow relevant to the counterexample

Step 2: Map Abstract States to Concrete Values

Translate the counterexample's abstract representation into concrete test inputs:

1. Determine concrete values for abstract state variables:

   • Map symbolic values to concrete instances
   • Resolve non-deterministic choices to specific values
   • Handle ranges and constraints from the model

2. Identify input sequences:

   • Extract the sequence of function calls or operations
   • Determine parameter values for each call
   • Identify timing or ordering constraints

3. Handle environment assumptions:

   • External inputs or system calls
   • Concurrency or scheduling decisions
   • Resource states (files, network, memory)

Step 3: Generate Test Structure

Create the test case framework in the target language:

1. Choose test framework based on the program language:
   • C/C++: Google Test, CUnit, Check
   • Java: JUnit, TestNG
   • Python: pytest, unittest
   • C#: NUnit, xUnit