Commit 0d5fa2ff authored by Yliès Falcone's avatar Yliès Falcone
Browse files

Update README.md

parent dc5d4436
......@@ -40,16 +40,47 @@ LTL formulae are analysed in two different modes:
## 2 Requirements
DecentMon requires GNU Make, [OCaml](https://ocaml.org) and a few OCaml extensions which can be easily installed with [opam](https://opam.ocaml.org).
Additional packages are:
Additional required packages are:
- oasis
- campl4
- batteries
- ocamlbuild
- ocamlfind
DecentMon has been built as end of 2021 with OCaml 4.02. Later versions of OCaml seem not compatible with camlp4.
## 3. Installation
If you wan to try DecentMon without installing it, you can find a [Virtual Box](https://www.virtualbox.org) virtual machine within the `decentmon_vm` directory of the repository.
If you wan to try DecentMon without installing it, you can:
- run it within a provided virtual machine where DecentMon is preinstalled;
- a Docker file allowing to build a Docker image and run DecentMon within a container.
Otherwise, in Section 3.3, you can find instructions to install DecentMon on your machine.
### 3.1 Pre-installed version from the provided virtual machine
There is a Ubuntu [Virtual Box](https://www.virtualbox.org) virtual machine within the `decentmon_vm` directory of the repository.
As the image is going to be outdated, make sure to update it with latest security patches.
### 3.2 Installation with Docker
In directory `docker`, there is a Dockerfile to build a docker image.
Once you have Docker and GNU make installed on your machine, simply run:
```
make docker
```
This may take a few minutes (depending on the images that will be downloaded).
Then to run the container, and compile DecentMon, run:
```
make run
```
Within the container, if you modify the source files (in src/), and need to recompile DecentMon, run:
```
ocaml setup.ml -build
```
### 3.3 Installation on your machine
Otherwise, to install DecenMon, please follow the below steps.
......@@ -112,15 +143,15 @@ Then several other options are mandatory:
In this benchmark, one indicates one or several LTL specification patterns to be tested (see the [Specification pattern Website](http://patterns.projects.cis.ksu.edu/)). For convenience, the various kinds of formulae for each LTL specification patterns are recalled in Appendix B. The options used to select patterns are:
- ` -abs [boolean]`: to select the *Absence* specification pattern for testing when the boolean is true;
- ` -exis [boolean]`: to select the *Existence* specification pattern for testing when the boolean is true;
- ` -univ [boolean]`: to select the *Universality* specification pattern for testing when the boolean is true;
- ` -prec [boolean]`: to select the *Precedence* specification pattern for testing when the boolean is true;
- ` -resp [boolean]`: to select the *Response* specification pattern for testing when the boolean is true;
- ` -prec [boolean]`: to select the *Precedence* specification pattern for testing when the boolean is true;
- ` -precc [boolean]`: to select the *Precedence Chain* specification pattern for testing when the boolean is true;
- ` -respc [boolean]`: to select the *Response Chain* specification pattern for testing when the boolean is true;
- ` -consc [boolean]`: to select the *Contrained Chain* specification pattern for testing when the boolean is true.
- `-abs [boolean]`: to select the *Absence* specification pattern for testing when the boolean is true;
- `-exis [boolean]`: to select the *Existence* specification pattern for testing when the boolean is true;
- `-univ [boolean]`: to select the *Universality* specification pattern for testing when the boolean is true;
- `-prec [boolean]`: to select the *Precedence* specification pattern for testing when the boolean is true;
- `-resp [boolean]`: to select the *Response* specification pattern for testing when the boolean is true;
- `-prec [boolean]`: to select the *Precedence* specification pattern for testing when the boolean is true;
- `-precc [boolean]`: to select the *Precedence Chain* specification pattern for testing when the boolean is true;
- `-respc [boolean]`: to select the *Response Chain* specification pattern for testing when the boolean is true;
- `-consc [boolean]`: to select the *Contrained Chain* specification pattern for testing when the boolean is true.
Not mentioning a specification patterns amounts to setting its Boolean flag to false.
......@@ -131,7 +162,7 @@ Similarly, several other options are mandatory:
Then, one can choose the metrics and statistics that shall be displayed by using one of the following options:
- `-prt_full [bool]` to indicate that all statistics (number of messages, trace lengths and their ratio, but also the maximal and average delay) shall be displayed,
- `-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.
- `-prt_delay [bool]` to indicate that delay statistics shall be displayed.
## Appendix A: Input formats
......
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