PMC-SOG
(P)arallel (M)odel (C)hecking using the (S)ymbolic (O)bservation (G)raph.
A Symbolic Observation Graph software tool has been implemented in C/C++. The user can choose between sequential or parallel construction.
The BuDDy BDD package and Sylvan package are exploited in order to represent aggregates compactly.
BuDDy used for sequential version and Sylvan for both sequential and parallel construction.
It is necessary to install Spot.
Description
This repository hosts the experiments and results for the Hybrid (MPI/pthreads) approach for the SOG construction and provides a short guide on how to install the tools and reproduce the results.
-
MPI: The Message Passing Interface (OpenMPI implementation). The goal of the MPI is to establish a portable, efficient, and flexible standard for message passing between processess (nodes).
-
Pthread: POSIX thread library. Mutexes (Pthread lock functionality) are used to prevent data inconsistencies due to race conditions.
Dependencies
- Cmake
- Bison
- Flex
- OpenMPI development libraries
- OpenSSL development libraries
- GMP development libraries
Building
-
git clone --recursive https://depot.lipn.univ-paris13.fr/PMC-SOG/mc-sog.git -
cd mc-sog && mkdir build && cd build -
cmake .. -
cmake --build .
Testing
SOG building from an LTL formula (philo3.net example)
Multi-threading execution
mpirun -n 1 hybrid-sog arg1 arg2 arg3 arg4 [arg5]
arg1: specifies method of creating threads or/and specifies if modelchecking should be performed on the fly. It can be set with one of the following values:
* p : using pthread library
* pc : using pthread library and applying canonization on nodes
* l : using lace framework
* lc : using lace framework and applying canonization on nodes
* otfL : perform modelchecking on the fly using laceframework
* otfP : perform modelchecking on the fly using pthread
* otfC : perform modelchecking on the fly using c++17 algorithms and a work-stealing approach for the construction of aggregates
arg2: specify the number of threads/workers to be created
arg3: specify the net to build its SOG
arg4: specify the LTL formula file
arg5: (Optional) select an algorithm for the emptiness check provided by spot, see https://spot.lrde.epita.fr/doxygen/group__emptiness__check.html
* Cou99
+ shy
+ poprem
+ group
* GC04
* CVWY90
+ bsh : set the size of a hash-table
* SE05
+ bsh : set the size of a hash-table
* Tau03
* Tau03_opt
Distributed execution
mpirun -n arg0 hybrid-sog arg1 arg 2 arg3 arg4
arg0 : specifies the number of processes must be >1
arg1: specifies whether modelchecking should be performed on the fly. It can be set with one of the following values:
* otf : Construction performing Model checking on the fly
* otherwise : construction without Model checking
arg2: specifies the number of threads/workers to be created
arg3: specifies the net to build its SOG
arg4: specifies the LTL formula file
arg5: (Optional) select an algorithm for the emptiness check provided by spot, see https://spot.lrde.epita.fr/doxygen/group__emptiness__check>
* Cou99
+ shy
+ poprem
+ group
* GC04
* CVWY90
+ bsh : set the size of a hash-table
* SE05
+ bsh : set the size of a hash-table
* Tau03
* Tau03_opt