Commit d7a44e46 authored by Jaime Arias's avatar Jaime Arias
Browse files

Initial commit

parents
# Created by https://www.gitignore.io/api/jupyternotebooks
# Edit at https://www.gitignore.io/?templates=jupyternotebooks
### JupyterNotebooks ###
# gitignore template for Jupyter Notebooks
# website: http://jupyter.org/
.ipynb_checkpoints
*/.ipynb_checkpoints/*
# IPython
profile_default/
ipython_config.py
# results
results
!results/*
results/*
!results/pmc-sog.zip
!results/pnml2lts-mc.zip
# Byte-compiled / optimized / DLL files
__pycache__/
*.py[cod]
*$py.class
# slurm batch
slurm
# editor
.vscode
# Remove previous ipynb_checkpoints
# git rm -r .ipynb_checkpoints/
# End of https://www.gitignore.io/api/jupyternotebooks
# 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
((Wsr3NotDeployed==1) && ((Wsr2NotDeployed==1) <-> <>(ScWorking==1))) <-> []((ScUnavailable==1) || (WebAppRuntime==1) || []<>(WsRuntime3==1))
((Wsr3NotDeployed) && ((Wsr2NotDeployed) <-> <>(ScWorking))) <-> []((ScUnavailable) || (WebAppRuntime) || []<>(WsRuntime3))
(OsAvailable==1) <-> (!(WSRuntime2==1) || ([](WebAppRuntime==1) -> !((WsRuntime3==1) && []((Bounder2==1) <-> (ContainerDown==1)))))
(OsAvailable) <-> (!(WSRuntime2) || ([](WebAppRuntime) -> !((WsRuntime3) && []((Bounder2) <-> (ContainerDown)))))
!(WebAppRuntime==1) || (Wsr3Started==1) || <>((ScStopped==1) -> !((WebAppRuntime==1) <-> ((WSRuntime1==1) <-> (Wsr2Started==1))))
!(WebAppRuntime) || (Wsr3Started) || <>((ScStopped) -> !((WebAppRuntime) <-> ((WSRuntime1) <-> (Wsr2Started))))
[](ServerContainer==1) <-> (((Bounder2==1) && !(WSRuntime1==1)) -> ((Wsr2NotDeployed==1) <-> !((SwContainer==1) <-> [](Bounder2==1))))
[](ServerContainer) <-> (((Bounder2) && !(WSRuntime1)) -> ((Wsr2NotDeployed) <-> !((SwContainer) <-> [](Bounder2))))
(!((ContainerDown==1) || (OsContainer==1)) && <>(OsAvailable==1)) <-> ((SwContainer==1) <-> <>[](ServerContainer==1))
(!((ContainerDown) || (OsContainer)) && <>(OsAvailable)) <-> ((SwContainer) <-> <>[](ServerContainer))
!(((OsContainer==1) <-> ((Bounder1==1) || !(Container==1) || !(OsContainer==1))) && (!(Bounder1==1) || (Wsr1Started==1)))
!(((OsContainer) <-> ((Bounder1) || !(Container) || !(OsContainer))) && (!(Bounder1) || (Wsr1Started)))
(!(SwContainer==1) || ((Bounder1==1) <-> (WebAppRuntime==1))) && ((SwContainer==1) || ([](ScUnavailable==1) <-> <>!(ScWorking==1)))
(!(SwContainer) || ((Bounder1) <-> (WebAppRuntime))) && ((SwContainer) || ([](ScUnavailable) <-> <>!(ScWorking)))
((ServerContainer==1) || !(SwContainer==1) || <>!(Wsr3Deployed==1)) <-> []((Wsr3Deployed==1) || [](WebAppRuntime==1))
((ServerContainer) || !(SwContainer) || <>!(Wsr3Deployed)) <-> []((Wsr3Deployed) || [](WebAppRuntime))
(((OsContainer==1) <-> ((WSRuntime2==1) || !(WebAppRuntime==1))) -> ((ScStopped==1) && (Wsr2Deployed==1))) && []((WsRuntime3==1) -> (Bounder2==1))
(((OsContainer) <-> ((WSRuntime2) || !(WebAppRuntime))) -> ((ScStopped) && (Wsr2Deployed))) && []((WsRuntime3) -> (Bounder2))
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