Merge branch 'falconey-master-patch-78681' into 'master'

Update README.md

See merge request !1

README.md

@@ -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