README.md 4.65 KB
Newer Older
Jaime Arias's avatar
Jaime Arias committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
# SOG-Based Hybrid LTL Model Checking

This repository hosts the results for the paper.

The experimental results were obtained on [Magi
cluster](http://magi.univ-paris13.fr/wiki/) of [University Sorbonne Paris
Nord](https://univ-paris13.fr/). We used the partition `COMPUTE` which has 40
processors (two Intel Xeon E5-2650 v3 at 2.30GHz) connected by an InfiniBand
network, and 64GB of RAM. A total of 5 models from the [Model Checking
Contest](https://mcc.lip6.fr/models.php) were used in our experiments:
*[Philosophers](models/philo/description.pdf)* (`philo`),
*[RobotManipulation](models/robot/description.pdf)* (`robot`),
*[SwimmingPool](models/spool/description.pdf)*
(`spool`), *[CircularTrains]((models/train/description.pdf))* (`train`), and
*[TokenRing](models/tring/description.pdf)* (`ring`).


## Clone this repository:
```
git clone https://depot.lipn.univ-paris13.fr/PMC-SOG/experiments/atva2020.git && cd atva2020
```

## Folder Structure

```
.
├── formulas                        # folder containing the LTL\X formulas
├── models                          # folder containing the models
├── results
│   ├── pmc-sog.zip                 # results (logs) related to our model-checker
│   └── pnml2lts-mc.zip             # results (logs) related to the ltsmin model-checker
├── run-experiment.py               # script that run a experiment on the local machine
├── scripts
│   ├── formula-generator.sh        # script that generates N random LTL\X formulas
│   ├── generate-csv.py             # script that generates a csv file with the results from the logs
│   └── plot-results.ipynb          # Python notebook that allows to generate the figures and interact with the results
│   └── sbatch_generator.py         # script that generates the sbatch files to run the experiments on Magi cluster
└── tools
    ├── pmc-sog                     # binary of our model-checker
    └── pnml2lts-mc                 # binary of the ltsmin model-checker
```

## Run experiments

In the following we provide the steps to run the experiments. We tested this
on Ubuntu 18.04.4 LTS.

### Install dependencies

  - `sudo apt install git python3`
  - `pmc-sog`: Please read the [installation notes](https://depot.lipn.univ-paris13.fr/PMC-SOG/mc-sog).
  - `pnml2lts-mc`: Download from [here](http://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/ltsmin-v3.0.2-linux.tgz).


The binaries `pmc-sog` and `pnml2lts-mc` must be copied in the `tools` folder.

### Local Run

To run the experiments on a local machine, the script `run-experiment.py` can
be used.

`./run-experiment.py --processes 1 --threads 8 --tool pmc-sog --model-name=philo --model-instance=philo10 --formula=1 --tool-parameter parallelisation=otfP --tool-parameter strategy="Cou99 (poprem)"`

```
./run-experiment.py -h
usage: run-experiment.py [-h] --processes PROCESSES --threads THREADS --tool
                         {pmc-sog,pnml2lts-mc} --model-name MODEL_NAME
                         --model-instance MODEL_INSTANCE --formula FORMULA
                         [--tool-parameter PARAMETERS]

Run an experiment on the local machine

optional arguments:
  -h, --help            show this help message and exit
  --processes PROCESSES
                        number of process
  --threads THREADS     number of threads
  --tool {pmc-sog,pnml2lts-mc}
                        model-checker tool
  --model-name MODEL_NAME
                        Name of the model (e.g. philo)
  --model-instance MODEL_INSTANCE
                        Instance of the model (e.g. philo10)
  --formula FORMULA     Number of the property to verify
  --tool-parameter PARAMETERS
                        Parameter of the tool
```

### Cluster (slurm) Run

- Run the script that generates slurm batch:
  - `./scripts/sbatch_generator.py`
- Execute the experiment with `sbtach`:
  - `sbatch slurm/slurm/pmc-sog/pmc-sog_otfP_default/philo/n1-th8.sbatch`

## Generate Figures

In the following we provide the steps to generate the figures. We tested this
on Ubuntu 18.04.4 LTS.

### Install dependencies
  - `sudo apt install git unzip wget libfuse2 libnss3 libgdk-pixbuf2.0-0 libgtk-3-0 libx11-xcb1 libxss1 libasound2 python3 python3-pip`
  - `pip3 install --user pandas plotly psutil requests`
  - `wget https://github.com/plotly/orca/releases/download/v1.3.1/orca-1.3.1.AppImage`
  - `chmod +x orca-1.3.1.AppImage`
  - `mv orca-1.3.1.AppImage /usr/local/bin/orca`

### Decompress results
  - `cd results`
  - `unzip -q pmc-sog.zip`
  - `unzip -q pnml2lts-mc.zip`
  - `cd ..`

### Generate Figures
  - `cd scripts`
  - `python3 generate-csv.py`
  - `python3 plot-results.py`

## Authors

## Abstract