To execute the project on your local machine, follow the instructions below.
We recommend that you install a recent verion of the OCaml compiler (>= 4.11) and necessary dependencies with opam.
In particular, if you are a Debian/Ubuntu user
# apt-get install opam libgmp-dev
and then
$ opam init -y
$ opam switch create 4.13.1
$ eval $(opam env --switch=4.13.1)
$ opam install dune core_kernel base zarith menhir js_of_ocaml js_of_ocaml-ppx \
zarith_stubs_js dune-build-info qcheck
should be enough.
From the root folder, you can compile the code with
$ dune build
to obtain the executable whyenf.exe inside the folder bin. Moreover, you can run one of our predefined examples with
$ ./bin/whyenf.exe -sig examples/enforcement/paper/case_study/arfelt.sig -formula examples/enforcement/paper/case_study/formulae_whyenf/arfelt_2_limitation.mfotl -log examples/enforcement/paper/case_study/arfelt.log
You can remove the binary and clean the working directory with
$ dune clean
This project is licensed under the GNU Lesser GPL-3.0 license - see LICENSE for details.