A tool using OCaml to check whether a monitor is symbolically controllable.
These instructions will get you a copy of the project up and running on your local machine for development and testing purposes.
What things you need to install the software and how to install them.
sudo apt install curl
Opam is the package manager for OCaml.
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
opam init
eval $(opam env)
opam switch create 4.08.0
eval $(opam env)
Opam-depext is a tool to query and install external dependencies of opam packages.
opam install depext
eval $(opam env)
opam depext conf-gmp.1
opam depext conf-m4.1
Z3 is an SMT Solver by Microsoft.
opam install z3
export LD_LIBRARY_PATH=~/.opam/4.08.0/lib/z3
eval $(opam env)
Zarith is a library used to implement arithmetic and logical operations over arbitrary-precision integers.
opam install zarith
eval $(opam env)
Menhir is a parser generator for OCaml.
opam install menhir
eval $(opam env)
Oasis is a tool used to integrate a configure, build and install system in for OCaml projects.
opam install oasis
eval $(opam env)
To generates a build system, produce the files setup.ml, configure and Makefile, along with some others which can be safely ignored
oasis setup -setup-update dynamic
make
To run the automated tests for this system, run the file run.py.
python run.py
This will automatically run the system set-up with generated monitor descriptions and calculate the mean running time (over 3 repeated runs).
The experiment is repeated for incremental size and complexity for each of the six templates in generate.py, starting at n=1 up to n=15. Each run has a predefined time threshold of 10 hours, which if overcame, the run is terminated.
This will produce a CSV file with 6 columns (one for each monitor template) and 15 rows (for incremental size and complexity). Each reading represents the corresponding mean running time.