Explanator: Send in the Explanator—it explains satisfaction/violation of LTL formulas on lasso words

    Bhargav Bhatt and Dmitriy Traytel
Department of Computer Science, ETH Zurich, Switzerland

This library is distributed under the terms of the GNU Lesser General Public License version 3. See files LICENSE and COPYING.

Explanator depends on a recent (>= 4.04.0) version of the OCaml compiler.

To install ocaml and some additional libraries use opam - ocaml's package manager. For example:

apt-get install opam
opam switch 4.05.0
eval $(opam config env)
opam install safa menhir

then compile Explanator with

make

to obtain a binary explanator.native file and

./explanator.native -fmla examples/ex1.ltl -log examples/ex1.log

to run an example.

./explanator.native -?

provides some additional hints about the tool's user interface.