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

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


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:

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.