Verifying: fire verify

fire verify checks a project’s process-algebra model with the UPPAAL model checker. It emits a UPPAAL XTA model of the system (every PD’s processes as timed automata, channels as synchronisations), then runs verifyta and pretty-prints per-query PASS / FAIL results.

🚧 The verify subcommand lands with PR #174. On earlier versions the same behaviour is fic <PROJECT_DIR> --verify.

Usage

fire verify [PROJECT_DIR] [-q <QUERY_FILE>]

Writing queries

Queries are user-authored — which properties matter is application-dependent, so fic emits only the model and you state the properties. Write a UPPAAL query file named <name>.q next to your sources (it is part of the project, so commit it). The customary first line is deadlock-freedom:

/* the system never gets permanently stuck */
A[] not deadlock

/* the diode can complete a forward */
E<> dd.L1

Queries reference the process instance names from the emitted model (the PD names, snake_case) and template location names — inspect build/<name>.xml (or open it in the UPPAAL GUI) to find them.

What it does

1. Reads fire.toml and resolves the source directory.
2. Invokes fic <src> --emit=xta, writing build/<name>.xml (the UPPAAL model).
3. Locates the query file: the -q flag, or <src>/<name>.q. Errors if neither exists.
4. Locates verifyta — [verify] path → $VERIFYTA → PATH — and runs it with -t 0 (request a counterexample / witness trace), the model, the query file, and any [verify] args.
5. Parses the output and prints one PASS / FAIL line per query. Exits non-zero if any query fails.

Reading the output

$ fire verify demo/datadiode/
  ✓ Running verifyta: /opt/uppaal/bin/verifyta

  A[] not deadlock                          PASS
  E<> EthOuter.Handle_eth                   PASS
  ...

A failing query prints FAIL and, when verifyta produces one, the counterexample trace:

  A[] not deadlock                          FAIL
    Trace (12 steps):
      pd0.State0 → pd0.State1
      ...
      ↯ stuck at: pd0.State1, pd1.State2, ...

The ↯ stuck at line lists each automaton’s location in the deadlocked state — usually enough to spot the circular wait. A FAIL on a reachability query with (property unreachable — no counterexample trace) means the named location can never be entered.

Worked example: ping-pong

demo/pingpong/ ships two PDs (ping/pong) that bounce a bounded notification ROUNDS times over a genuinely cyclic channel (ping <-> pong), then go quiescent — a real case where WF2’s over-approximation would reject a topology that’s actually deadlock-free. Its hand-written pingpong.q states that, verified against the real emitted model (see tests/uppaal/pingpong/expected.xml for a known-good snapshot):

fire verify demo/pingpong/
#   A[] (deadlock imply ping.rounds == ROUNDS)   PASS
#   E<> ping.rounds == ROUNDS                    PASS
#   A[] ping.rounds <= ROUNDS                    PASS
#   E<> pong.L1                                  PASS

The first query is deadlock-freedom modulo intended termination: the only reachable quiescent state is the completed rally, so a blanket A[] not deadlock would itself report a false “deadlock” at the correct terminal state — see the header comment in demo/pingpong/pingpong.q for the full reasoning.

Ad-hoc queries

Pass a different query file for a one-off check — a per-invocation input, like a cargo test filter:

fire verify demo/datadiode -q queries/liveness.q

Relationship to the WF2 check

fic always runs WF2, a structural acyclicity check on the channel dependency graph, before emitting a deployable image. WF2 is an over-approximation: it rejects every cyclic topology, including systems that are deadlock-free under a fair scheduler (demo/pingpong’s ping <-> pong, for instance). When fire verify establishes deadlock-freedom, you can build such systems anyway with fic --allow-wf2-cycles — see the fic reference.