This is mc3 v0.1.0
, a prototype implementation of a
satisfiability-based modal mu calculus (MMC) model checking algorithm.
Directory | Contents |
---|---|
src | the prototype solver, written in Racket |
examples | example problems |
benchmarks | benchmark problems |
Print some info about mc3
’s command-line interface:
racket src/mc3.rkt --help
Run mc3
on one of the examples:
racket src/mc3.rkt examples/mmc-1.rkt
Compile the Racket code and run all the examples:
make all
N.B.: This project is developed on Linux, so these instructions may need to be adapted to other platforms.
The prototype solver is written in Racket; on Debian-like Linux distributions, run the following command:
apt install racket
Current development of mc3
uses
Racket v8.0.
Rosette is used for its interface to SAT/SMT solvers. Current
development of mc3
uses
Rosette 4.0, installed
from source.
git clone https://github.com/emina/rosette.git --branch 4.0
raco pkg install ./rosette
It includes a copy of the SMT solver
Z3, which is what mc3
uses.
brag
is used to parse NuSMV models and Büchi automata encoded in the
LBTT format.
raco pkg install brag
The graph
library is used to analyze the structure of MMC formulas.
raco pkg install graph
The associated visualizations depend on Graphviz.
apt install graphviz
Spot’s ltl2tgba
command-line tool is used to convert an LTL formula
(or, more generally, a “path subformula” that appears in a CTL*
formula) to a Büchi automaton as part of the translation from CTL* to
MMC.
NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.
mc3
can parse and analyze a subset of NuSMV models (refer to
src/parser/grammar/nusmv.rkt and
src/parser/nusmv.rkt). Follow the links on NuSMV’s website
to download a copy.
AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs).
The AIGER tools can be downloaded from
http://fmv.jku.at/aiger/aiger-1.9.9.tar.gz. Two of them in
particular — aigtoaig
and aigtosmv
— are used for processing
benchmark problems that are defined in the AIGER format (refer to
src/parser/aiger.rkt and benchmarks/Makefile).