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.
Distributed-SOG
Description
This repository hosts the experiments and results for the Distributed approach for the SOG construction and provides a short guide on how to install the tools and reproduce the results. This approach is based on distributed memory architectures.
** 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).
All experiments were performed on a Magi cluster of Paris 13 university.
The results of the distributed approach are reported in publication.
Building
mkdir build
cd build
cmake ..
Testing
philo5 example using 2 processes
mpirun -n 2 ./distributed-sog philo5.net Obs5_philo 32