diff --git a/.gitmodules b/.gitmodules index e0f060479f35139515227f51c579dee8ddf5c28b..22c1558c01ea44e848625f065f06082d3423efec 100644 --- a/.gitmodules +++ b/.gitmodules @@ -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 diff --git a/CMakeLists.txt b/CMakeLists.txt index 8d84c87aacc3d00cea471e8bf45dc37a379b4f7b..44887aa06a9d6636ae913cb8827a048e54ce6d4e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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") diff --git a/README.md b/README.md index 7ccfdad50695d607fd4d081d4d28a13752c0f9b5..7e648388447c9997e83d55dcd27954a40f645b66 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # 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 ..` diff --git a/third-party/spot b/third-party/spot deleted file mode 160000 index 625a2e2836cd3d8294a02f625943b2daec2644d2..0000000000000000000000000000000000000000 --- a/third-party/spot +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 625a2e2836cd3d8294a02f625943b2daec2644d2