sml-modelcheck

Symbolic CTL model checking over finite Kripke structures, in pure Standard ML. Sets of states and the transition relation are represented as reduced ordered binary decision diagrams using the vendored sml-bdd library: states are encoded in k Boolean present-state variables, the transition relation in present+next variables, and the temporal operators are computed by BDD pre-image (EX) and least/greatest fixpoints (EU, EG). The remaining operators are derived (EF, AX, AF, AG, AU).

For confidence, the library ships two independent checkers:

• satStates — the symbolic BDD engine;
• satStatesExplicit — an explicit-state reference checker over integer-set fixpoints.

They always agree (the test suite asserts it across many formulas).

No FFI, no threads, no clock, no randomness: the same inputs always produce the same outputs under MLton and Poly/ML.

API

structure ModelCheck : sig
  datatype ctl =
      AP of string | TrueC | FalseC
    | NotC of ctl | AndC of ctl * ctl | OrC of ctl * ctl
    | ImpC of ctl * ctl | IffC of ctl * ctl
    | EX of ctl | EF of ctl | EG of ctl
    | AX of ctl | AF of ctl | AG of ctl
    | EU of ctl * ctl | AU of ctl * ctl

  type kripke = {
    numStates : int,
    init      : int list,
    trans     : (int * int) list,
    labels    : (int * string list) list
  }
  exception Model of string

  val satStates         : kripke -> ctl -> int list   (* symbolic, BDD *)
  val models            : kripke -> ctl -> bool        (* all initial states satisfy *)
  val satStatesExplicit : kripke -> ctl -> int list    (* explicit reference *)
end

The transition relation is assumed total (every state has a successor), as usual for CTL.

Example

(* traffic light: 0=red -> 1=green -> 2=yellow -> 0 *)
val light : ModelCheck.kripke =
  { numStates = 3, init = [0]
  , trans = [(0,1),(1,2),(2,0)]
  , labels = [(0,["red"]),(1,["green"]),(2,["yellow"])] }

(* red is always eventually reachable *)
val true = ModelCheck.models light
             (ModelCheck.AG (ModelCheck.EF (ModelCheck.AP "red")))

Running examples/demo.sml with make example prints:

Traffic light (0=red -> 1=green -> 2=yellow -> 0), checked symbolically:

  red                    sat = {0}   models = true
  EX green               sat = {0}   models = true
  EF yellow              sat = {0,1,2}   models = true
  AG EF red              sat = {0,1,2}   models = true
  AG (green -> AX yellow) sat = {0,1,2}   models = true
  AG !(green & red)      sat = {0,1,2}   models = true

  (AG EF red: red is always reachable; the safety/liveness props hold.)

Build & test

Requires MLton and/or Poly/ML.

make test        # build + run the suite under MLton
make test-poly   # run the suite under Poly/ML
make all-tests   # both
make example     # build + run the demo
make clean

Installing with smlpkg

smlpkg add github.com/sjqtentacles/sml-modelcheck
smlpkg sync

sml-modelcheck vendors sml-bdd under lib/github.com/sjqtentacles/sml-bdd/ (a byte-identical copy of the upstream library). Reference lib/github.com/sjqtentacles/sml-modelcheck/modelcheck.mlb from your own .mlb (MLton / MLKit), or feed sources.mlb to tools/polybuild (Poly/ML).

Layout

sml.pkg                                       smlpkg manifest (requires sml-bdd)
Makefile                                      MLton + Poly/ML targets
.github/workflows/ci.yml                      CI: MLton + Poly/ML
lib/github.com/sjqtentacles/
  sml-modelcheck/  modelcheck.sig modelcheck.sml sources.mlb modelcheck.mlb
  sml-bdd/         vendored ROBDD library (byte-identical copy)
examples/
  demo.sml      symbolic CTL of a traffic light
test/
  harness.sml / test.sml                      35 reference checks
  entry.sml / main.sml
tools/polybuild                               Poly/ML build wrapper

Tests

35 deterministic checks: hand-computed CTL extensions over a 3-state structure (AP, EX, EF, EG, AG, AF, constants, models), a 4-state cycle exercising multi-bit state encoding (including AG AF for "infinitely often"), and an agreement battery asserting that the symbolic BDD checker and the explicit-state reference checker return identical state sets for many compound formulas (AX, AU, Iff, implication, and nested temporal operators). Run make all-tests to verify identical output under both compilers.

License

MIT. See LICENSE.