Docs

Coverage

See what your checks exercised and where to improve the model or workload.

snappea check reports coverage for each test and for the selected tests together. snappea observe measures the monitors exercised by your application events. A passing check and high coverage are useful evidence; neither establishes that every requirement is modeled or that the model matches your application.

What is measured

Type	Question it answers
Statements	Which executable statements ran? Locations are reported as source lines.
Branches	Did each `if` take both its true and false paths, including an empty else?
Condition outcomes	Did each atomic condition in an `if` or `while` evaluate both true and false? Short-circuited operands count only when evaluated.
Event handlers	Did each state's `do` or `goto` handler run?
Transition pairs	Did each structural path `A → B → C` occur on one instance in one execution?
Scenarios	Did a named behavioral target reach its accepting state? Unwitnessed scenarios remain coverage gaps.

Condition coverage distinguishes operands inside decisions such as ready && authorized. Both branch outcomes can occur while authorized is always true when evaluated. This measures operand outcomes, not whether each operand independently changes the decision (MC/DC). Literal Boolean constants and assertion conditions are excluded from condition targets.

Transition-pair targets come from declared transitions and gotos in actions and called helpers. Guards and data constraints can make a structural pair unreachable. Covering two edges in separate executions does not cover their pair. Other actors may run between the two transitions.

Use the gaps

snappea check
snappea check tcRecovery --json-report coverage.json

Uncovered locations identify missing driver actions, inputs, or event orderings worth investigating. Components loaded from source but outside the selected tests are listed separately and excluded from the totals. They may belong to another test or be checked only through application events. Code beginning with assert false is also excluded because it must never run.

Counts combine hits across executions; they do not describe one complete execution. A bug stops a test early and marks its coverage partial. An incomplete search can miss reachable targets; uncovered does not mean impossible. JSON includes the full gap list and the separate conditions, transition_pairs, and excluded_components fields.

Behavior needs a target

Full structural coverage can still miss two clients competing for the same resource, or a retry reusing a request ID after restart. Express those relationships as scenarios, observing the relevant identities and events. A scenario recognizes a challenging situation; a spec checks that the system handles it correctly. Reaching a cold state after an observed event satisfies a scenario.

Mutation testing complements coverage by changing behavior and asking whether checks reject it. It measures sensitivity to those changes, rather than adding a reachability guarantee. Missing requirements and inaccurate application instrumentation still need review.

See the command line guide, checking reference, and application-event coverage and merging.