CtrlK
BlogDocsLog inGet started
Tessl Logo

smv-model-extractor

Extracts an SMV (NuSMV/nuXmv) finite-state model from code or state-machine descriptions, for CTL/LTL model checking of reactive systems. Use when verifying hardware-adjacent or embedded logic, when the state space is naturally finite and small, or when CTL branching-time properties are needed.

71

Quality

86%

Does it follow best practices?

Run evals on this skill

Adds up to 20 points to the overall score

View guide

SecuritybySnyk

Passed

No findings from the security scan

SKILL.md
Quality
Evals
Security

SMV Model Extractor

SMV is for small, finite, synchronous systems — think hardware controllers, protocol handshakes, embedded state machines. Compared to → program-to-tlaplus-spec-generator: SMV is synchronous (all transitions fire together) and finite by construction; TLA+ is asynchronous and handles unbounded state.

When SMV over TLA+

CharacteristicSMV fitsTLA+ fits
State spaceNaturally finite (< 10⁸ states ideally)Can be unbounded (abstracted)
Execution modelSynchronous — all modules step togetherAsynchronous interleaving
Property languageCTL (branching) + LTLTLA (linear, actions)
Source domainHardware, embedded, protocol handshakesDistributed systems, concurrency

The SMV shape

MODULE main
VAR
  state : {idle, waiting, active, error};
  counter : 0..15;
  input : boolean;

ASSIGN
  init(state) := idle;
  next(state) := case
    state = idle & input      : waiting;
    state = waiting & counter = 0 : active;
    state = active & !input   : idle;
    TRUE                      : state;      -- stutter
  esac;

  init(counter) := 0;
  next(counter) := case
    state = waiting & counter > 0 : counter - 1;
    TRUE : counter;
  esac;

SPEC AG (state = error -> AF state = idle)   -- CTL: always recoverable

Extraction from code

Code patternSMV construct
enum State { A, B, C }state : {A, B, C}
switch(state) { case A: ... }next(state) := case state = A : ...; esac
Bounded int (uint4_t, i % 16)x : 0..15
Bool flagflag : boolean
if (cond) state = XOne branch in the case
Parallel componentsSeparate MODULEs, instantiated in main
Shared variable between componentsPassed as parameter: MODULE foo(shared_var)

Worked example

Code (traffic light controller):

enum { RED, GREEN, YELLOW } light = RED;
int timer = 0;

void tick(bool car_waiting) {
    switch (light) {
    case RED:
        if (timer >= 30 && car_waiting) { light = GREEN; timer = 0; }
        else timer++;
        break;
    case GREEN:
        if (timer >= 25) { light = YELLOW; timer = 0; }
        else timer++;
        break;
    case YELLOW:
        if (timer >= 5) { light = RED; timer = 0; }
        else timer++;
        break;
    }
}

SMV:

MODULE main
VAR
  light : {RED, GREEN, YELLOW};
  timer : 0..31;
  car_waiting : boolean;         -- environment input, unconstrained

ASSIGN
  init(light) := RED;
  init(timer) := 0;

  next(light) := case
    light = RED    & timer >= 30 & car_waiting : GREEN;
    light = GREEN  & timer >= 25               : YELLOW;
    light = YELLOW & timer >= 5                : RED;
    TRUE : light;
  esac;

  next(timer) := case
    next(light) != light : 0;            -- reset on transition
    timer < 31           : timer + 1;
    TRUE                 : timer;        -- saturate
  esac;

-- Safety: never GREEN and YELLOW simultaneously (trivially true here — single var)
-- Liveness: if a car waits, eventually GREEN
LTLSPEC G (car_waiting -> F light = GREEN)

timer capped at 31 — SMV needs finite ranges. The saturation at 31 is a modeling choice; check it doesn't affect the property (here it doesn't — thresholds are all ≤ 30).

Check: LTLSPEC fails if car_waiting can oscillate — a car that waits then leaves then waits again resets no clock. The fix is in the property (G car_waiting -> F GREEN — persistent waiting) or a fairness assumption.

Bounding the infinite

SMV requires finite domains. When the code has unbounded state:

Unbounded constructBounding strategy
Counter that grows foreverCap at max(threshold) + 1 — values above the highest comparison are equivalent
Message queueBound length. If property violated → was it at the bound? Raise the bound.
Arbitrary data payloadAbstract to a few symbolic values. data : {d1, d2} — if it doesn't affect control, one value suffices.

If you can't sensibly bound it, SMV is the wrong tool — use TLA+ with a state constraint, or go parametric.

Do not

  • Do not model a naturally asynchronous system as synchronous. If processes step independently, SMV's lockstep will hide interleavings. Use TLA+.
  • Do not forget the TRUE : state stutter branch. Without it, case is partial → "incomplete case" or arbitrary next value.
  • Do not leave environment inputs unconstrained without thinking. car_waiting : boolean with no constraint means it can toggle every tick — that's maximum chaos, often too adversarial.
  • Do not use a range larger than you need. 0..1000000 → NuSMV allocates log₂(10⁶) ≈ 20 bits per state. Blowup is exponential in bits.

Output format

## Finite-state abstraction
<var> : <range> — <what code construct, how bounded>

## SMV model
<code block>

## Properties
<CTL/LTL specs — each traced to a requirement>

## Bounding assumptions
<every cap you imposed, and why it's sound for this property>
Repository
santosomar/general-secure-coding-agent-skills
Path

skills/verification/smv-model-extractor/SKILL.md

Commit

47d56bb

Last updated
First committed

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.

Claim skill