Commit 06e7f0ad authored by Ylies Falcone's avatar Ylies Falcone
Browse files

Merge branch 'master' of gricad-gitlab.univ-grenoble-alpes.fr:falconey/decentmon

parents 29580467 50883a95
......@@ -6,7 +6,10 @@ Current Version 1.1.
## 1 Description
### Overview
DecenMon is an OCaml Benchmark for Decentralized Monitoring of LTL formulae.
DcentMont is written in the functional programming language OCaml.
For a full description of the underlying algorithms and principles, we refer the reader to the following journal publications:
> * Andreas Bauer, Yliès Falcone:
......@@ -37,42 +40,36 @@ LTL formulae are analysed in two different modes:
## 2 Requirements
MANDATORY:
- An [OCaml](https://ocaml.org) environment and compiler (ocamlc, ocamlopt).
- Ocaml's preprocessor [camlp4](https://ocaml.org). It can be installed smoothly on Linux and Mac OS X.
OPTIONAL:
- [GNU Make](https://www.gnu.org/software/make/).
- [ocamlweb](https://www.lri.fr/~filliatr/ocamlweb/) to generate automatically the documentation.
DecentMon requires GNU Make, [OCaml](https://ocaml.org) and a few OCaml extensions which can be installed with [opam](https://opam.ocaml.org).
Additional packages
- oasis
- campl4
- batteries
- ocamlbuild
- ocamlfind
## 3. Installation
1. [Install OPAM](https://opam.ocaml.org/doc/Install.html).
2. Install a C compiler (to install OCaml).
3. [Install OCaml](https://ocaml.org/docs/install.html).
4. Install the aditional extensions:
```
opam install --unlock-base oasis camlp4 batteries ocamlbuild ocamlfind
```
5. Run oasis configuration by running in the root of the project:
```
oasis setup -setup-update dynamic
```
6. To build DecentMon, run:
```
ocaml setup.ml -build
```
7. If need be, to clean DecentMon, run:
```
ocaml setup.ml -clean
```
If you have GNU Make available on your machine, a Makefile is provided to ease the installation. Please follow the following steps:
1. Unzip the distribution in some directory of your choice, e.g., /home/you/DECENTMON.
2. Goto the directory where the sources have been extracted.
3. Either:
1. type `make decentmon`, it will generate the benchmark in native binary code;
1. type `make decentmon_nonat`, it will generate a bytecode executable.
Prefer option 3.1 if ocamlopt is available on your machine (the benchmark will run faster).
If you do not have GNU Make installed on your machine, please follow first steps 1. and 2., and then type:
- for native code generation:
```
ocamlopt -I +camlp4 -pp camlp4of.opt types.ml enum.mli enum.ml extString.mli
extString.ml IO.mli IO.ml std.mli std.ml ltl.ml ltl_parser.ml
ltl_generator.ml progression.ml trace.ml d_progression.ml
trace_parser.ml alphabet_parser.ml
```
- for bytecode generation:
```
ocamlc -I +camlp4 -pp camlp4of.opt types.ml enum.mli enum.ml extString.mli
extString.ml IO.mli IO.ml std.mli std.ml ltl.ml ltl_parser.ml
ltl_generator.ml progression.ml trace.ml d_progression.ml
trace_parser.ml alphabet_parser.ml
```
In both cases, installation will generate an executable file named "decentmon".
## 4 Running DecentMon
......@@ -117,7 +114,7 @@ Then, one can choose the metrics and statistics that shall be displayed by using
- `-prt_trace_mess [bool]` to indicate that trace and number of messages statistics") shall be displayed,
- ` -prt_delay [bool]` to indicate that delay statistics shall be displayed.
## Appendix A Input formats
## Appendix A: Input formats
We describe below some input formats that shall be used when submitting inputs for benchmark to DecentMon.
......@@ -126,7 +123,7 @@ We describe below some input formats that shall be used when submitting inputs f
They are represented by a quoted string. Distributed alphabets are delimited by curly braces. Inside a distributed alphabet the symbol `|` (resp. `,`) is used to indicate component separation (reps. separate symbols inside a component).
For instance `{a1,a2|b1,b2|c1,c2}` denotes a 3-component architecture. On component 1 (reps. 2,3), the local alphabet contains symbols a1 and a2 (resp. b1 and b2, c1 and c2).
### Appendix B LTL Specification Patterns
### Appendix B: LTL Specification Patterns
The following patterns come from the [Specification Pattern Website](http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml) (for LTL formulae).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment