From 7294d1148ecffe49039067eeb282c476cf46bf46 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Fri, 19 Feb 2021 11:12:16 +0100
Subject: [PATCH] Added new distributed algorithm
---
CMakeLists.txt | 2 +-
src/CMakeLists.txt | 31 +-
src/CommonSOG.cpp | 76 +++
src/CommonSOG.h | 7 +-
src/DistributedSOG.h | 2 +-
src/{ => Hybrid}/HybridKripke.cpp | 4 +-
src/{ => Hybrid}/HybridKripke.h | 2 +-
src/{ => Hybrid}/HybridKripkeIterator.cpp | 0
src/{ => Hybrid}/HybridKripkeIterator.h | 0
src/{ => Hybrid}/HybridKripkeState.cpp | 0
src/{ => Hybrid}/HybridKripkeState.h | 0
src/{ => Hybrid/MCHybrid}/MCHybridSOG.cpp | 84 +---
src/{ => Hybrid/MCHybrid}/MCHybridSOG.h | 6 +-
src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp | 456 ++++++++++++++++++
src/Hybrid/MCHybridReq/MCHybridSOGReq.h | 94 ++++
src/HybridSOG.h | 2 +-
src/{ => MCMultiCore}/ModelCheckThReq.cpp | 71 +--
src/{ => MCMultiCore}/ModelCheckThReq.h | 2 +-
.../ModelCheckerCPPThread.cpp | 78 +--
src/{ => MCMultiCore}/ModelCheckerCPPThread.h | 4 +-
src/{ => MCMultiCore}/ModelCheckerTh.cpp | 72 +--
src/{ => MCMultiCore}/ModelCheckerTh.h | 0
src/main.cpp | 59 +--
src/{ => misc}/SafeDequeue.cpp | 0
src/{ => misc}/SafeDequeue.h | 0
src/{ => misc}/md5_hash.h | 0
src/{ => misc}/sha2.c | 0
src/{ => misc}/sha2.h | 0
src/{ => misc}/stacksafe.cpp | 0
src/{ => misc}/stacksafe.h | 0
30 files changed, 685 insertions(+), 367 deletions(-)
rename src/{ => Hybrid}/HybridKripke.cpp (94%)
rename src/{ => Hybrid}/HybridKripke.h (85%)
rename src/{ => Hybrid}/HybridKripkeIterator.cpp (100%)
rename src/{ => Hybrid}/HybridKripkeIterator.h (100%)
rename src/{ => Hybrid}/HybridKripkeState.cpp (100%)
rename src/{ => Hybrid}/HybridKripkeState.h (100%)
rename src/{ => Hybrid/MCHybrid}/MCHybridSOG.cpp (87%)
rename src/{ => Hybrid/MCHybrid}/MCHybridSOG.h (94%)
create mode 100644 src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
create mode 100644 src/Hybrid/MCHybridReq/MCHybridSOGReq.h
rename src/{ => MCMultiCore}/ModelCheckThReq.cpp (67%)
rename src/{ => MCMultiCore}/ModelCheckThReq.h (93%)
rename src/{ => MCMultiCore}/ModelCheckerCPPThread.cpp (57%)
rename src/{ => MCMultiCore}/ModelCheckerCPPThread.h (93%)
rename src/{ => MCMultiCore}/ModelCheckerTh.cpp (66%)
rename src/{ => MCMultiCore}/ModelCheckerTh.h (100%)
rename src/{ => misc}/SafeDequeue.cpp (100%)
rename src/{ => misc}/SafeDequeue.h (100%)
rename src/{ => misc}/md5_hash.h (100%)
rename src/{ => misc}/sha2.c (100%)
rename src/{ => misc}/sha2.h (100%)
rename src/{ => misc}/stacksafe.cpp (100%)
rename src/{ => misc}/stacksafe.h (100%)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5ae4704..503c29e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -15,7 +15,7 @@ set(CMAKE_CXX_EXTENSIONS OFF)
# Add compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
#used flags -Og -DNDEBUG
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread -DNDEBUG -funswitch-loops -floop-interchange -floop-unroll-and-jam -fpeel-loops -fpredictive-commoning -fsplit-loops -fsplit-paths -fexpensive-optimizations -fcse-follow-jumps -fthread-jumps -finline-functions -finline-small-functions -findirect-inlining -foptimize-strlen -fpartial-inlining -fexpensive-optimizations -falign-functions -falign-jumps -falign-labels -falign-loops -fcaller-saves -fdelete-null-pointer-checks")#-DNDEBUG -funswitch-loops -floop-interchange -floop-unroll-and-jam -fpeel-loops -fpredictive-commoning -fsplit-loops -fsplit-paths -fexpensive-optimizations -fcse-follow-jumps -fthread-jumps -finline-functions -finline-small-functions -findirect-inlining -foptimize-strlen -fpartial-inlining -fexpensive-optimizations -falign-functions -falign-jumps -falign-labels -falign-loops -fcaller-saves -fdelete-null-pointer-checks") #
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread -DNDEBUG -funswitch-loops -floop-interchange -floop-unroll-and-jam -fpeel-loops -fpredictive-commoning -fsplit-loops -fsplit-paths -fexpensive-optimizations -fcse-follow-jumps -fthread-jumps -finline-functions -finline-small-functions -findirect-inlining -foptimize-strlen -fpartial-inlining -fexpensive-optimizations -falign-functions -falign-jumps -falign-labels -falign-loops -fcaller-saves -fdelete-null-pointer-checks -DNDEBUG -funswitch-loops -floop-interchange -floop-unroll-and-jam -fpeel-loops -fpredictive-commoning -fsplit-loops -fsplit-paths -fexpensive-optimizations -fcse-follow-jumps -fthread-jumps -finline-functions -finline-small-functions -findirect-inlining -foptimize-strlen -fpartial-inlining -fexpensive-optimizations -falign-functions -falign-jumps -falign-labels -falign-loops -fcaller-saves -fdelete-null-pointer-checks") #
endif()
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0b6a393..26f1d64 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -60,25 +60,28 @@ add_executable(mc-sog main.cpp
SogKripkeIteratorTh.cpp
SogKripkeIteratorTh.h
- stacksafe.cpp
- stacksafe.h
- SafeDequeue.cpp
- SafeDequeue.h
- HybridKripke.cpp
- HybridKripke.h
- HybridKripkeIterator.cpp
- HybridKripkeIterator.h
- HybridKripkeState.cpp
- HybridKripkeState.h
+ misc/stacksafe.cpp
+ misc/stacksafe.h
+ misc/SafeDequeue.cpp
+ misc/SafeDequeue.h
+ Hybrid/HybridKripke.cpp
+ Hybrid/HybridKripke.h
+ Hybrid/HybridKripkeIterator.cpp
+ Hybrid/HybridKripkeIterator.h
+ Hybrid/HybridKripkeState.cpp
+ Hybrid/HybridKripkeState.h
SylvanWrapper.cpp
SylvanWrapper.h
SylvanCacheWrapper.cpp SylvanCacheWrapper.h
- ModelCheckerCPPThread.cpp ModelCheckerCPPThread.h
- ModelCheckerTh.cpp ModelCheckerTh.h
+ MCMultiCore/ModelCheckerCPPThread.cpp MCMultiCore/ModelCheckerCPPThread.h
+ MCMultiCore/ModelCheckerTh.cpp MCMultiCore/ModelCheckerTh.h
threadSOG.cpp threadSOG.h
HybridSOG.cpp HybridSOG.h
- MCHybridSOG.cpp MCHybridSOG.h
- ModelCheckThReq.cpp ModelCheckThReq.h md5_hash.h )
+ Hybrid/MCHybrid/MCHybridSOG.cpp Hybrid/MCHybrid/MCHybridSOG.h
+ MCMultiCore/ModelCheckThReq.cpp MCMultiCore/ModelCheckThReq.h
+ Hybrid/MCHybridReq/MCHybridSOGReq.cpp
+ Hybrid/MCHybridReq/MCHybridSOGReq.h
+ misc/md5_hash.h)
target_include_directories(mc-sog PUBLIC "${PROJECT_BINARY_DIR}/src")
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 3bf63d0..8fc570e 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -177,4 +177,80 @@ LDDGraph *CommonSOG::m_graph;
string_view CommonSOG::getPlace(int pos) {
return string_view {m_graph->getPlace(pos)};
+}
+
+void CommonSOG::initializeLDD() {
+ SylvanWrapper::sylvan_set_limits(16LL << 30, 10, 0);
+ SylvanWrapper::sylvan_init_package();
+ SylvanWrapper::sylvan_init_ldd();
+ SylvanWrapper::init_gc_seq();
+ SylvanWrapper::lddmc_refs_init();
+ SylvanWrapper::displayMDDTableInfo();
+}
+
+void CommonSOG::loadNetFromFile() {
+ int i;
+ vector<Place>::const_iterator it_places;
+ m_nbPlaces = m_net->places.size();
+ m_transitions = m_net->transitions;
+ m_observable = m_net->Observable;
+ m_place_proposition = m_net->m_formula_place;
+ m_nonObservable = m_net->NonObservable;
+
+ m_transitionName = &m_net->transitionName;
+ m_placeName = &m_net->m_placePosName;
+
+
+ InterfaceTrans = m_net->InterfaceTrans;
+
+ cout << "Nombre de places : " << m_nbPlaces << endl;
+ cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
+
+ uint32_t *liste_marques = new uint32_t[m_net->places.size()];
+ for (i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++) {
+ liste_marques[i] = it_places->marking;
+ }
+
+ m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, m_net->places.size());
+ SylvanWrapper::lddmc_refs_push(m_initialMarking);
+ delete[]liste_marques;
+
+ uint32_t *prec = new uint32_t[m_nbPlaces];
+ uint32_t *postc = new uint32_t[m_nbPlaces];
+ // Transition relation
+ for (auto t = m_net->transitions.begin();
+ t != m_net->transitions.end(); t++) {
+ // Initialisation
+ for (i = 0; i < m_nbPlaces; i++) {
+ prec[i] = 0;
+ postc[i] = 0;
+ }
+ // Calculer les places adjacentes a la transition t
+ set<int> adjacentPlace;
+ for (vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++) {
+ adjacentPlace.insert(it->first);
+ prec[it->first] = prec[it->first] + it->second;
+ //printf("It first %d \n",it->first);
+ //printf("In prec %d \n",prec[it->first]);
+ }
+ // arcs post
+ for (vector<pair<int, int> >::const_iterator it = t->post.begin(); it != t->post.end(); it++) {
+ adjacentPlace.insert(it->first);
+ postc[it->first] = postc[it->first] + it->second;
+
+ }
+ for (set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++) {
+ MDD Precond = lddmc_true;
+ Precond = Precond & ((*it) >= prec[*it]);
+ }
+
+ MDD _minus = SylvanWrapper::lddmc_cube(prec, m_nbPlaces);
+ SylvanWrapper::lddmc_refs_push(_minus);
+ MDD _plus = SylvanWrapper::lddmc_cube(postc, m_nbPlaces);
+ SylvanWrapper::lddmc_refs_push(_plus);
+ m_tb_relation.push_back(TransSylvan(_minus, _plus));
+ }
+ delete[] prec;
+ delete[] postc;
+
}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index a866a05..da68e0b 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -24,7 +24,6 @@ class CommonSOG
CommonSOG();
virtual ~CommonSOG();
static LDDGraph *getGraph();
-
inline set<uint16_t> & getPlaceProposition() {return m_place_proposition;}
inline string_view getTransition(int pos) {
{
@@ -33,8 +32,11 @@ class CommonSOG
}
static string_view getPlace(int pos);
void finish() {m_finish=true;}
+ virtual void computeDSOG(LDDGraph &g) { };
protected:
- NewNet* m_net;
+ void initializeLDD();
+ void loadNetFromFile();
+ const NewNet* m_net;
int m_nbPlaces = 0;
static LDDGraph *m_graph;
vector<TransSylvan> m_tb_relation;
@@ -57,7 +59,6 @@ class CommonSOG
std::mutex m_graph_mutex,m_gc_mutex;
atomic<uint8_t> m_gc;
volatile bool m_finish=false;
- //MDD fireTransition(MDD cmark,MDD minus, MDD plus);
private:
};
diff --git a/src/DistributedSOG.h b/src/DistributedSOG.h
index 4fe634a..b62e1ab 100644
--- a/src/DistributedSOG.h
+++ b/src/DistributedSOG.h
@@ -15,7 +15,7 @@
#include "TransSylvan.h"
#include <mpi.h>
-#include <sha2.h>
+#include <misc/sha2.h>
#include <stdio.h>
#include <sys/ipc.h>
#include <sys/shm.h>
diff --git a/src/HybridKripke.cpp b/src/Hybrid/HybridKripke.cpp
similarity index 94%
rename from src/HybridKripke.cpp
rename to src/Hybrid/HybridKripke.cpp
index 1a2765a..5b70eee 100644
--- a/src/HybridKripke.cpp
+++ b/src/Hybrid/HybridKripke.cpp
@@ -27,7 +27,7 @@ HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr): spot::kripke(dict_ptr)
HybridKripkeIterator::m_div.Successors.push_back(pair<LDDState*,int>(&HybridKripkeIterator::m_div,-1));*/
}
-HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap,NewNet &net_):HybridKripke(dict_ptr) {
+HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr, set<string> &l_transap, set<string> &l_placeap, NewNet &net_): HybridKripke(dict_ptr) {
m_net=&net_;
HybridKripkeIterator::m_net=&net_;
for (auto it:l_transap) {
@@ -41,7 +41,7 @@ HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_tra
}
-state* HybridKripke::get_init_state() const {
+state* HybridKripke::get_init_state() const {
int v;
MPI_Send( &v, 1, MPI_INT, 0, TAG_INITIAL, MPI_COMM_WORLD);
char message[23];
diff --git a/src/HybridKripke.h b/src/Hybrid/HybridKripke.h
similarity index 85%
rename from src/HybridKripke.h
rename to src/Hybrid/HybridKripke.h
index 53f7fc9..4d43998 100644
--- a/src/HybridKripke.h
+++ b/src/Hybrid/HybridKripke.h
@@ -10,7 +10,7 @@
class HybridKripke: public spot::kripke {
public:
HybridKripke(const spot::bdd_dict_ptr& dict_ptr);
- HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap,NewNet &net_);
+ HybridKripke(const spot::bdd_dict_ptr& dict_ptr, set<string> &l_transap, set<string> &l_placeap, NewNet &net_);
virtual ~HybridKripke();
spot::state* get_init_state() const override;
HybridKripkeIterator* succ_iter(const spot::state* s) const override;
diff --git a/src/HybridKripkeIterator.cpp b/src/Hybrid/HybridKripkeIterator.cpp
similarity index 100%
rename from src/HybridKripkeIterator.cpp
rename to src/Hybrid/HybridKripkeIterator.cpp
diff --git a/src/HybridKripkeIterator.h b/src/Hybrid/HybridKripkeIterator.h
similarity index 100%
rename from src/HybridKripkeIterator.h
rename to src/Hybrid/HybridKripkeIterator.h
diff --git a/src/HybridKripkeState.cpp b/src/Hybrid/HybridKripkeState.cpp
similarity index 100%
rename from src/HybridKripkeState.cpp
rename to src/Hybrid/HybridKripkeState.cpp
diff --git a/src/HybridKripkeState.h b/src/Hybrid/HybridKripkeState.h
similarity index 100%
rename from src/HybridKripkeState.h
rename to src/Hybrid/HybridKripkeState.h
diff --git a/src/MCHybridSOG.cpp b/src/Hybrid/MCHybrid/MCHybridSOG.cpp
similarity index 87%
rename from src/MCHybridSOG.cpp
rename to src/Hybrid/MCHybrid/MCHybridSOG.cpp
index c1bc263..dd5980c 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/Hybrid/MCHybrid/MCHybridSOG.cpp
@@ -1,11 +1,9 @@
#include "MCHybridSOG.h"
//#define DEBUG_GC
-
#include <cstdio>
-
#include <openssl/md5.h>
-#include "md5_hash.h"
+#include "misc/md5_hash.h"
#define LENGTH_ID 16
//#define LENGTH_MSG 180
@@ -25,93 +23,18 @@
using namespace std;
MCHybridSOG::MCHybridSOG(const NewNet &R, MPI_Comm &comm_world, bool init) {
-
m_comm_world = comm_world;
- SylvanWrapper::sylvan_set_limits(16LL << 29, 8, 0);
-
- //sylvan_init_package();
- SylvanWrapper::sylvan_init_package();
- SylvanWrapper::sylvan_init_ldd();
- SylvanWrapper::init_gc_seq();
- SylvanWrapper::lddmc_refs_init();
- SylvanWrapper::displayMDDTableInfo();
+ initializeLDD();
m_net = &R;
-
m_init = init;
m_nbPlaces = R.places.size();
- int i, domain;
- vector<Place>::const_iterator it_places;
-
- //#init_gc_seq();
- //_______________
- m_transitions = R.transitions;
- m_observable = R.Observable;
- m_nonObservable = R.NonObservable;
- m_place_proposition = R.m_formula_place;
- m_transitionName = &R.transitionName;
- m_placeName = &R.m_placePosName;
- InterfaceTrans = R.InterfaceTrans;
-
- m_nbPlaces = R.places.size();
- cout << "Nombre de places : " << m_nbPlaces << endl;
- cout << "Derniere place : " << R.places[m_nbPlaces - 1].name << endl;
- // place domain, place bvect, place initial marking and place name
-
- uint32_t *liste_marques = new uint32_t[R.places.size()];
- for (i = 0, it_places = R.places.begin(); it_places != R.places.end(); i++, it_places++) {
- liste_marques[i] = it_places->marking;
- }
- m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, R.places.size());
- //SylvanWrapper::lddmc_refs_push( m_initialMarking );
-
- delete[]liste_marques;
- // place names
-
-
-
- auto *prec = new uint32_t[m_nbPlaces];
- auto *postc = new uint32_t[m_nbPlaces];
- // Transition relation
-
- for (vector<Transition>::const_iterator t = R.transitions.begin();
- t != R.transitions.end(); t++) {
- // Initialisation
- for (i = 0; i < m_nbPlaces; i++) {
- prec[i] = 0;
- postc[i] = 0;
- }
- // Calculer les places adjacentes a la transition t
- set<int> adjacentPlace;
- for (vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++) {
- adjacentPlace.insert(it->first);
- prec[it->first] = prec[it->first] + it->second;
-
- }
- // arcs post
- for (auto it : t->post) {
- adjacentPlace.insert(it.first);
- postc[it.first] = postc[it.first] + it.second;
- }
-
- MDD _minus = SylvanWrapper::lddmc_cube(prec, m_nbPlaces);
- //SylvanWrapper::lddmc_refs_push ( _minus );
-
- MDD _plus = SylvanWrapper::lddmc_cube(postc, m_nbPlaces);
- // SylvanWrapper::lddmc_refs_push ( _plus );
- m_tb_relation.emplace_back(TransSylvan(_minus, _plus));
- }
- //sylvan_gc_seq();
- delete[] prec;
- delete[] postc;
-
+ loadNetFromFile();
}
void *MCHybridSOG::doCompute() {
int id_thread;
-
id_thread = m_id_thread++;
-
unsigned char Identif[20];
m_Terminated = false;
@@ -242,7 +165,6 @@ void *MCHybridSOG::doCompute() {
if (destination == task_id) {
bool res = false;
- //= m_graph->insertFind(reached_class);
LDDState *pos = m_graph->insertFindByMDD(ldd_reachedclass, res);
if (!res) {
pos->setProcess(task_id);
diff --git a/src/MCHybridSOG.h b/src/Hybrid/MCHybrid/MCHybridSOG.h
similarity index 94%
rename from src/MCHybridSOG.h
rename to src/Hybrid/MCHybrid/MCHybridSOG.h
index 4351764..202f5e6 100644
--- a/src/MCHybridSOG.h
+++ b/src/Hybrid/MCHybrid/MCHybridSOG.h
@@ -15,7 +15,7 @@
#include "TransSylvan.h"
#include <mpi.h>
-#include <sha2.h>
+#include <misc/sha2.h>
#include <sys/ipc.h>
#include <sys/shm.h>
@@ -33,7 +33,7 @@
#include <thread>
#include <mutex>
#include <condition_variable>
-#include "SafeDequeue.h"
+#include "misc/SafeDequeue.h"
// namespace mpi = boost::mpi;
//#define MASTER 0
@@ -51,7 +51,7 @@ enum class state {waitInitial,waitingBuild,waitingSucc};
class MCHybridSOG : public CommonSOG
{
public:
- MCHybridSOG(const NewNet &,MPI_Comm &, bool init = false);
+ MCHybridSOG(const NewNet &, MPI_Comm &, bool init = false);
void buildFromNet(int index);
/// principal functions to construct the SOG
void computeDSOG(LDDGraph &g);
diff --git a/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp b/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
new file mode 100644
index 0000000..7bfd2d7
--- /dev/null
+++ b/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
@@ -0,0 +1,456 @@
+#include "MCHybridSOGReq.h"
+//#define DEBUG_GC
+
+#include <cstdio>
+#include <openssl/md5.h>
+#include "misc/md5_hash.h"
+
+#define LENGTH_ID 16
+//#define LENGTH_MSG 180
+#define TAG_STATE 1
+#define TAG_FINISH 2
+#define TAG_INITIAL 3
+#define TAG_ASK_SUCC 4
+
+
+#define TAG_ACK_INITIAL 8
+#define TAG_ASK_STATE 9
+#define TAG_ACK_STATE 10
+#define TAG_ACK_SUCC 11
+
+//#define DEBUG_GC 1
+#define REDUCE 1
+using namespace std;
+
+MCHybridSOGReq::MCHybridSOGReq(const NewNet &R, MPI_Comm &comm_world, bool init) {
+ m_comm_world = comm_world;
+ initializeLDD();
+ m_net = &R;
+ m_init = init;
+ loadNetFromFile();
+}
+
+void *MCHybridSOGReq::doCompute() {
+
+ int id_thread;
+ id_thread = m_id_thread++;
+ unsigned char Identif[20];
+ m_Terminated = false;
+
+ /****************************************** initial state ********************************************/
+ if (task_id == 0 && id_thread == 0) {
+ string *chaine = new string();
+ LDDState *c = new LDDState;
+ MDD Complete_meta_state = Accessible_epsilon(m_initialMarking);
+ c->m_lddstate = Complete_meta_state;
+ SylvanWrapper::convert_wholemdd_stringcpp(Complete_meta_state, *chaine);
+ md5_hash::compute(*chaine, Identif);
+
+ auto destination = (uint16_t) (Identif[0] % n_tasks);
+ c->setProcess(destination);
+ if (destination == 0) {
+ m_nbmetastate++;
+ Set fire = firable_obs(Complete_meta_state);
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
+ memcpy(c->m_SHA2, Identif, 16);
+ m_common_stack.push(Pair(couple(c, Complete_meta_state), fire));
+ m_condStack.notify_one();
+ } else {
+ MDD initialstate = Complete_meta_state;
+ m_graph->insertSHA(c);
+ memcpy(c->m_SHA2, Identif, 16);
+ initialstate = Canonize(Complete_meta_state, 0);
+ //initialstate = Complete_meta_state;
+ SylvanWrapper::convert_wholemdd_stringcpp(initialstate, *chaine);
+ m_tosend_msg.push(MSG(chaine, destination));
+
+ }
+ }
+
+
+
+
+ /******************************* envoie et reception des aggregats ************************************/
+ string chaine;
+ if (id_thread == 0) {
+ do {
+ send_state_message();
+ read_message();
+ if (m_waitingBuildSucc == statereq::waitingBuild) {
+ bool res;
+ size_t pos = m_graph->findSHAPos(m_id_md5, res);
+ if (res) {
+ m_waitingBuildSucc = statereq::waitingSucc;
+ m_aggWaiting = m_graph->getLDDStateById(pos);
+ }
+ }
+ if (m_waitingBuildSucc == statereq::waitingSucc) {
+ if (m_aggWaiting->isCompletedSucc()) {
+ m_waitingBuildSucc = statereq::waitInitial;
+ sendSuccToMC();
+ }
+ }
+ if (m_waitingAgregate) {
+ bool res = false;
+ size_t pos = m_graph->findSHAPos(m_id_md5, res);
+ if (res) {
+ m_waitingAgregate = false;
+ sendPropToMC(pos);
+ }
+ }
+
+ } while (!m_Terminated);
+
+ }
+ /******************************* Construction des aggregats ************************************/
+
+ else {
+ while (!m_Terminated) {
+ std::unique_lock<std::mutex> lk(m_mutexCond);
+ m_condStack.wait(lk, [this] { return !m_common_stack.empty() || !m_received_msg.empty() || m_Terminated; });
+ lk.unlock();
+
+ /*if ( id_thread>1 ) {
+ if ( ++m_gc==1 ) {
+ m_gc_mutex.lock();
+ }
+ }*/
+ if (!m_Terminated) {
+ Pair e;
+ if (m_common_stack.try_pop(e)) {
+ while (!e.second.empty() && !m_Terminated) {
+ int t = *(e.second.begin());
+ e.second.erase(t);
+ MDD ldd_reachedclass = Accessible_epsilon(get_successor(e.first.second, t));
+ // SylvanWrapper::lddmc_refs_push ( ldd_reachedclass );
+
+ //if ( id_thread==1 ) {
+ //displayMDDTableInfo();
+ //if ( SylvanWrapper::isGCRequired() ) {
+ // m_gc_mutex.lock();
+//#ifdef DEBUG_GC
+
+ // SylvanWrapper::displayMDDTableInfo();
+//#endif // DEBUG_GC
+ //SylvanWrapper::sylvan_gc_seq();
+//#ifdef DEBUG_GC
+
+ // SylvanWrapper::displayMDDTableInfo();
+//#endif // DEBUG_GC
+ //m_gc_mutex.unlock();
+ // }
+
+
+ //pthread_spin_unlock(&m_spin_md5);
+
+
+
+ //MDD Reduced=Canonize(ldd_reachedclass,0);
+ // ldd_refs_push(Reduced);
+
+ //MDD Reduced=ldd_reachedclass;
+ string *message_to_send1 = new string();
+ SylvanWrapper::convert_wholemdd_stringcpp(ldd_reachedclass, *message_to_send1);
+ md5_hash::compute(*message_to_send1, Identif);
+ uint16_t destination = (uint16_t) (Identif[0] % n_tasks);
+ /**************** construction local ******/
+ if (destination == task_id) {
+ bool res = false;
+ LDDState *pos = m_graph->insertFindByMDD(ldd_reachedclass, res);
+ if (!res) {
+ pos->setProcess(task_id);
+ pos->setDiv(Set_Div(ldd_reachedclass));
+ pos->setDeadLock(Set_Bloc(ldd_reachedclass));
+ memcpy(pos->m_SHA2, Identif, 16);
+ Set fire = firable_obs(pos->m_lddstate);
+ m_common_stack.push(Pair(couple(pos, pos->m_lddstate), fire));
+ m_condStack.notify_one();
+ }
+ m_graph->addArc();
+ {
+ std::scoped_lock<std::mutex> guard(m_graph_mutex);
+ e.first.first->Successors.insert(e.first.first->Successors.begin(),
+ LDDEdge(pos, t));
+ pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
+ }
+
+
+ }
+ /**************** construction externe ******/
+ else { // send to another process
+ LDDState *reached_class = new LDDState;
+ reached_class->m_lddstate = ldd_reachedclass;
+ reached_class->setProcess(destination);
+ LDDState *posV = m_graph->insertFindSha(Identif, reached_class);
+ if (!posV) {
+ MDD reached{ldd_reachedclass};
+ reached = Canonize(ldd_reachedclass, 0);
+ /*string *message_to_send2 = new string();
+ SylvanWrapper::convert_wholemdd_stringcpp(reached, *message_to_send2);*/
+ m_graph->addArc();
+ m_graph_mutex.lock();
+ e.first.first->Successors.insert(e.first.first->Successors.begin(),
+ LDDEdge(reached_class, t));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(),
+ LDDEdge(e.first.first, t));
+ m_graph_mutex.unlock();
+ // m_tosend_msg.push(MSG(message_to_send2, destination));
+
+ } else {
+ //cout<<"sha found "<<endl;
+ m_graph->addArc();
+ {
+ std::scoped_lock<std::mutex> guard(m_graph_mutex);
+ e.first.first->Successors.insert(e.first.first->Successors.begin(),
+ LDDEdge(posV, t));
+ posV->Predecessors.insert(posV->Predecessors.begin(), LDDEdge(e.first.first, t));
+ }
+ delete reached_class;
+ }
+ }
+ }
+ e.first.first->setCompletedSucc();
+ }
+
+ /******************************* Construction des aggregats � partir de pile de messages ************************************/
+ MSG popped_msg;
+ if (m_received_msg.try_pop(popped_msg)) {
+ MDD receivedLDD = decodage_message(popped_msg.first->c_str());
+ delete popped_msg.first;
+ MDD MState = Accessible_epsilon(receivedLDD);
+ bool res = false;
+ LDDState *Agregate = m_graph->insertFindByMDD(MState, res);
+ if (!res) {
+ Agregate->setDiv(Set_Div(MState));
+ Agregate->setDeadLock(Set_Bloc(MState));
+ Agregate->setProcess(task_id);
+ SylvanWrapper::convert_wholemdd_stringcpp(MState, chaine);
+ md5_hash::compute(chaine, Identif);
+ memcpy(Agregate->m_SHA2, Identif, 16);
+ Set fire = firable_obs(MState);
+ m_common_stack.push(Pair(couple(Agregate, MState), fire));
+ m_condStack.notify_one();
+ }
+ }
+
+ /* if ( id_thread>1 ) {
+ if ( --m_gc==0 ) {
+ m_gc_mutex.unlock();
+ }
+
+ }*/
+
+
+
+
+ // }
+
+ }
+ } /// End else
+
+ // cout<<"Working process "<<task_id<<" leaved...thread "<<id_thread<<endl;
+
+ }
+
+ // cout<<"Finnnnnn...."<<endl;
+}
+
+
+void MCHybridSOGReq::read_message() {
+ int flag = 0;
+ MPI_Iprobe(MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &flag, &m_status); // exist a msg to receiv?
+// int nbytes;
+// MPI_Get_count(&m_status, MPI_CHAR, &nbytes);
+// cout<<"Count of bytes "<<nbytes<<endl;
+ while (flag != 0) {
+
+ if (m_status.MPI_TAG == TAG_ASK_STATE) {
+
+ char mess[17];
+ MPI_Recv(mess, 16, MPI_BYTE, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
+ bool res;
+ m_waitingAgregate = false;
+ size_t pos = m_graph->findSHAPos(mess, res);
+ if (!res) {
+ m_waitingAgregate = true;
+ memcpy(m_id_md5, mess, 16);
+ } else {
+ sendPropToMC(pos);
+ }
+ //cout<<"TAG ASKSTATE completed by task "<<task_id<<" from "<<m_status.MPI_SOURCE<<endl;
+
+
+ } else if (m_status.MPI_TAG == TAG_ASK_SUCC) {
+ //cout<<"=============================TAG_ASK_SUCC received by task "<<task_id<<endl;
+ char mess[17];
+ MPI_Recv(mess, 16, MPI_BYTE, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
+ m_waitingBuildSucc = statereq::waitInitial;
+ bool res;
+
+ size_t pos = m_graph->findSHAPos(mess, res);
+
+ if (res) {
+ m_aggWaiting = m_graph->getLDDStateById(pos);
+ if (m_aggWaiting->isCompletedSucc()) {
+ sendSuccToMC();
+ } else {
+ m_waitingBuildSucc = statereq::waitingSucc;
+ }
+ } else {
+ m_waitingBuildSucc = statereq::waitingBuild;
+ memcpy(m_id_md5, mess, 16);
+ }
+ } else if (m_status.MPI_TAG == TAG_STATE) {
+ int nbytes;
+ MPI_Get_count(&m_status, MPI_CHAR, &nbytes);
+ char inmsg[nbytes + 1];
+ MPI_Recv(inmsg, nbytes, MPI_CHAR, m_status.MPI_SOURCE, TAG_STATE, MPI_COMM_WORLD, &m_status);
+ m_nbrecv++;
+ string *msg_receiv = new string(inmsg, nbytes);
+ m_received_msg.push(MSG(msg_receiv, 0));
+ m_condStack.notify_one();
+ } else if (m_status.MPI_TAG == TAG_FINISH) {
+ int v;
+ MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
+ m_Terminated = true;
+ m_condStack.notify_all();
+ } else if (m_status.MPI_TAG == TAG_INITIAL) {
+ int v;
+ MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
+ LDDState *i_agregate = m_graph->getInitialState();
+ char message[22];
+ memcpy(message, i_agregate->getSHAValue(), 16);
+ uint16_t id_p = i_agregate->getProcess();
+ memcpy(message + 16, &id_p, 2);
+ MPI_Send(message, 22, MPI_BYTE, m_status.MPI_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD);
+
+ }
+ MPI_Iprobe(MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &flag, &m_status);
+ }
+
+}
+
+
+/**
+ * send a message containing an aggregate
+ */
+void MCHybridSOGReq::send_state_message() {
+ MSG s;
+ while (m_tosend_msg.try_pop(s) && !m_Terminated) {
+ int message_size;
+ message_size = (int)s.first->size() + 1;
+ int destination = s.second;
+ //MPI_Request request;
+ read_message();
+ MPI_Send(s.first->c_str(), message_size, MPI_CHAR, destination, TAG_STATE, MPI_COMM_WORLD);
+ m_nbsend++;
+ m_size_mess += message_size;
+ delete s.first;
+ }
+}
+
+/*
+ * Creation of threads
+ */
+void MCHybridSOGReq::computeDSOG(LDDGraph &g) {
+ m_graph = &g;
+ MPI_Barrier(m_comm_world);
+ m_nb_thread = nb_th;
+ m_id_thread = 0;
+ m_nbrecv = 0;
+ m_nbsend = 0;
+ m_gc = 0;
+
+ for (uint8_t i = 0; i < m_nb_thread - 1; i++) {
+ m_list_thread[i] = new thread(threadHandler, this);
+ if (m_list_thread[i] == nullptr) {
+ cout << "error: thread creation failed..." << endl;
+ }
+ }
+ doCompute();
+ for (int i = 0; i < m_nb_thread - 1; i++) {
+ m_list_thread[i]->join();
+ delete m_list_thread[i];
+ }
+}
+
+
+MCHybridSOGReq::~MCHybridSOGReq() = default;
+
+/******************************************convert char ---> MDD ********************************************/
+
+MDD MCHybridSOGReq::decodage_message(const char *chaine) {
+ MDD M = lddmc_false;
+ unsigned int nb_marq = (((unsigned char) chaine[1] - 1) << 7) | ((unsigned char) chaine[0] >> 1);
+ //nb_marq = (nb_marq << 7) | ((unsigned char) chaine[0] >> 1);
+ unsigned int index = 2;
+ uint32_t list_marq[m_nbPlaces];
+ for (unsigned int i = 0; i < nb_marq; i++) {
+ for (unsigned int j = 0; j < m_nbPlaces; j++) {
+ list_marq[j] = (uint32_t) ((unsigned char) chaine[index] - 1);
+ index++;
+ }
+ MDD N = SylvanWrapper::lddmc_cube(list_marq, m_nbPlaces);
+ M = SylvanWrapper::lddmc_union_mono(M, N);
+ }
+ return M;
+}
+
+void *MCHybridSOGReq::threadHandler(void *context) {
+ return ((MCHybridSOGReq *) context)->doCompute();
+}
+
+
+void MCHybridSOGReq::sendSuccToMC() {
+ uint32_t nb_succ = m_aggWaiting->getSuccessors()->size();
+ uint32_t message_size = nb_succ * 20 + 4;
+ char mess_tosend[message_size];
+ memcpy(mess_tosend, &nb_succ, 4);
+ uint32_t i_message = 4;
+ //cout<<"***************************Number of succesors to send :"<<nb_succ<<endl;
+ for (uint32_t i = 0; i < nb_succ; i++) {
+ pair<LDDState *, int> elt;
+ elt = m_aggWaiting->getSuccessors()->at(i);
+ memcpy(mess_tosend + i_message, elt.first->getSHAValue(), 16);
+ i_message += 16;
+ uint16_t pcontainer = elt.first->getProcess();
+ memcpy(mess_tosend + i_message, &pcontainer, 2);
+ i_message += 2;
+ memcpy(mess_tosend + i_message, &(elt.second), 2);
+ i_message += 2;
+ }
+ read_message();
+ MPI_Send(mess_tosend, message_size, MPI_BYTE, n_tasks, TAG_ACK_SUCC, MPI_COMM_WORLD);
+
+}
+
+// Send propositions to Model checker
+void MCHybridSOGReq::sendPropToMC(size_t pos) {
+ LDDState *agg = m_graph->getLDDStateById(pos);
+ vector<uint16_t> marked_places = agg->getMarkedPlaces(m_place_proposition);
+ vector<uint16_t> unmarked_places = agg->getUnmarkedPlaces(m_place_proposition);
+ uint16_t s_mp = marked_places.size();
+ uint16_t s_up = unmarked_places.size();
+ char mess_to_send[8 + s_mp * 2 + s_up * 2 + 5];
+ memcpy(mess_to_send, &pos, 8);
+ size_t indice = 8;
+ memcpy(mess_to_send + indice, &s_mp, 2);
+ indice += 2;
+ for (auto it = marked_places.begin(); it != marked_places.end(); it++) {
+ memcpy(mess_to_send + indice, &(*it), 2);
+ indice += 2;
+ }
+ memcpy(mess_to_send + indice, &s_up, 2);
+ indice += 2;
+ for (auto it : unmarked_places) {
+ memcpy(mess_to_send + indice, &(it), 2);
+ indice += 2;
+ }
+ uint8_t divblock = agg->isDiv();
+ divblock = divblock | (agg->isDeadLock() << 1);
+ memcpy(mess_to_send + indice, &divblock, 1);
+ indice++;
+ read_message();
+ MPI_Send(mess_to_send, indice, MPI_BYTE, n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD);
+}
\ No newline at end of file
diff --git a/src/Hybrid/MCHybridReq/MCHybridSOGReq.h b/src/Hybrid/MCHybridReq/MCHybridSOGReq.h
new file mode 100644
index 0000000..c5c8bba
--- /dev/null
+++ b/src/Hybrid/MCHybridReq/MCHybridSOGReq.h
@@ -0,0 +1,94 @@
+#ifndef MCHybridSOGReq_H
+#define MCHybridSOGReq_H
+
+#include <stack>
+#include <vector>
+#include "NewNet.h"
+// #include "MDD.h"
+//#include "MDGraph.h"
+//#include "bvec.h"
+#include <pthread.h>
+#include <cstdio>
+#include <sys/types.h>
+#include <unistd.h>
+#include "LDDGraph.h"
+#include "TransSylvan.h"
+
+#include <mpi.h>
+#include <misc/sha2.h>
+
+#include <sys/ipc.h>
+#include <sys/shm.h>
+#include <sys/types.h>
+#include <cstdlib> //std::system
+#include <sstream>
+
+#include <iostream>
+#include <queue>
+#include <string>
+#include <ctime>
+#include <chrono>
+#include "CommonSOG.h"
+#include <atomic>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+#include "misc/SafeDequeue.h"
+// namespace mpi = boost::mpi;
+
+//#define MASTER 0
+//#define large 128
+extern unsigned int nb_th;
+extern int n_tasks, task_id;
+
+
+
+typedef pair<string *, unsigned int> MSG;
+
+typedef stack<MSG> pile_msg;
+enum class statereq {waitInitial,waitingBuild,waitingSucc};
+// typedef vector<Trans> vec_trans;
+class MCHybridSOGReq : public CommonSOG
+{
+public:
+ MCHybridSOGReq(const NewNet &, MPI_Comm &, bool init = false);
+ void buildFromNet(int index);
+ /// principal functions to construct the SOG
+ void computeDSOG(LDDGraph &g);
+ ~MCHybridSOGReq() override;
+ static void *threadHandler(void *context);
+ void *doCompute();
+protected:
+private:
+ std::condition_variable m_condStack;
+ mutable std::mutex m_mutexCond;
+ MPI_Comm m_comm_world;
+ void sendSuccToMC();
+ void sendPropToMC(size_t pos);
+ atomic<bool> m_waitingAgregate;// (false);
+ atomic<statereq> m_waitingBuildSucc;
+ char m_id_md5[16];
+ LDDState * m_aggWaiting=nullptr;
+ int m_nbmetastate;
+ SafeDequeue<Pair> m_common_stack;
+ SafeDequeue<MSG> m_received_msg;
+ SafeDequeue<MSG> m_tosend_msg;
+
+ int m_init;
+ /// Convert a string caracter to an MDD
+ MDD decodage_message(const char *chaine);
+ /// there is a message to receive?
+ void read_message();
+
+ /// receive state message
+ void send_state_message();
+ thread* m_list_thread[128];
+ atomic<uint8_t> m_id_thread;
+ volatile bool m_Terminated = false;
+ unsigned long m_size_mess = 0;
+ int m_nbsend = 0, m_nbrecv = 0;
+ MPI_Status m_status;
+
+};
+
+#endif // MCHybridSOGReq_H
diff --git a/src/HybridSOG.h b/src/HybridSOG.h
index 6e2e395..c0b1393 100644
--- a/src/HybridSOG.h
+++ b/src/HybridSOG.h
@@ -15,7 +15,7 @@
#include "TransSylvan.h"
#include <mpi.h>
-#include <sha2.h>
+#include <misc/sha2.h>
#include <stdio.h>
#include <sys/ipc.h>
#include <sys/shm.h>
diff --git a/src/ModelCheckThReq.cpp b/src/MCMultiCore/ModelCheckThReq.cpp
similarity index 67%
rename from src/ModelCheckThReq.cpp
rename to src/MCMultiCore/ModelCheckThReq.cpp
index 43e5358..333737d 100644
--- a/src/ModelCheckThReq.cpp
+++ b/src/MCMultiCore/ModelCheckThReq.cpp
@@ -24,75 +24,8 @@ getMaxMemoryTh() {
void ModelCheckThReq::preConfigure() {
//cout<<"Enter : "<<__func__ <<endl;
- SylvanWrapper::sylvan_set_limits(16LL << 30, 10, 0);
- SylvanWrapper::sylvan_init_package();
- SylvanWrapper::sylvan_init_ldd();
- SylvanWrapper::init_gc_seq();
- SylvanWrapper::lddmc_refs_init();
- SylvanWrapper::displayMDDTableInfo();
- int i;
- vector<Place>::const_iterator it_places;
-
- m_transitions = m_net->transitions;
- m_observable = m_net->Observable;
- m_place_proposition = m_net->m_formula_place;
- m_nonObservable = m_net->NonObservable;
-
- m_transitionName = &m_net->transitionName;
- m_placeName = &m_net->m_placePosName;
-
-
- InterfaceTrans = m_net->InterfaceTrans;
-
- cout << "Nombre de places : " << m_nbPlaces << endl;
- cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
-
- uint32_t *liste_marques = new uint32_t[m_net->places.size()];
- for (i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++) {
- liste_marques[i] = it_places->marking;
- }
-
- m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, m_net->places.size());
- SylvanWrapper::lddmc_refs_push(m_initialMarking);
- delete[]liste_marques;
-
- uint32_t *prec = new uint32_t[m_nbPlaces];
- uint32_t *postc = new uint32_t[m_nbPlaces];
- // Transition relation
- for (auto t = m_net->transitions.begin();
- t != m_net->transitions.end(); t++) {
- // Initialisation
- for (i = 0; i < m_nbPlaces; i++) {
- prec[i] = 0;
- postc[i] = 0;
- }
- // Calculer les places adjacentes a la transition t
- set<int> adjacentPlace;
- for (vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++) {
- adjacentPlace.insert(it->first);
- prec[it->first] = prec[it->first] + it->second;
- //printf("It first %d \n",it->first);
- //printf("In prec %d \n",prec[it->first]);
- }
- // arcs post
- for (vector<pair<int, int> >::const_iterator it = t->post.begin(); it != t->post.end(); it++) {
- adjacentPlace.insert(it->first);
- postc[it->first] = postc[it->first] + it->second;
-
- }
- for (set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++) {
- MDD Precond = lddmc_true;
- Precond = Precond & ((*it) >= prec[*it]);
- }
-
- MDD _minus = SylvanWrapper::lddmc_cube(prec, m_nbPlaces);
- SylvanWrapper::lddmc_refs_push(_minus);
- MDD _plus = SylvanWrapper::lddmc_cube(postc, m_nbPlaces);
- SylvanWrapper::lddmc_refs_push(_plus);
- m_tb_relation.push_back(TransSylvan(_minus, _plus));
- }
- delete[] prec;
- delete[] postc;
+ initializeLDD();
+ loadNetFromFile();
}
/**
diff --git a/src/ModelCheckThReq.h b/src/MCMultiCore/ModelCheckThReq.h
similarity index 93%
rename from src/ModelCheckThReq.h
rename to src/MCMultiCore/ModelCheckThReq.h
index 51dfb7b..be6fc98 100644
--- a/src/ModelCheckThReq.h
+++ b/src/MCMultiCore/ModelCheckThReq.h
@@ -4,7 +4,7 @@
#include <atomic>
#include <mutex>
#include <thread>
-#include "SafeDequeue.h"
+#include "misc/SafeDequeue.h"
typedef pair<LDDState *, int> couple_th;
//typedef stack<pair<LDDState *,int>> pile_t;
diff --git a/src/ModelCheckerCPPThread.cpp b/src/MCMultiCore/ModelCheckerCPPThread.cpp
similarity index 57%
rename from src/ModelCheckerCPPThread.cpp
rename to src/MCMultiCore/ModelCheckerCPPThread.cpp
index 3f43d71..bb0dfae 100644
--- a/src/ModelCheckerCPPThread.cpp
+++ b/src/MCMultiCore/ModelCheckerCPPThread.cpp
@@ -23,83 +23,9 @@ getMaxMemoryV3() {
}
void ModelCheckerCPPThread::preConfigure() {
-
- /*lace_init ( 1, 0 );
- lace_startup ( 0, NULL, NULL );
- size_t max = 16LL<<34;
- if ( max > getMaxMemoryV3() ) {
- max = getMaxMemoryV3() /10*9;
- }*/
- SylvanWrapper::sylvan_set_limits(16LL << 30, 10, 0);
-
- //sylvan_init_package();
- SylvanWrapper::sylvan_init_package();
- SylvanWrapper::sylvan_init_ldd();
- SylvanWrapper::init_gc_seq();
- SylvanWrapper::displayMDDTableInfo();
-
- vector<Place>::const_iterator it_places;
- m_transitions = m_net->transitions;
- m_observable = m_net->Observable;
- m_place_proposition = m_net->m_formula_place;
- m_nonObservable = m_net->NonObservable;
-
- m_transitionName = &m_net->transitionName;
- m_placeName = &m_net->m_placePosName;
-
- InterfaceTrans = m_net->InterfaceTrans;
-
- cout << "Nombre de places : " << m_nbPlaces << endl;
- cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
-
- uint32_t *liste_marques = new uint32_t[m_net->places.size()];
- uint32_t i;
- for (i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++) {
- liste_marques[i] = it_places->marking;
- }
-
- m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, m_net->places.size());
- SylvanWrapper::lddmc_refs_push(m_initialMarking);
-
- uint32_t *prec = new uint32_t[m_nbPlaces];
- uint32_t *postc = new uint32_t[m_nbPlaces];
- // Transition relation
- for (vector<Transition>::const_iterator t = m_net->transitions.begin(); t != m_net->transitions.end(); t++) {
- // Initialisation
- for (i = 0; i < m_nbPlaces; i++) {
- prec[i] = 0;
- postc[i] = 0;
- }
- // Calculer les places adjacentes a la transition t
- set<int> adjacentPlace;
- for (vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++) {
- adjacentPlace.insert(it->first);
- prec[it->first] = prec[it->first] + it->second;
- //printf("It first %d \n",it->first);
- //printf("In prec %d \n",prec[it->first]);
- }
- // arcs post
- for (auto it = t->post.begin(); it != t->post.end(); it++) {
- adjacentPlace.insert(it->first);
- postc[it->first] = postc[it->first] + it->second;
-
- }
- for (set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++) {
- MDD Precond = lddmc_true;
- Precond = Precond & ((*it) >= prec[*it]);
- }
-
- MDD _minus = SylvanWrapper::lddmc_cube(prec, m_nbPlaces);
- SylvanWrapper::lddmc_refs_push(_minus);
- MDD _plus = SylvanWrapper::lddmc_cube(postc, m_nbPlaces);
- SylvanWrapper::lddmc_refs_push(_plus);
- m_tb_relation.emplace_back(TransSylvan(_minus, _plus));
- }
- delete[] prec;
- delete[] postc;
+ initializeLDD();
+ loadNetFromFile();
ComputeTh_Succ();
-
-
}
diff --git a/src/ModelCheckerCPPThread.h b/src/MCMultiCore/ModelCheckerCPPThread.h
similarity index 93%
rename from src/ModelCheckerCPPThread.h
rename to src/MCMultiCore/ModelCheckerCPPThread.h
index da96837..4761e58 100644
--- a/src/ModelCheckerCPPThread.h
+++ b/src/MCMultiCore/ModelCheckerCPPThread.h
@@ -1,8 +1,8 @@
#ifndef ModelCheckerCPPThread_H
#define ModelCheckerCPPThread_H
#include "ModelCheckBaseMT.h"
-#include "stacksafe.h"
-#include "SafeDequeue.h"
+#include "misc/stacksafe.h"
+#include "misc/SafeDequeue.h"
#include <atomic>
#include <thread>
#include <mutex>
diff --git a/src/ModelCheckerTh.cpp b/src/MCMultiCore/ModelCheckerTh.cpp
similarity index 66%
rename from src/ModelCheckerTh.cpp
rename to src/MCMultiCore/ModelCheckerTh.cpp
index 80b1db9..fed67f6 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/MCMultiCore/ModelCheckerTh.cpp
@@ -13,77 +13,9 @@ getMaxMemory()
return pages * page_size;
}
void ModelCheckerTh::preConfigure() {
-
- SylvanWrapper::sylvan_set_limits ( 16LL<<30, 10, 0 );
- SylvanWrapper::sylvan_init_package();
- SylvanWrapper::sylvan_init_ldd();
- SylvanWrapper::init_gc_seq();
- SylvanWrapper::displayMDDTableInfo();
-
- vector<Place>::const_iterator it_places;
-
- //init_gc_seq();
-
-
- m_transitions = m_net->transitions;
- m_observable = m_net->Observable;
- m_place_proposition = m_net->m_formula_place;
- m_nonObservable = m_net->NonObservable;
-
- m_transitionName = &m_net->transitionName;
- m_placeName = &m_net->m_placePosName;
-
- InterfaceTrans = m_net->InterfaceTrans;
-
- cout << "Nombre de places : " << m_nbPlaces << endl;
- cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
-
- uint32_t *liste_marques = new uint32_t[m_net->places.size()];
- uint32_t i;
- for (i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++) {
- liste_marques[i] = it_places->marking;
- }
-
- m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, m_net->places.size());
- //ldd_refs_push(m_initialMarking);
- uint32_t *prec = new uint32_t[m_nbPlaces];
- uint32_t *postc = new uint32_t[m_nbPlaces];
- // Transition relation
- for (vector<Transition>::const_iterator t = m_net->transitions.begin(); t != m_net->transitions.end(); t++) {
- // Initialisation
- for (i = 0; i < m_nbPlaces; i++) {
- prec[i] = 0;
- postc[i] = 0;
- }
- // Calculer les places adjacentes a la transition t
- set<int> adjacentPlace;
- for (vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++) {
- adjacentPlace.insert(it->first);
- prec[it->first] = prec[it->first] + it->second;
- //printf("It first %d \n",it->first);
- //printf("In prec %d \n",prec[it->first]);
- }
- // arcs post
- for (vector<pair<int, int> >::const_iterator it = t->post.begin(); it != t->post.end(); it++) {
- adjacentPlace.insert(it->first);
- postc[it->first] = postc[it->first] + it->second;
-
- }
- for (set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++) {
- MDD Precond = lddmc_true;
- Precond = Precond & ((*it) >= prec[*it]);
- }
-
- MDD _minus = SylvanWrapper::lddmc_cube(prec, m_nbPlaces);
- //#ldd_refs_push(_minus);
- MDD _plus = SylvanWrapper::lddmc_cube(postc, m_nbPlaces);
- //#ldd_refs_push(_plus);
- m_tb_relation.push_back(TransSylvan(_minus, _plus));
- }
- delete[] prec;
- delete[] postc;
+ initializeLDD();
+ loadNetFromFile();
ComputeTh_Succ();
-
}
void* ModelCheckerTh::Compute_successors() {
diff --git a/src/ModelCheckerTh.h b/src/MCMultiCore/ModelCheckerTh.h
similarity index 100%
rename from src/ModelCheckerTh.h
rename to src/MCMultiCore/ModelCheckerTh.h
diff --git a/src/main.cpp b/src/main.cpp
index 4aa400d..91c4031 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -7,12 +7,12 @@
#include "LDDGraph.h"
-#include "ModelCheckerCPPThread.h"
-#include "ModelCheckerTh.h"
-#include "ModelCheckThReq.h"
+#include "MCMultiCore/ModelCheckerCPPThread.h"
+#include "MCMultiCore/ModelCheckerTh.h"
+#include "MCMultiCore/ModelCheckThReq.h"
#include "threadSOG.h"
#include "HybridSOG.h"
-#include "MCHybridSOG.h"
+#include "Hybrid/MCHybrid/MCHybridSOG.h"
#include <spot/misc/version.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/tl/parse.hh>
@@ -28,7 +28,8 @@
#include "SogKripke.h"
#include "SogKripkeTh.h"
-#include "HybridKripke.h"
+#include "Hybrid/HybridKripke.h"
+#include "Hybrid/MCHybridReq/MCHybridSOGReq.h"
#include "SylvanWrapper.h"
#include "PMCSOGConfig.h"
// #include "RdPBDD.h"
@@ -128,8 +129,9 @@ int main(int argc, char **argv) {
cout << "Multi-threaded algorithm based on C++ Thread library!" << endl;
cout << "Building automata for not(formula)\n";
auto d = spot::make_bdd_dict();
+ spot::translator obj=spot::translator(d);
- spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ spot::twa_graph_ptr af = obj.run(not_f);
cout << "Formula automata built.\n";
ModelCheckBaseMT *mcl;
@@ -256,7 +258,7 @@ int main(int argc, char **argv) {
if (nb_th > 1) {
if (task_id == 0)
cout << "**************Hybrid version**************** \n" << endl;
- if (strcmp(argv[1], "otf")) {
+ if (strcmp(argv[1], "otf") && strcmp(argv[1], "otfPR") ) {
HybridSOG DR(Rnewnet);
LDDGraph g(&DR);
if (task_id == 0)
@@ -274,9 +276,14 @@ int main(int argc, char **argv) {
//cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
if (task_id != n_tasks) {
cout << "N task :" << n_tasks << endl;
- MCHybridSOG DR(Rnewnet, gprocess, false);
- LDDGraph g(&DR);
- DR.computeDSOG(g);
+ CommonSOG* DR;
+ if (strcmp(argv[1], "otf")==0) DR= new MCHybridSOG(Rnewnet, gprocess, false);
+ else {
+ cout<<"Progressive construction..."<<endl;
+ DR= new MCHybridSOGReq(Rnewnet, gprocess, false);
+ }
+ LDDGraph g(DR);
+ DR->computeDSOG(g);
} else {
cout << "************************************" << endl;
cout << "On the fly Model checker by process " << task_id << endl;
@@ -301,12 +308,6 @@ int main(int argc, char **argv) {
auto finalTime = std::chrono::high_resolution_clock::now();
displayTime(startTime, finalTime);
displayCheckResult(res);
- /*spot::couvreur99_check check = spot::couvreur99_check(product);
- auto startTime = std::chrono::steady_clock::now();
- bool res = (check.check() == 0);
- auto finalTime = std::chrono::steady_clock::now();
- displayTime(startTime, finalTime);
- displayCheckResult(res);*/
} else {
auto startTime = std::chrono::steady_clock::now();
bool res = (k->intersecting_run(af) == 0);
@@ -314,34 +315,8 @@ int main(int argc, char **argv) {
displayTime(startTime, finalTime);
displayCheckResult(res);
}
-
- /*if (auto run = k->intersecting_run(af))
- {
- std::cout << "formula is violated by the following run:\n"<<*run<<endl;
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
- cout<<"=================================="<<endl;
- }
- else
- {
- std::cout << "formula is verified\n";
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
-
- }*/
}
}
- } else {
- /*cout << "*************Distibuted version******************* \n" << endl;
- {
- DistributedSOG DR(Rnewnet);cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
- LDDGraph g(nullptr);
- DR.computeDSOG(g);
- }*/
}
}
MPI_Finalize();
diff --git a/src/SafeDequeue.cpp b/src/misc/SafeDequeue.cpp
similarity index 100%
rename from src/SafeDequeue.cpp
rename to src/misc/SafeDequeue.cpp
diff --git a/src/SafeDequeue.h b/src/misc/SafeDequeue.h
similarity index 100%
rename from src/SafeDequeue.h
rename to src/misc/SafeDequeue.h
diff --git a/src/md5_hash.h b/src/misc/md5_hash.h
similarity index 100%
rename from src/md5_hash.h
rename to src/misc/md5_hash.h
diff --git a/src/sha2.c b/src/misc/sha2.c
similarity index 100%
rename from src/sha2.c
rename to src/misc/sha2.c
diff --git a/src/sha2.h b/src/misc/sha2.h
similarity index 100%
rename from src/sha2.h
rename to src/misc/sha2.h
diff --git a/src/stacksafe.cpp b/src/misc/stacksafe.cpp
similarity index 100%
rename from src/stacksafe.cpp
rename to src/misc/stacksafe.cpp
diff --git a/src/stacksafe.h b/src/misc/stacksafe.h
similarity index 100%
rename from src/stacksafe.h
rename to src/misc/stacksafe.h
--
GitLab