Pushed to traytel/aerial
Aerial: An Almost Event-Rate Independent Monitor for Metric Temporal Logic and Metric Dynamic Logic Srđan Krstić 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. The algorithms behind this tool were developed jointly with David Basin and Bhargav Bhatt. The theory is described in the paper draft: Almost Event-Rate Independent Monitoring of Metric Temporal Logic http://people.inf.ethz.ch/trayteld/papers/aerial/aerial.pdf Aerial depends on a recent (>= 4.04.0) version of the OCaml compiler. (An outdated PolyML implementation of Aerial referenced in the above paper can be found in this repository under the tag 'poly'.) To install ocaml and some additional libraries use opam - ocaml's package manager. For example: apt-get install opam opam switch 4.04.1 eval $(opam config env) opam install safa menhir then compile Aerial with make to obtain a binary aerial.native file and ./aerial.native -fmla examples/test1.mtl -log examples/test2.log to run an example. ./aerial.native -? provides some additional hints about the tool's user interface. This repository also contains the bash scripts used to generate log files and run the experiments reported on in the above paper (directory experiments). The shell scripts assume the "aerial", "monpoly" and "montre" binary files to be available in the PATH, a working installation of GNU Parallel and coreutils package for macOS. Scripts are tested on macOS 10.12.4 and Ubuntu 16.04. A pre-configured environment for running the experiments can be found on the official tool website: http://www.infsec.ethz.ch/research/software/aerial.html Alternatively, if Docker is available, no need to clone this repository, simply run: docker run -it krledmno1/aerial to pull and run a Docker container with Aerial installed.