Commit c2c4970e authored by Yliès Falcone's avatar Yliès Falcone
Browse files

Update README.md

parent 8a224099
......@@ -8,7 +8,6 @@ Current Version: 3.1.
### Overview
<<<<<<< HEAD
DecenMon is an OCaml Benchmark for Decentralized Monitoring of LTL formulae.
DcentMont is written in the functional programming language OCaml.
......@@ -23,22 +22,6 @@ Earlier versions of the benchmark were released with the following conference pu
Decentralised LTL Monitoring. FM 2012: 85-100
> * Christian Colombo, Yliès Falcone:
Organising LTL Monitors over Distributed Systems with a Global Clock. RV 2014: 140-155
=======
DecentMon is an OCaml Benchmark for Decentralized Monitoring of LTL formulae.
DecentMon 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:
> Decentralised LTL monitoring. Formal Methods in System Design 48(1-2): 46-93 (2016)
> * Christian Colombo, Yliès Falcone:
> Organising LTL monitors over distributed systems with a global clock. Formal Methods in System Design 49(1-2): 109-158 (2016)
Earlier versions of the benchmark were released with the following conference publications:
> * Andreas Klaus Bauer, Yliès Falcone:
> Decentralised LTL Monitoring. FM 2012: 85-100
> * Christian Colombo, Yliès Falcone:
> Organising LTL Monitors over Distributed Systems with a Global Clock. RV 2014: 140-155
>>>>>>> c9c56920319b86718c69d3401ab4527d4dbe9cce
DecentMon takes as input:
......@@ -67,13 +50,10 @@ Additional packages
## 3. Installation
<<<<<<< HEAD
=======
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.
Otherwise, to install DecenMon, please follow the below steps.
>>>>>>> c9c56920319b86718c69d3401ab4527d4dbe9cce
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).
......@@ -105,24 +85,17 @@ Executable decentmon
- `MainIs` indicates the main file (entry point of the compilation process)
- `CompileObject` indicates whether to compile in bytecode or native format. It can take the values `bytecode` (compile in bytecode), `native` (compile in native) or `best` (compile in native if possible otherwise in bytecode).
<<<<<<< HEAD
The provided configutation can left as is or you can amend the file as per your needs.
=======
The provided configutation can be left as is or you can amend the file as per your needs.
>>>>>>> c9c56920319b86718c69d3401ab4527d4dbe9cce
6. Run the following command at the root of the project:
```
oasis setup -setup-update dynamic
```
<<<<<<< HEAD
7. Edit setup.data to match the pathes of your OCaml binaries.
=======
7. Run the following command at the root of the project:
```
ocaml setup.ml -configure
```
>>>>>>> c9c56920319b86718c69d3401ab4527d4dbe9cce
8. To build DecentMon, run:
```
ocaml setup.ml -build
......@@ -409,12 +382,8 @@ it tells DecentMon to execute a benchmark with the following options:
- Storing the results in `log.txt`
DecentMon will recall the selected options, run for a while and display the results as illustrated by the following screenshot.
<<<<<<< HEAD
One can consult `log.txt to look at the individual sample experiments.
![alt text](doc_images/bench_pattern_formulae.png)
=======
One can consult `log.txt` to look at the individual sample experiments.
One can consult `log.txt to look at the individual sample experiments.
![alt text](doc_images/bench_pattern_formulae.png)
......@@ -430,4 +399,3 @@ Scripts to run the examples from the FMSD paper
> Organising LTL monitors over distributed systems with a global clock. Formal Methods in System Design 49(1-2): 109-158 (2016)
are provided within the `example_benchs/fmsd_bench` directory.
>>>>>>> c9c56920319b86718c69d3401ab4527d4dbe9cce
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