From f5a668d8aedf30354bdfc3d773ecccbd223d7c57 Mon Sep 17 00:00:00 2001
From: Jaime Arias <arias@lipn.univ-paris13.fr>
Date: Thu, 13 Feb 2020 14:17:33 +0100
Subject: [PATCH] Download spot from URL instead of compiling from git
---
.gitmodules | 3 ---
CMakeLists.txt | 11 ++++++-----
README.md | 22 ++++++++++++----------
third-party/spot | 1 -
4 files changed, 18 insertions(+), 19 deletions(-)
delete mode 160000 third-party/spot
diff --git a/.gitmodules b/.gitmodules
index e0f0604..22c1558 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 8d84c87..44887aa 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 7ccfdad..7e64838 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 625a2e2..0000000
--- a/third-party/spot
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 625a2e2836cd3d8294a02f625943b2daec2644d2
--
GitLab