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

rebooting - snapshot WIP

parent 13e61437
install:
opam install --unlock-base oasis camlp4 batteries ocamlbuild ocamlfind
oasis setup -setup-update dynamic
ocaml setup.ml -configure
ocaml setup.ml -build
uninstall:
rm -f setup.data
rm -f setup.ml
rm -rf _build
rm -f decentmon.native
compile:
ocaml setup.ml -build
clean:
ocaml setup.ml -clean
# DecentMon: an OCaml Benchmark for Decentralised Monitoring of LTL Formulae
Current Version 1.1.
Current Version: 3.1.
---
......@@ -41,7 +41,7 @@ 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 installed with [opam](https://opam.ocaml.org).
Additional packages
Additional packages
- oasis
- campl4
- batteries
......@@ -57,20 +57,48 @@ Additional packages
```
opam install --unlock-base oasis camlp4 batteries ocamlbuild ocamlfind
```
5. Run oasis configuration by running in the root of the project:
5. [Configure oasis](https://ocaml.org/learn/tutorials/setting_up_with_oasis.html).
For this, the current oasis configutation file is used:
```
OASISFormat: 0.4
Name: DecentMon
Version: 3.1
Synopsis: Decentralised Monitoring of LTL formulae
Authors: Ylies Falcone, Univ. Grenoble Alpes, Inria
License: GPL-3
Executable decentmon
Path: src
BuildTools: ocamlbuild
MainIs: decentmon.ml
CompiledObject: best
BuildDepends: batteries, camlp4
```
- `OASISFormat` should be left as is;
- `Name`, `Version`, `Synopsis`, `Authors` and `Licence` are for information purposes
- `Path`indicates the relative path to the directory containing the source files
- `BuildTools` should be left as is
- `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).
The provided configutation can left as is or you can amend the file as per your needs.
6. Run the following command at the root of the project:
```
oasis setup -setup-update dynamic
```
6. Edit setup.data to match the pathes of your OCaml binaries.
7. To build DecentMon, run:
7. Edit setup.data to match the pathes of your OCaml binaries.
8. To build DecentMon, run:
```
ocaml setup.ml -build
```
8. If need be, to clean DecentMon, run:
For convenience, script `compile.sh` executes this command.
9. If need be, to clean DecentMon, run:
```
ocaml setup.ml -clean
```
For convenience, script `clean.sh` executes this command.
## 4 Running DecentMon
......@@ -261,3 +289,91 @@ S,T without Z responds to P:
[] (Q -> (P -> (!R U (S & !R & !Z & o((!R & !Z) U T)))) U
(R | [] (P -> (S & !Z & o(!Z U T)))))
```
## Appendix C: Complete List of Options
The list of all input options to DecentMon can be obtained by executing
```
decentmon.ext --help
```
(where `ext` is either `.native` or `byte` depending on your compilation option)
- `-n`: the maximm number of tests to run to obtain one row benchmark (each test can result in a meaningful sample or not, e.g., in the case of a non-monitorable formula)
- `-sf`: the *size of the formula*
- `-msf`: the *maximum size of the formula* (will test from size 1 to the value provided)
- `-st`: the *size of the trace*
- `-dalpha`: the *decentralized alphabet*
- `-alpha`: the *centralized alphabet* (will consider possible dalphabets generated from it)
- `-abs`: use *abscence* patterns
- `-exis`: use *existence* patterns
- `-bexis`: use *bounded existence* patterns
- `-univ`: use *universality* patterns
- `-prec`: use *precedence* patterns
- `-resp`: use *response* patterns
- `-precc`: use *precedence chain* patterns
- `-respc`: use *response chain* patterns
- `-consc`: use *constrained chain* patterns
- `-prt_trace_mess`: print *trace and number of messages statistics*
- `-prt_delay`: print *delay statistics*
- `-prt_full`: print *full statistics*
- `-flipcoin`: use the *flipcoin* probability distribution (uniform distribution with probabily 0.5)
- `-bernouilli` use the *BERNOUILLI* probability distribution (uniform distribution with a probability given as an argument)
- `-expo`: use the *EXPONENTIAL* probability distribution (the rate parameter is given as an argument)
- `-beta`: use the *BETA* probability distribution (the rate parameters are given as arguments)
- `-only_changes`: if enabled, components send the value of their propositions only if there is a change in its value. More precisely, if among the monitors, there is atleast the value of one proposition that is modified wrt the previous event, the component has to send a message to the monitor
- `-bias`: *bias the generation* of formulae to favor one component; the integer parameter is the index of the component
- `-precision`: the *precision of numbers* (number of decimals)
- `-eval`: CURRENT EVAL
- `-keep_samples`: keep samples
- `-file`: the name of the file on which samples should be stored
- `-nb_samples`: the number of target samples to obtain
- `-help`: display this list of options
- `--help`: display this list of options
We recommend having the value for option `-n` much larger than the value for option `nb_samples`.
## Appendix D: Examples
Examples should be executed at the root of the project (where the decentmon executable is located).
### Benchmark with Random Formulae
By running the following command:
```
./decentmon.native -n 500 -nb_samples 10 -msf 3 -st 1000 -dalpha "{a|b|c}" -prt_full true -keep_samples true -file log.txt
```
it tells DecentMon to execute a benchmark with the following options:
- For each entry line, the maximum number of tests is: 500
- For each entry line, the target number of sample is: 10
- Running benchmarks for formulae of maximum size: 3 (i.e., it will do a complete bench for each formula size between 1 and 3)
- Each formula will be monitored against a freshly randomly generated trace of size: 1000
- The probability distribution that will be used for the trace is flipcoin
- Distributed alphabet used: {a|b|c}
- Full statistics will be displayed.
- 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.
One can consult `log.txt to look at the individual sample experiments.
![alt text](doc_images/bench_random_formulae.png)
### Benchmark with Specification Patterns
By running the following command:
```
/decentmon.native -n 500 -nb_samples 10 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 1000 -dalpha "{a|b|c}" -prt_full true -keep_samples true -file log.txt
```
it tells DecentMon to execute a benchmark with the following options:
- For each entry line, the maximum number of tests is: 500
- For each entry line, the target number of sample is: 10
- The following LTL specification pattern(s) will be tested: abscence existence universality precedence response response_chain precedence_chain constrained_chain
- Each formula will be monitored against a freshly randomly generated trace of size: 1000
- The probability distribution that will be used for the trace is flipcoin
- Distributed alphabet used: {a|b|c}
- Full statistics will be displayed.
- 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.
One can consult `log.txt to look at the individual sample experiments.
![alt text](doc_images/bench_pattern_formulae.png)
# OASIS_START
# DO NOT EDIT (digest: 1b4c9dd0a477229a8c83547336834ac2)
# DO NOT EDIT (digest: 3ee2aa973816665a642e9e2601bf9875)
# Ignore VCS directories, you can use the same kind of rule outside
# OASIS_START/STOP if you want to exclude directories that contains
# useless stuff for the build process
......@@ -15,8 +15,8 @@ true: annot, bin_annot
"_darcs": -traverse
"_darcs": not_hygienic
# Executable decentmon
<src/decentmon.{native,byte}>: pkg_batteries
<src/decentmon.{native,byte}>: pkg_camlp4
<src/test.{native,byte}>: pkg_batteries
<src/test.{native,byte}>: pkg_camlp4
<src/*.ml{,i,y}>: pkg_batteries
<src/*.ml{,i,y}>: pkg_camlp4
# OASIS_STOP
......
ocaml setup.ml -clean
ocaml setup.ml -clean
ocaml setup.ml -build
FROM ocaml/opam
# Step 1: Installing OCaml dependencies
USER opam
RUN echo "Installing OCaml packages..."
RUN opam install oasis batteries ocamlbuild ocamlfind camlp4
RUN eval $(opam env)
#RUN echo "...Done."
# Create Workspace
USER root
RUN useradd -ms /bin/bash decentmon
RUN passwd -d decentmon
RUN mkdir -p /home/decentmon
USER decentmon
RUN chown decentmon /home/decentmon
WORKDIR /home/decentmon
# Step 3: Retrieving source files...
ADD src.zip .
ADD _oasis .
# Step: Building DecentMon
#RUN echo "Building DecentMon..."
#RUN oasis setup -setup-update dynamic
#RUN ocaml setup.ml -configure
#RUN ocaml setup.ml -build
#RUN echo "...Done."
CMD ["/bin/sh"]
docker:
cp ../_oasis .
zip src.zip ../src/*.ml
docker build -t decentmon:1 .
run:
docker run -ti decentmon:1
.PHONY: clean
clean:
rm _oasis
rm src.zip
OASISFormat: 0.4
Name: DecentMon
Version: 1.3
Synopsis: Decentralised Monitoring of LTL formulae
Authors: Ylies Falcone
License: GPL-3
Executable decentmon
Path: src
BuildTools: ocamlbuild
MainIs: decentmon.ml
CompiledObject: best
BuildDepends: batteries, camlp4
\ No newline at end of file
File added
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