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

update README

parent e2cd72f2
......@@ -35,7 +35,7 @@ git clone https://depot.lipn.univ-paris13.fr/PMC-SOG/experiments/hybrid.git && c
│   └── pnml2lts-mc.zip # results (logs) related to the ltsmin model-checker
├── run-experiment.py # script that run a experiment on the local machine
├── scripts
│   ├── csv_generator.py # script that generates a csv file with the results from the logs
│   ├── csv_generator.py # script that generates a csv file with the results from the logs
│   ├── formula_generator.py # script that generates N random LTL\X formulas
│   └── plot-results.ipynb # Python notebook that allows to generate the figures and interact with the results
│   └── plot-results.py # script that generates the figures (if you do not want to open the notebook)
......@@ -97,7 +97,7 @@ optional arguments:
- 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`
- `sbatch slurm/experiments/pmc-sog/pmc-sog_otfP_default/philo/n1-th8.sbatch`
## Generate Figures
......@@ -119,9 +119,27 @@ on Ubuntu 18.04.4 LTS.
### Generate Figures
- `cd scripts`
- `python3 generate-csv.py`
- `python3 csv_generator.py`
- `python3 plot-results.py`
## Authors
- Kais Klai (University of Paris 13, Sorbonne Paris Cite CNRS UMR 7030 LIPN
- Chiheb Ameur Abid (Faculty of Sciences of Tunis, University of Tunis El Manar, 2092, Tunis, Tunisia)
- Jaime Arias (University of Paris 13, Sorbonne Paris Cite CNRS UMR 7030 LIPN)
## Abstract
In this paper, we propose a hybrid parallel model checking algorithm for both
shared and distributed memory architectures. The model checking is performed
simultaneously with a parallel construction of system state space by
distributed multi-core machines. The representation of the system's state
space is a hybrid graph called Symbolic Observation Graph (SOG) combining
symbolic representation of its nodes (sets of single states) and explicit
representation of arcs. The SOG is adapted in order to allow the preservation
of both state and event-based LTL formulae (hybrid LTL) i.e., the atomic
propositions involved in the formula to be checked could be either
state-based or event-based propositions.
We have implemented the proposed model checker within a C++ prototype and
compared our preliminary results with the state of the art model checkers.
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