HTTPS SSH
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)

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 run:

    docker run -it krledmno1/aerial
    
to pull and run a Docker container with Aerial installed.