Skip to content
Snippets Groups Projects
Commit f5a668d8 authored by Jaime Arias's avatar Jaime Arias
Browse files

Download spot from URL instead of compiling from git

parent 30bbc07d
No related branches found
No related tags found
No related merge requests found
......@@ -5,6 +5,3 @@
path = third-party/sylvan
url = https://depot.lipn.univ-paris13.fr/PMC-SOG/sylvan.git
branch = Sylvan-SOG
[submodule "third-party/spot"]
path = third-party/spot
url = https://gitlab.lrde.epita.fr/spot/spot.git
......@@ -29,14 +29,15 @@ if(NOT SPOT_LIBRARY)
include(ExternalProject)
message(STATUS "Building Spot ...")
set(SPOT_SOURCE_DIR "${CMAKE_SOURCE_DIR}/third-party/spot")
set(SPOT_DIR "${CMAKE_BINARY_DIR}/third-party/spot")
ExternalProject_Add(SpotLibrary
PREFIX ${SPOT_DIR}
SOURCE_DIR ${SPOT_SOURCE_DIR}
CONFIGURE_COMMAND autoreconf -if ${SPOT_SOURCE_DIR} && ${SPOT_SOURCE_DIR}/configure --disable-python --prefix=<INSTALL_DIR>
BUILD_COMMAND make -j
PREFIX ${SPOT_DIR}
URL http://www.lrde.epita.fr/dload/spot/spot-2.8.5.tar.gz
DOWNLOAD_NO_PROGRESS YES
CONFIGURE_COMMAND ./configure --disable-doxygen --disable-python --enable-silent-rules --silent --prefix=<INSTALL_DIR>
BUILD_COMMAND make -j
BUILD_IN_SOURCE 1
)
include_directories("${SPOT_DIR}/include")
......
# PMC-SOG
(P)arallel (M)odel (C)hecking using the (S)ymbolic (O)bservation (G)raph
(P)arallel (M)odel (C)hecking using the (S)ymbolic (O)bservation (G)raph.
A [Symbolic Observation Graph](https://www.researchgate.net/profile/Kais_Klai/publication/48445044_Design_and_Evaluation_of_a_Symbolic_and_Abstraction-Based_Model_Checker/links/00463514319a181966000000.pdf) software tool has been implemented in C/C++.
The user can choose between sequential or parallel construction.
......@@ -9,28 +9,30 @@ The [BuDDy](http://buddy.sourceforge.net/manual/main.html) BDD package and [Sylv
BuDDy used for sequential version and Sylvan for both sequential and parallel construction.
It is necessary to install [Spot](https://spot.lrde.epita.fr/install.html).
## 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](https://www.open-mpi.org/) implementation). The goal of the MPI is to establish a portable, efficient, and flexible standard for message passing between processess (nodes).
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.
** Pthread : POSIX thread librarie. Mutexes (Pthread lock functionality) are used to prevent data inconsistencies due to race conditions.
* **MPI:** The Message Passing Interface ([OpenMPI](https://www.open-mpi.org/) 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](https://cmake.org/)
- [Bison](https://www.gnu.org/software/bison/)
- [Flex](https://github.com/westes/flex)
- [OpenMPI](https://www.open-mpi.org/) development libraries
- [OpenSSL](https://www.openssl.org/) development libraries
- [GMP](https://gmplib.org/) development libraries
## Building
- `git clone --recursive https://depot.lipn.univ-paris13.fr/PMC-SOG/mc-sog.git`
- `mkdir build`
- `cd build`
- `cd mc-sog && mkdir build && cd build`
- `cmake ..`
......
spot @ 625a2e28
Subproject commit 625a2e2836cd3d8294a02f625943b2daec2644d2
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment