A tool for solving the satisfiability and validity problems for modal fixpoint logics.
Version 1.4, Copyright (c) 2008-2017
It is developed and maintained by:
Install the OCaml Package Manager OPAM.
Then:
opam update
opam upgrade
opam switch 4.03.0
eval `opam config env`
opam install ocamlbuild ocamlfind ounit TCSLib extlib ocaml-sat-solvers minisat pgsolver
git clone https://github.com/tcsprojects/mlsolver.git
cd mlsolver
ocaml setup.ml -configure
ocaml setup.ml -build
You can verify that everything is working by calling:
bin/ltmcparitybuechi 3 | bin/mlsolver -stenv -val ltmc "#phi" -pgs recursive