diff --git a/CMakeLists.txt b/CMakeLists.txt
index eb31e4d9f2804f346645b15cafe7d2974802cdc5..d56af45406dc07a86c6e3c47f104c610985113e4 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -3,6 +3,9 @@ cmake_minimum_required(VERSION 3.8 FATAL_ERROR)
# project name and language
project(pmc-sog C CXX)
+project(pmc-sog VERSION 0.4.0)
+
+configure_file(PMCSOGConfig.h.in src/PMCSOGConfig.h)
#set(CMAKE_CXX_STANDARD 14)
@@ -12,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") #-Og
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread -g3")#-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/PMCSOGConfig.h.in b/PMCSOGConfig.h.in
new file mode 100644
index 0000000000000000000000000000000000000000..837c7b2c8caff27babb76b643575054aed371fce
--- /dev/null
+++ b/PMCSOGConfig.h.in
@@ -0,0 +1,3 @@
+#define PMCSOG_VERSION_MAJOR @pmc-sog_VERSION_MAJOR@
+#define PMCSOG_VERSION_MINOR @pmc-sog_VERSION_MINOR@
+#define PMCSOG_VERSION_PATCH @pmc-sog_VERSION_PATCH@
\ No newline at end of file
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 90327eb43d168ef0581fccbb5a9da89a0fa78e0a..f4deee428652c9431dc47cc7314d57822a7f9ce4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -21,6 +21,7 @@ else()
set_target_properties(bddx PROPERTIES IMPORTED_LOCATION ${SPOT_LIBRARY})
endif()
+
# Hybrid SOG executable
add_executable(mc-sog main.cpp
NewNet.cpp
@@ -73,7 +74,9 @@ add_executable(mc-sog main.cpp
threadSOG.cpp threadSOG.h
HybridSOG.cpp HybridSOG.h
MCHybridSOG.cpp MCHybridSOG.h
- ModelCheckThReq.cpp ModelCheckThReq.h)
+ ModelCheckThReq.cpp ModelCheckThReq.h md5_hash.h )
+
+target_include_directories(mc-sog PUBLIC "${PROJECT_BINARY_DIR}")
target_link_libraries(mc-sog
bddx
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 45c52184139a1fcd9952807007f0389eb934417a..3bf63d04027488a97f1b247047837066e540c1d0 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -2,20 +2,10 @@
#include "SylvanWrapper.h"
#include "CommonSOG.h"
-#include <stack>
+CommonSOG::CommonSOG() =default;
+CommonSOG::~CommonSOG() =default;
-
-const vector<class Place> *_places = NULL;
-
-CommonSOG::CommonSOG() {
- //ctor
-}
-
-CommonSOG::~CommonSOG() {
- //dtor
-}
-
-LDDGraph *CommonSOG::getGraph() const {
+LDDGraph *CommonSOG::getGraph() {
return m_graph;
}
@@ -23,16 +13,12 @@ MDD CommonSOG::Accessible_epsilon(MDD From) {
MDD M1;
MDD M2 = From;
do {
-
M1 = M2;
- for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
+ for (auto i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
//fireTransition
MDD succ = SylvanWrapper::lddmc_firing_mono(M2, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
-
M2 = SylvanWrapper::lddmc_union_mono(M2, succ);
-
}
-
} while (M1 != M2);
return M2;
}
@@ -40,13 +26,11 @@ MDD CommonSOG::Accessible_epsilon(MDD From) {
// Return the set of firable observable transitions from an agregate
Set CommonSOG::firable_obs(MDD State) {
Set res;
- for (Set::const_iterator i = m_observable.begin(); !(i == m_observable.end()); i++) {
- //cout<<"firable..."<<endl;
- MDD succ = SylvanWrapper::lddmc_firing_mono(State, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ for (auto i : m_observable) {
+ MDD succ = SylvanWrapper::lddmc_firing_mono(State, m_tb_relation[i].getMinus(), m_tb_relation[i].getPlus());
if (succ != lddmc_false) {
- res.insert(*i);
+ res.insert(i);
}
-
}
return res;
}
@@ -58,8 +42,8 @@ MDD CommonSOG::get_successor(MDD From, int t) {
MDD CommonSOG::ImageForward(MDD From) {
MDD Res = lddmc_false;
- for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
- MDD succ = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ for (auto i : m_nonObservable) {
+ MDD succ = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[i].getMinus(), m_tb_relation[i].getPlus());
Res = SylvanWrapper::lddmc_union_mono(Res, succ);
}
return Res;
@@ -115,7 +99,7 @@ MDD CommonSOG::Canonize(MDD s, unsigned int level) {
}
- MDD Repr = lddmc_false;
+ MDD Repr;
if (SylvanWrapper::isSingleMDD(s0)) {
Repr = s0;
@@ -137,28 +121,6 @@ MDD CommonSOG::Canonize(MDD s, unsigned int level) {
}
-void CommonSOG::printhandler(ostream &o, int var) {
- o << (*_places)[var / 2].name;
- if (var % 2) {
- o << "_p";
- }
-}
-
-
-vector<TransSylvan> *CommonSOG::getTBRelation() {
- return &m_tb_relation;
-}
-
-Set *CommonSOG::getNonObservable() {
- return &m_nonObservable;
-}
-
-
-/*********Returns the count of places******************************************/
-unsigned int CommonSOG::getPlacesCount() {
- return m_nbPlaces;
-}
-
/**** Detect divergence in an agregate ****/
bool CommonSOG::Set_Div(MDD &M) const {
@@ -167,8 +129,7 @@ bool CommonSOG::Set_Div(MDD &M) const {
}
Set::const_iterator i;
MDD Reached, From;
- //cout<<"Ici detect divergence \n";
- Reached = lddmc_false;
+
From = M;
do {
Reached = lddmc_false;
@@ -178,12 +139,7 @@ bool CommonSOG::Set_Div(MDD &M) const {
}
if (Reached == From) {
- /*MDD Reached_obs=lddmc_false;
- for (i = m_observable.begin(); !(i == m_observable.end()) && (Reached_obs==lddmc_false); i++) {
- Reached_obs= fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
- }
- if (Reached_obs==lddmc_false) return true;*/
- return true;
+ return true;
}
From = Reached;
} while (Reached != lddmc_false);
@@ -194,9 +150,9 @@ bool CommonSOG::Set_Div(MDD &M) const {
bool CommonSOG::Set_Bloc(MDD &M) const {
MDD cur = lddmc_true;
- for (vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i != m_tb_relation.end(); i++) {
+ for (auto i : m_tb_relation) {
- cur = cur & (TransSylvan(*i).getMinus());
+ cur = cur & (i.getMinus());
}
return ((M & cur) != lddmc_false);
@@ -206,12 +162,7 @@ bool CommonSOG::Set_Bloc(MDD &M) const {
LDDGraph *CommonSOG::m_graph;
-struct elt_t {
- MDD cmark;
- MDD minus;
- MDD plus;
- uint32_t level;
-};
+
/*MDD CommonSOG::fireTransition(MDD cmark, MDD minus, MDD plus) {
return SylvanWrapper::lddmc_firing_mono(cmark,minus,plus);
@@ -224,7 +175,6 @@ struct elt_t {
//}
string_view CommonSOG::getPlace(int pos) {
- // cout<<"yes it is : "<<m_transitions.at(pos).name<<endl;
- // cout<<"Ok "<<m_graph->getPlace(pos)<<endl;
+
return string_view {m_graph->getPlace(pos)};
}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 1598c5b00382111ba9032432e4e7e87f6b25f866..a866a05f3baa9cb728e6659ff1232fff8a40efd9 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -23,20 +23,16 @@ class CommonSOG
public:
CommonSOG();
virtual ~CommonSOG();
- LDDGraph *getGraph() const;
- static void printhandler(ostream &o, int var);
- vector<TransSylvan>* getTBRelation();
- Set * getNonObservable();
- unsigned int getPlacesCount();
+ static LDDGraph *getGraph();
+
inline set<uint16_t> & getPlaceProposition() {return m_place_proposition;}
inline string_view getTransition(int pos) {
{
return string_view {m_transitions.at(pos).name};
}
}
- string_view getPlace(int pos);
-
-
+ static string_view getPlace(int pos);
+ void finish() {m_finish=true;}
protected:
NewNet* m_net;
int m_nbPlaces = 0;
@@ -60,6 +56,7 @@ class CommonSOG
uint8_t m_nb_thread;
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/HybridKripke.cpp b/src/HybridKripke.cpp
index 9194765858bd6a9e4d83d65b2d7c3771b8ed1eb9..1a2765ad61c3267238839bba2185f6a4f4cafa7b 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -30,12 +30,12 @@ HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr): spot::kripke(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.begin();it!=l_transap.end();it++) {
- register_ap(*it);
+ for (auto it:l_transap) {
+ register_ap(it);
}
- for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
- register_ap(*it);
+ for (auto it:l_placeap)
+ register_ap(it);
}
@@ -45,15 +45,13 @@ state* HybridKripke::get_init_state() const {
int v;
MPI_Send( &v, 1, MPI_INT, 0, TAG_INITIAL, MPI_COMM_WORLD);
char message[23];
- MPI_Status status; int nbytes;
+ MPI_Status status;
MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD, &status);
- MPI_Get_count(&status, MPI_BYTE, &v);
MPI_Recv(message, 22, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_INITIAL,MPI_COMM_WORLD, &status);
succ_t* elt=new succ_t;
memcpy(elt->id,message,16);
memcpy(&elt->pcontainer,message+16,2);
elt->_virtual=false;
-
return new HybridKripkeState(*elt);
}
@@ -69,15 +67,15 @@ std::string HybridKripke::format_state(const spot::state* s) const
HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
//cout<<__func__<<endl;
- auto ss = static_cast<const HybridKripkeState*>(s);
+ auto ss = static_cast<const HybridKripkeState*>(s);
bdd cond = state_condition(ss);
HybridKripkeState* st=ss;
if (iter_cache_)
{
- auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
+ /* auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
it->recycle(*st,cond);
- return it;
+ return it;*/
}
#ifdef TESTENABLE
SylvanWrapper::m_agg++;
diff --git a/src/HybridKripke.h b/src/HybridKripke.h
index d8caeb85d1c1f577816fd1038b50ac3b73239cea..53f7fc9282acda08e2192a0c5215aad14c03f220 100644
--- a/src/HybridKripke.h
+++ b/src/HybridKripke.h
@@ -9,7 +9,6 @@
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_);
virtual ~HybridKripke();
@@ -17,13 +16,9 @@ class HybridKripke: public spot::kripke {
HybridKripkeIterator* succ_iter(const spot::state* s) const override;
std::string format_state(const spot::state* s) const override;
bdd state_condition(const spot::state* s) const override;
-
- //ModelCheckBaseMT *m_builder;
-
protected:
private:
- std::map<int, int> place_prop;
NewNet *m_net;
};
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index 579cbb77078fdd334968833d6cb1b110fc3bb8ab..e6ffd20eefad6ed96394c227ec1bccebc0617e18 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -14,8 +14,7 @@ bool HybridKripkeIterator::first() {
//cout<<"entering "<<__func__<<endl;
m_current_edge=0;
-
- return m_current_state->getListSucc()->size()!=0;
+ return !m_current_state->getListSucc()->empty();
}
diff --git a/src/HybridKripkeIterator.h b/src/HybridKripkeIterator.h
index c56a8e84ebf5d8a59b99bdd53c44c58a6801829b..8e597d8cf1092eb1dc334eb9071cccc3857e06f4 100644
--- a/src/HybridKripkeIterator.h
+++ b/src/HybridKripkeIterator.h
@@ -8,8 +8,6 @@
class HybridKripkeIterator : public spot::kripke_succ_iterator
{
public:
- static LDDState m_deadlock;
- static LDDState m_div;
static NewNet * m_net;
static spot::bdd_dict_ptr* m_dict_ptr;
@@ -20,12 +18,12 @@ public:
bool next() override;
bool done() const override;
HybridKripkeState* dst() const override;
- bdd cond() const override final;
+ bdd cond() const override;
// HybridKripkeState* current_state() const;
void recycle(HybridKripkeState &st, bdd cond);
- std::string format_transition() const;
+
private:
diff --git a/src/HybridKripkeState.cpp b/src/HybridKripkeState.cpp
index 80744b5d4574debd040f2ace427435e1ed0acaef..7a8966a3c3577e4a6f81c286348fb86a8be8235b 100644
--- a/src/HybridKripkeState.cpp
+++ b/src/HybridKripkeState.cpp
@@ -1,12 +1,8 @@
#include <spot/kripke/kripke.hh>
-#include "LDDState.h"
#include "HybridKripkeState.h"
-HybridKripkeState::~HybridKripkeState()
-{
- //dtor
- //cout<<__func__<<endl;
-}
+HybridKripkeState::~HybridKripkeState()=default;
+
//static ModelCheckBaseMT * HybridKripkeState::m_builder;
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index e43146644de0486cda224461e004233c6e93adf7..14641f8bc3378b1194fde6be66152e4ac1247aee 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -7,9 +7,9 @@
#include "SylvanWrapper.h"
constexpr auto TAG_ASK_STATE = 9;
constexpr auto TAG_ACK_STATE = 10;
-#define TAG_ASK_SUCC 4
-#define TAG_ACK_SUCC 11
-#define TAG_NOTCOMPLETED 20
+constexpr auto TAG_ASK_SUCC = 4;
+constexpr auto TAG_ACK_SUCC = 11;
+
typedef struct {
char id[16];
int16_t transition;
@@ -23,7 +23,7 @@ public:
HybridKripkeState(succ_t &e):m_container(e.pcontainer) {
if (e._virtual) { //div or deadlock
- if (e.id[0]=='v') { // div
+ /*if (e.id[0]=='v') { // div
//cout<<"div created..."<<endl;
m_hashid=0xFFFFFFFFFFFFFFFE;
m_id[0]='v';
@@ -32,26 +32,25 @@ public:
elt.transition=-1;
elt._virtual=true;
m_succ.push_back(elt);
- }
- else {
+ }*/
+ /*else {*/
m_id[0]='d';
m_hashid=0xFFFFFFFFFFFFFFFF; // deadlock
- }
+ /* }*/
}
else {
- memcpy(m_id,e.id,16);
+ memcpy(m_id,e.id,16);
MPI_Send(m_id,16,MPI_BYTE,e.pcontainer, TAG_ASK_STATE, MPI_COMM_WORLD);
-
MPI_Status status; //int nbytes;
MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_STATE, MPI_COMM_WORLD, &status);
uint32_t nbytes;
MPI_Get_count(&status, MPI_BYTE, &nbytes);
// Receive hash id =idprocess | position
char message[nbytes];
+
MPI_Recv(message, nbytes, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_STATE,MPI_COMM_WORLD, &status);
- memcpy(&m_hashid,message,8);
- //cout<<"Pos :"<<m_hashid<<endl;
- //cout<<"Process :"<<m_container<<endl;
+
+ memcpy(&m_hashid,message,8);
m_hashid=m_hashid | (size_t(m_container)<<56);
// Determine Place propositions
@@ -84,9 +83,9 @@ public:
indice++; // Added for stats
memcpy(&m_size,message+indice,8); // Added for stats
- // Get successors
+ // Get successors
MPI_Send(m_id,16,MPI_BYTE,m_container, TAG_ASK_SUCC, MPI_COMM_WORLD);
-
+
// Receive list of successors
MPI_Probe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&status);
@@ -120,12 +119,7 @@ public:
el.transition=-1;
m_succ.push_back(el);
}
- if (m_div) {
- /*succ_t el;
- el.id[0]='v';
- el.transition=-1;
- el._virtual=true;
- m_succ.push_back(el);*/
+ if (m_div) {
succ_t el=e;
el._virtual=false;
el.transition=-1;
@@ -180,7 +174,6 @@ protected:
private:
char m_id[17];
- uint32_t m_pos; // Added for stats
size_t m_hashid;
bool m_div;
bool m_deadlock;
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index 495946519429f5a98a764cc65077762a59e2772b..7af8640b6c836042aa6fe579994b522745c017fa 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -1,66 +1,63 @@
#include "LDDGraph.h"
-
-#include <string.h>
+#include <cstring>
#include <map>
#include "SylvanWrapper.h"
-LDDGraph::~LDDGraph() {
- //dtor
-}
+LDDGraph::~LDDGraph()=default;
void LDDGraph::setInitialState(LDDState *c) {
- m_currentstate = m_initialstate = c;
+ m_initialstate = c;
}
-
/*----------------------find()----------------*/
LDDState *LDDGraph::find(LDDState *c) {
- std::lock_guard<std::mutex> lock(m_mutex);
+ std::shared_lock<std::shared_mutex> lock(m_mutex);
for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()); i++)
if (c->m_lddstate == (*i)->m_lddstate)
return *i;
- return NULL;
+ return nullptr;
}
-LDDState *LDDGraph::insertFind(LDDState *c) {
- LDDState *res = nullptr;
- std::lock_guard<std::mutex> lock(m_mutex);
- for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()) && res == nullptr; i++) {
- if (c->m_lddstate == (*i)->m_lddstate)
- res = *i;
+
+
+LDDState *LDDGraph::insertFindByMDD(MDD md, bool &found) {
+ std::lock_guard lock(m_mutex);
+ {
+
+ for (auto& i : m_GONodes) {
+ if (md == i->m_lddstate) {
+ found = true;
+ return i;
+ }
+ }
}
- if (res == nullptr) m_GONodes.push_back(c);
- return res;
+ LDDState *n = new LDDState;
+ n->m_lddstate = md;
+ found = false;
+ m_GONodes.push_back(n);
+ return n;
}
-/*----------------------find()----------------*/
-bool LDDGraph::cmpSHA(const unsigned char *s1, const unsigned char *s2) {
- bool res = true;
- for (int i = 0; i < 16 && res; i++) {
- res = (s1[i] == s2[i]);
- }
- return !res;
-}
LDDState *LDDGraph::findSHA(unsigned char *c) {
- std::lock_guard<std::mutex> lock(m_mutex_sha);
+ std::shared_lock<std::shared_mutex> lock(m_mutex);
for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()); i++)
if ((*i)->isVirtual() == true)
- if ((cmpSHA(c, (unsigned char *) (*i)->m_SHA2) == 0))
+ if (memcmp((char*)c, (char*) (*i)->m_SHA2,16) == 0)
return *i;
- return NULL;
+ return nullptr;
}
/*** Try to find an aggregate by its md5 code, else it is inserted***/
LDDState *LDDGraph::insertFindSha(unsigned char *c, LDDState *agg) {
LDDState *res = nullptr;
- std::lock_guard<std::mutex> lock(m_mutex_sha);
+ std::lock_guard<std::shared_mutex> lock(m_mutex);
for (auto i = m_GONodes.begin(); !(i == m_GONodes.end()) && !res; i++) {
if ((*i)->isVirtual() == true)
- if ((cmpSHA(c, (unsigned char *) (*i)->m_SHA2) == 0))
+ if (memcmp((char*)c, (char*) (*i)->m_SHA2,16) == 0)
res = *i;
}
if (res == nullptr) {
@@ -73,64 +70,39 @@ LDDState *LDDGraph::insertFindSha(unsigned char *c, LDDState *agg) {
/*--------------------------------------------*/
size_t LDDGraph::findSHAPos(unsigned char *c, bool &res) {
- size_t i = 0;
+ size_t i;
res = false;
+ std::shared_lock<std::shared_mutex> lock(m_mutex);
for (i = 0; i < m_GONodes.size(); i++)
- if ((cmpSHA(c, m_GONodes.at(i)->m_SHA2) == 0)) {
+ if (memcmp(c, m_GONodes.at(i)->m_SHA2,16) == 0) {
res = true;
return i;
}
- // cout<<__func__<<" : Aggregate not found!!!"<<endl;
return i;
}
/*----------------------insert() ------------*/
void LDDGraph::insert(LDDState *c) {
- std::lock_guard<std::mutex> lock(m_mutex);
+ std::lock_guard<std::shared_mutex> lock(m_mutex);
this->m_GONodes.push_back(c);
- //m_nbStates++;
}
/*----------------------insert() ------------*/
void LDDGraph::insertSHA(LDDState *c) {
c->setVirtual();
+ std::lock_guard<std::shared_mutex> lock(m_mutex);
this->m_GONodes.push_back(c);
}
-/*----------------------NbBddNod()------------------------*/
-int LDDGraph::NbBddNode(LDDState *S, size_t &nb) {
- /*if(S->m_visited==false)
- {
- //cout<<"insertion du meta etat numero :"<<nb<<"son id est :"<<S->class_state.id()<<endl;
- //cout<<"sa taille est :"<<bdd_nodecount(S->class_state)<<" noeuds \n";
- Tab[nb-1]=S->class_state;
- S->Visited=true;
- int bddnode=bdd_nodecount(S->class_state);
- int size_succ=0;
- for(Edges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++)
- {
- if((*i).first->Visited==false)
- {
- nb++;
- size_succ+=NbBddNode((*i).first,nb);
- }
- }
- return size_succ+bddnode;
-
- }
- else*/
- cout << "Not implemented yet...." << endl;
- return 0;
-}
/*----------------------Visualisation du graphe------------------------*/
void LDDGraph::printCompleteInformation() {
long count_ldd = 0L;
for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()); i++) {
count_ldd += SylvanWrapper::lddmc_nodecount((*i)->m_lddstate);
- m_nbMarking+= SylvanWrapper::getMarksCount((*i)->m_lddstate);
+ m_nbMarking += SylvanWrapper::getMarksCount((*i)->m_lddstate);
}
cout << "\n\nGRAPH SIZE : \n";
cout << "\n\tNB LDD NODES : " << count_ldd;
@@ -142,19 +114,19 @@ void LDDGraph::printCompleteInformation() {
cin >> c;*/
//InitVisit(initialstate,n);
- /* size_t n = 1;
- //cout<<"NB BDD NODE : "<<NbBdm_current_state->getContainerProcess()dNode(initialstate,n)<<endl;
- NbBddNode(m_initialstate, n);
- // cout<<"NB BDD NODE : "<<bdd_anodecount(m_Tab,(int)m_nbStates)<<endl;
- //cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
- InitVisit(m_initialstate, 1);
- //int toto;cin>>toto;
- //bdd Union=UnionMetaState(initialstate,1);
- //cout<<"a titre indicatif taille de l'union : "<<bdd_nodecount(Union)<<endl;
- if (c == 'y' || c == 'Y') {
- size_t n = 1;
- printGraph(m_initialstate, n);
- }*/
+ /* size_t n = 1;
+ //cout<<"NB BDD NODE : "<<NbBdm_current_state->getContainerProcess()dNode(initialstate,n)<<endl;
+ NbBddNode(m_initialstate, n);
+ // cout<<"NB BDD NODE : "<<bdd_anodecount(m_Tab,(int)m_nbStates)<<endl;
+ //cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
+ InitVisit(m_initialstate, 1);
+ //int toto;cin>>toto;
+ //bdd Union=UnionMetaState(initialstate,1);
+ //cout<<"a titre indicatif taille de l'union : "<<bdd_nodecount(Union)<<endl;
+ if (c == 'y' || c == 'Y') {
+ size_t n = 1;
+ printGraph(m_initialstate, n);
+ }*/
}
/*----------------------InitVisit()------------------------*/
@@ -196,16 +168,6 @@ void LDDGraph::printGraph(LDDState *s, size_t &nb) {
}
-/*---------void print_successors_class(Class_Of_State *)------------*/
-void LDDGraph::printsuccessors(LDDState *s) {
- cout << "Not implemented yet!" << endl;
-}
-
-/*---------void printpredescessors(Class_Of_State *)------------*/
-void LDDGraph::printpredecessors(LDDState *s) {
- cout << "Not implemented yet!" << endl;
-}
-
/*** Giving a position in m_GONodes Returns an LDDState ****/
LDDState *LDDGraph::getLDDStateById(unsigned int id) {
return m_GONodes.at(id);
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index aebec6ee675879417e6b58993b841895135b593b..0541ce16b2f7ce0d992cdbf25115af6b76c48daa 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -3,6 +3,7 @@
#include "LDDState.h"
#include "CommonSOG.h"
#include <mutex>
+#include <shared_mutex>
#include <atomic>
//#include "LDDStateExtend.h"
using namespace std;
@@ -15,8 +16,7 @@ class CommonSOG;
class LDDGraph
{
private:
- mutable std::mutex m_mutex;
- mutable std::mutex m_mutex_sha;
+ mutable std::shared_mutex m_mutex;
map<string,uint16_t>* m_transition;
map<uint16_t,string>* m_places;
void printGraph(LDDState *, size_t &);
@@ -29,33 +29,26 @@ class LDDGraph
void setTransition(map<string,uint16_t>& list_transitions);
MetaLDDNodes m_GONodes;
LDDState *getLDDStateById(unsigned int id);
- void Reset();
LDDState *m_initialstate=nullptr;
- LDDState *m_currentstate;
uint64_t m_nbStates;
uint64_t m_nbMarking;
atomic<uint32_t> m_nbArcs;
LDDState* find(LDDState*);
- LDDState* insertFind(LDDState*);
+ LDDState* insertFindByMDD(MDD,bool&);
LDDState* findSHA(unsigned char*);
LDDState* insertFindSha(unsigned char*,LDDState*);
size_t findSHAPos(unsigned char*,bool &res);
- bool cmpSHA(const unsigned char *s1, const unsigned char *s2);
void insertSHA(LDDState *c);
- LDDEdges& get_successor(LDDState*);
- void printsuccessors(LDDState *);
- int NbBddNode(LDDState*,size_t&);
void InitVisit(LDDState * S,size_t nb);
- void printpredecessors(LDDState *);
+
inline void addArc() {m_nbArcs++;}
void insert(LDDState*);
- LDDGraph(CommonSOG *constuctor) {m_nbArcs=m_nbMarking=0;m_constructor=constuctor;}
+ explicit LDDGraph(CommonSOG *constuctor) {m_nbArcs=m_nbMarking=0;m_constructor=constuctor;}
void setInitialState(LDDState*); //Define the initial state of this graph
- //LDDState* getInitialState() const;
LDDState *getInitialState() const {
return m_GONodes.at(0);
}
- LDDState *getInitialAggregate() {
+ LDDState *getInitialAggregate() const {
return m_initialstate;
}
void printCompleteInformation();
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index d48f621681a714da6731cb8efd0209076842678f..b92653a9f4a45ea3f00fc5abce013970832fa99a 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -1,13 +1,10 @@
#include "LDDState.h"
#include "LDDGraph.h"
-#include <iostream>
#include "SylvanWrapper.h"
-LDDState::~LDDState()
-{
- //dtor
-}
+LDDState::~LDDState()=default;
+
void LDDState::setLDDValue(MDD m) {
m_lddstate=m;
}
@@ -60,4 +57,10 @@ vector<uint16_t> LDDState::getUnmarkedPlaces(set<uint16_t>& lplacesAP) {
return result;
}
+uint8_t LDDState::getMCurrentLevel() const {
+ return m_currentLevel;
+}
+void LDDState::setMCurrentLevel(uint8_t mCurrentLevel) {
+ m_currentLevel = max(m_currentLevel,mCurrentLevel);
+}
diff --git a/src/LDDState.h b/src/LDDState.h
index e261f9e4ab62207cfc29e84d4874cd5b57cdf0c6..d9c448099af63c05e938ebd0538800c51dd82854 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -4,6 +4,7 @@
#include <set>
#include <vector>
#include <string>
+#include <atomic>
#include "SylvanWrapper.h"
using namespace std;
@@ -14,14 +15,13 @@ class LDDState {
LDDState() {
m_boucle = m_blocage = m_visited = false;m_completed=false;
+ m_currentLevel=0;m_nbSuccessorsToBeProcessed=0;
m_virtual = false;
}
virtual ~LDDState();
- Set firable;
- void* Class_Appartenance;
vector<pair<LDDState*, int>>* getSuccessors();
vector<pair<LDDState*, int> > Predecessors, Successors;
- pair<LDDState*, int> LastEdge;
+
void setLDDValue(MDD m);
MDD getLDDValue();
MDD m_lddstate=0;
@@ -29,8 +29,6 @@ class LDDState {
unsigned char* getSHAValue();
bool m_boucle=false;
bool m_blocage=false;
-
-
bool isVirtual() {return m_virtual;}
void setVirtual(){m_virtual=true;}
void setDiv(bool di) {m_boucle=di;}
@@ -38,19 +36,28 @@ class LDDState {
void setDeadLock(bool de) {m_blocage=de;}
bool isDeadLock() {return m_blocage;}
inline void setVisited() {m_visited=true;}
- inline bool isVisited() {return m_visited;}
+ [[nodiscard]] inline bool isVisited() const {return m_visited;}
void setCompletedSucc() {m_completed=true;}
bool isCompletedSucc() {return m_completed;}
vector<uint16_t> getMarkedPlaces(set<uint16_t>& lplacesAP);
vector<uint16_t> getUnmarkedPlaces(set<uint16_t>& lplacesAP);
void setProcess(uint16_t v) {m_process=v;}
- uint16_t getProcess() {return m_process;}
+ [[nodiscard]] uint16_t getProcess() const {return m_process;}
+ inline void decNbSuccessors() {m_nbSuccessorsToBeProcessed--;}
protected:
private:
bool m_virtual = false;
bool m_visited=false;
volatile bool m_completed=false;
uint16_t m_process=0;
+ uint8_t m_currentLevel;
+
+public:
+ atomic<uint32_t> m_nbSuccessorsToBeProcessed;
+
+public:
+ [[nodiscard]] uint8_t getMCurrentLevel() const;
+ void setMCurrentLevel(uint8_t mCurrentLevel);
};
typedef pair<LDDState*, int> LDDEdge;
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index e02c0a8769bdd12a26f88ee7a325781d22a685e5..c1bc2634394a1c43d18235308f7b3bce3fe420e8 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -5,7 +5,7 @@
#include <cstdio>
#include <openssl/md5.h>
-
+#include "md5_hash.h"
#define LENGTH_ID 16
//#define LENGTH_MSG 180
@@ -21,318 +21,282 @@
#define TAG_ACK_SUCC 11
//#define DEBUG_GC 1
-
+#define REDUCE 1
using namespace std;
-MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
-{
- m_comm_world=comm_world;
- SylvanWrapper::sylvan_set_limits ( 16LL<<30, 8, 0 );
+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();
- m_net=&R;
+ m_net = &R;
- m_init=init;
- m_nbPlaces=R.places.size();
+ 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;
+ 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;
+ 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() );
+ m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, R.places.size());
//SylvanWrapper::lddmc_refs_push( m_initialMarking );
- delete []liste_marques;
+ delete[]liste_marques;
// place names
- uint32_t *prec = new uint32_t[m_nbPlaces];
- uint32_t *postc= new uint32_t [m_nbPlaces];
+ 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++ ) {
+ 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;
+ 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 );
+ 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 ( 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 (auto it : t->post) {
+ adjacentPlace.insert(it.first);
+ postc[it.first] = postc[it.first] + it.second;
}
- MDD _minus=SylvanWrapper::lddmc_cube ( prec,m_nbPlaces );
+ 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 ) );
+ 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;
+ delete[] prec;
+ delete[] postc;
}
+void *MCHybridSOG::doCompute() {
-
-//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////////////////////////////// Version distribu�e en utilisant les LDD - MPI/////////////////////////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-
-
-void *MCHybridSOG::doCompute()
-{
- int min_charge=1;
int id_thread;
- id_thread=m_id_thread++;
+ id_thread = m_id_thread++;
unsigned char Identif[20];
- m_Terminated=false;
+ 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;
+ 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::lddmc_refs_push ( Complete_meta_state );
// MDD reduced_initialstate=Canonize(Complete_meta_state,0);
- SylvanWrapper::convert_wholemdd_stringcpp ( Complete_meta_state,*chaine );
- get_md5 ( *chaine,Identif );
- //lddmc_getsha(Complete_meta_state, Identif);
- uint16_t destination= ( uint16_t ) ( Identif[0]%n_tasks );
- c->setProcess ( destination );
- if ( destination==0 ) {
+ SylvanWrapper::convert_wholemdd_stringcpp(Complete_meta_state, *chaine);
+ md5_hash::compute(*chaine, Identif);
+
+ //lddmc_getsha(Complete_meta_state, 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_st[1].push ( Pair ( couple ( c,Complete_meta_state ),fire ) );
- m_graph->setInitialState ( c );
- m_graph->insert ( c );
- m_charge[1]++;
- memcpy ( c->m_SHA2,Identif,16 );
+ 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;
- //cout<<"Initial marking is sent"<<endl;
- m_graph->insertSHA ( c );
- memcpy ( c->m_SHA2,Identif,16 );
- initialstate=Canonize ( Complete_meta_state,0 );
-
- //#endif // REDUCE
- SylvanWrapper::convert_wholemdd_stringcpp ( initialstate,*chaine );
-
+ 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));
- pthread_mutex_lock ( &m_spin_msg[0] );
- m_msg[0].push ( MSG ( chaine,destination ) );
- pthread_mutex_unlock ( &m_spin_msg[0] );
- //delete c;
}
}
- while ( m_Terminated==false ) {
- /******************************* envoie et reception des aggregats ************************************/
-
- if ( id_thread==0 ) {
+ /******************************* envoie et reception des aggregats ************************************/
+ string chaine;
+ if (id_thread == 0) {
do {
send_state_message();
read_message();
- if ( m_waitingBuild ) {
+ if (m_waitingBuildSucc==state::waitingBuild) {
bool res;
- size_t pos=m_graph->findSHAPos ( m_id_md5,res );
- if ( res ) {
- m_waitingBuild=false;
- m_aggWaiting=m_graph->getLDDStateById ( pos );
- m_waitingSucc=true;
- // cout<<"Get build..."<<endl;
+ size_t pos = m_graph->findSHAPos(m_id_md5, res);
+ if (res) {
+ m_waitingBuildSucc=state::waitingSucc;
+ m_aggWaiting = m_graph->getLDDStateById(pos);
}
-
}
- if ( m_waitingSucc ) {
-
- if ( m_aggWaiting->isCompletedSucc() ) {
- //cout<<"Get succ..."<<endl;
- m_waitingSucc=false;
+ if (m_waitingBuildSucc==state::waitingSucc) {
+ if (m_aggWaiting->isCompletedSucc()) {
+ m_waitingBuildSucc = state::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 );
+ 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 );
+
+ } while (!m_Terminated);
+
}
- /******************************* Construction des aggregats ************************************/
+ /******************************* Construction des aggregats ************************************/
else {
- if ( !m_st[id_thread].empty() || !m_msg[id_thread].empty() ) {
- if ( id_thread>1 ) {
- if ( ++m_gc==1 ) {
- m_gc_mutex.lock();
- }
+ while (m_Terminated == false) {
+ 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_st[id_thread].empty() ) {
- Pair e;
- pthread_mutex_lock ( &m_spin_stack[id_thread] );
- e=m_st[id_thread].top();
- m_st[id_thread].pop();
- pthread_mutex_unlock ( &m_spin_stack[id_thread] );
- m_charge[id_thread]--;
- LDDState *reached_class=NULL;
- while ( !e.second.empty() ) {
- int t = * ( e.second.begin() );
- e.second.erase ( t );
- reached_class=new LDDState();
-
-
- MDD ldd_reachedclass=Accessible_epsilon ( get_successor ( e.first.second,t ) );
- // SylvanWrapper::lddmc_refs_push ( ldd_reachedclass );
+ }*/
+ 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();
+ //displayMDDTableInfo();
+ //if ( SylvanWrapper::isGCRequired() ) {
+ // m_gc_mutex.lock();
//#ifdef DEBUG_GC
- // SylvanWrapper::displayMDDTableInfo();
+ // SylvanWrapper::displayMDDTableInfo();
//#endif // DEBUG_GC
- //SylvanWrapper::sylvan_gc_seq();
+ //SylvanWrapper::sylvan_gc_seq();
//#ifdef DEBUG_GC
- // SylvanWrapper::displayMDDTableInfo();
+ // SylvanWrapper::displayMDDTableInfo();
//#endif // DEBUG_GC
- //m_gc_mutex.unlock();
- // }
+ //m_gc_mutex.unlock();
+ // }
//pthread_spin_unlock(&m_spin_md5);
- reached_class->m_lddstate=ldd_reachedclass;
+
//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 );
- get_md5 ( *message_to_send1,Identif );
-
-
- //lddmc_getsha(ldd_reachedclass, Identif);
-
- uint16_t destination= ( uint16_t ) ( Identif[0]%n_tasks );
-
+ 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 ******/
// cout<<"debut boucle pile process "<<task_id<< " thread "<< id_thread<<endl;
- reached_class->setProcess ( destination );
- if ( destination==task_id ) {
- // cout << " construction local de l'aggregat " <<endl;
-
- LDDState* pos=m_graph->insertFind(reached_class );
- if ( !pos ) {
- //cout<<"enter A"<<endl;
- reached_class->setDiv ( Set_Div ( ldd_reachedclass ) );
- reached_class->setDeadLock ( Set_Bloc ( ldd_reachedclass ) );
- memcpy ( reached_class->m_SHA2,Identif,16 );
- 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_graph->addArc();
- Set fire=firable_obs ( ldd_reachedclass );
- min_charge=minCharge();
- pthread_mutex_lock ( &m_spin_stack[min_charge] );
- m_st[min_charge].push ( Pair ( couple ( reached_class,ldd_reachedclass ),fire ) );
- pthread_mutex_unlock ( &m_spin_stack[min_charge] );
- //pthread_mutex_lock(&m_spin_charge);
- m_charge[min_charge]++;
- } else {
- //cout<<"enter B"<<endl;
- m_graph->addArc();
- m_graph_mutex.lock();
- e.first.first->Successors.insert ( e.first.first->Successors.begin(),LDDEdge ( pos,t ) );
- pos->Predecessors.insert ( pos->Predecessors.begin(),LDDEdge ( e.first.first,t ) );
- m_graph_mutex.unlock();
- delete reached_class;
- //cout<<"quit B"<<endl;
+ 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);
+ 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 ******/
+ /**************** construction externe ******/
else { // send to another process
-
- LDDState* posV=m_graph->insertFindSha( Identif,reached_class );
- if ( !posV ) {
+ 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);
#ifndef REDUCE
- reached=Canonize ( ldd_reachedclass,0 );
- // SylvanWrapper::lddmc_refs_push( reached );
+ reached = Canonize(ldd_reachedclass, 0);
+ // SylvanWrapper::lddmc_refs_push( reached );
#endif
- //MDD Reduced=ldd_reachedclass;
- string* message_to_send2=new string();
- SylvanWrapper::convert_wholemdd_stringcpp ( reached,*message_to_send2 );
+ 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 ) );
+ 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();
- pthread_mutex_lock ( &m_spin_msg[0] );
- m_msg[0].push ( MSG ( message_to_send2,destination ) );
- pthread_mutex_unlock ( &m_spin_msg[0] );
+ m_tosend_msg.push(MSG(message_to_send2, destination));
//cout<<"quit C"<<endl;
} else {
//cout<<"sha found "<<endl;
m_graph->addArc();
- m_graph_mutex.lock();
- e.first.first->Successors.insert ( e.first.first->Successors.begin(),LDDEdge ( posV,t ) );
- posV->Predecessors.insert ( posV->Predecessors.begin(),LDDEdge ( e.first.first,t ) );
- m_graph_mutex.unlock();
+ {
+ 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;
}
}
@@ -340,418 +304,256 @@ void *MCHybridSOG::doCompute()
e.first.first->setCompletedSucc();
}
-
/******************************* Construction des aggregats � partir de pile de messages ************************************/
-
- if ( !m_msg[id_thread].empty() ) {
- MSG popped_msg;
- pthread_mutex_lock ( &m_spin_msg[id_thread] );
- popped_msg=m_msg[id_thread].top();
- m_msg[id_thread].pop();
- pthread_mutex_unlock ( &m_spin_msg[id_thread] );
-
- m_charge[id_thread]--;
- MDD receivedLDD=decodage_message ( popped_msg.first->c_str() );
+ MSG popped_msg;
+ if (m_received_msg.try_pop(popped_msg)) {
+ MDD receivedLDD = decodage_message(popped_msg.first->c_str());
delete popped_msg.first;
- LDDState* Agregate=new LDDState();
- MDD MState=Accessible_epsilon ( receivedLDD );
- Agregate->m_lddstate=MState;
- if ( !m_graph->insertFind( Agregate ) ) {
- //cout<<"enter D"<<endl;
- //#ldd_refs_push ( MState );
- Agregate->setDiv ( Set_Div ( MState ) );
- Agregate->setDeadLock ( Set_Bloc ( MState ) );
- Agregate->setProcess ( task_id );
- //m_graph_mutex.lock();
- string* chaine=new string();
- SylvanWrapper::convert_wholemdd_stringcpp ( MState,*chaine );
- get_md5 ( *chaine,Identif );
- delete chaine;
- memcpy ( Agregate->m_SHA2,Identif,16 );
- //m_graph_mutex.unlock();
- Set fire=firable_obs ( MState );
- min_charge=minCharge();
- pthread_mutex_lock ( &m_spin_stack[min_charge] );
- m_st[min_charge].push ( Pair ( couple ( Agregate,MState ),fire ) );
- pthread_mutex_unlock ( &m_spin_stack[min_charge] );
- m_charge[min_charge]++;
- //cout<<"quit D"<<endl;
- }
- else {
- delete Agregate;
+ 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();
- }
+ /* if ( id_thread>1 ) {
+ if ( --m_gc==0 ) {
+ m_gc_mutex.unlock();
+ }
- }
+ }*/
- } // End while (m_msg[id_thread].size()>0 || m_st[id_thread].size()>0);
- // }
+ // }
+ }
} /// End else
- // cout<<"Working process "<<task_id<<" leaved...thread "<<id_thread<<endl;
+ // cout<<"Working process "<<task_id<<" leaved...thread "<<id_thread<<endl;
}
- // cout<<"Finnnnnn...."<<endl;
+ // cout<<"Finnnnnn...."<<endl;
}
+void MCHybridSOG::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) {
-void MCHybridSOG::read_message()
-{
- int flag=0;
- MPI_Iprobe ( MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status ); // exist a msg to receiv?
- while ( flag!=0 ) {
- //cout<<"message tag :"<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
- if ( m_status.MPI_TAG==TAG_ASK_STATE ) {
+ if (m_status.MPI_TAG == TAG_ASK_STATE) {
//cout<<"TAG ASKSTATE received by task "<<task_id<<" from "<<m_status.MPI_SOURCE<<endl;
char mess[17];
- MPI_Recv ( mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status );
+ 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 ) {
- //cout<<"Not found"<<endl;
- m_waitingAgregate=true;
- memcpy ( m_id_md5,mess,16 );
+ 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 );
+ 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 ) {
-
+ } 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_waitingBuild=false;
- m_waitingSucc=false;
+ MPI_Recv(mess, 16, MPI_BYTE, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
+ m_waitingBuildSucc=state::waitInitial;
bool res;
- //cout<<"Before "<<res<<endl;
- size_t pos=m_graph->findSHAPos ( mess,res );
- //cout<<"After "<<res<<endl;
- if ( res ) {
- LDDState *aggregate=m_graph->getLDDStateById ( pos );
- m_aggWaiting=aggregate;
- if ( aggregate->isCompletedSucc() ) {
+
+ size_t pos = m_graph->findSHAPos(mess, res);
+
+ if (res) {
+ m_aggWaiting = m_graph->getLDDStateById(pos);
+ if (m_aggWaiting->isCompletedSucc()) {
sendSuccToMC();
} else {
- m_waitingSucc=true;
- //cout<<"Waiting for succ..."<<endl;
+ m_waitingBuildSucc=state::waitingSucc;
}
} else {
- m_waitingBuild=true;
- //cout<<"Waiting for build..."<<endl;
- memcpy ( m_id_md5,mess,16 );
+ m_waitingBuildSucc=state::waitingBuild;
+ memcpy(m_id_md5, mess, 16);
}
-
}
- int v;
- switch ( m_status.MPI_TAG ) {
- case TAG_STATE:
- //cout<<"=============================TAG STATE received by task "<<task_id<<endl;
- read_state_message();
- break;
- case TAG_FINISH:
- //cout<<"TAG FINISH received by task "<<task_id<<endl;
- MPI_Recv ( &v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status );
- m_Terminated=true;
- break;
- case TAG_INITIAL:
- // cout<<"TAG INITIAL received by task "<<task_id<<endl;
- 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 );
- break;
- /*default: cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
- //AbortTerm();
- //break; */
+ 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 );
+ }
+ MPI_Iprobe(MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &flag, &m_status);
}
}
-void MCHybridSOG::read_state_message()
-{
- int min_charge;
- /****************************************** debut reception 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 );
- min_charge=minCharge();
- m_charge[min_charge]++;
- pthread_mutex_lock ( &m_spin_msg[min_charge] );
- m_msg[min_charge].push ( MSG ( msg_receiv,0 ) );
- pthread_mutex_unlock ( &m_spin_msg[min_charge] );
-}
-
-void MCHybridSOG::send_state_message()
-{
- while ( !m_msg[0].empty() ) {
- pthread_mutex_lock ( &m_spin_msg[0] );
- MSG s=m_msg[0].top();
- m_msg[0].pop();
- pthread_mutex_unlock ( &m_spin_msg[0] );
- unsigned int message_size;
- message_size=s.first->size()+1;
- int destination=s.second;
+/**
+ * send a message containing an aggregate
+ */
+void MCHybridSOG::send_state_message() {
+ MSG s;
+ while (m_tosend_msg.try_pop(s) && !m_Terminated) {
+ int message_size;
+ message_size = 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 );
+ MPI_Send(s.first->c_str(), message_size, MPI_CHAR, destination, TAG_STATE, MPI_COMM_WORLD);//, &request);
+ /*int flag;
+ do {
+ read_message();
+ MPI_Test(&request, &flag, &m_status);
+ } while (!flag);*/
m_nbsend++;
- m_size_mess+=message_size;
+ m_size_mess += message_size;
delete s.first;
}
}
-void MCHybridSOG::computeDSOG ( LDDGraph &g )
-
-{
- m_graph=&g;
- double tps;
-
- // double t1=(double)clock() / (double)CLOCKS_PER_SEC;
- //cout<<"process with id "<<task_id<<" / "<<n_tasks<<endl;
- MPI_Barrier ( m_comm_world );
- // cout<<"After!!!!process with id "<<task_id<<endl;
- // int nb_th;
- m_nb_thread=nb_th;
- //cout<<"nb de thread"<<nb_th<<endl;
- int rc;
- m_id_thread=0;
- m_nbrecv=0;
- m_nbsend=0;
- for ( int i=1; i<m_nb_thread; i++ ) {
- m_charge[i]=0;
- }
-
- m_gc=0;
- pthread_spin_init ( &m_spin_md5,0 );
- for ( uint8_t i=0; i<m_nb_thread; i++ ) {
- pthread_mutex_init ( &m_spin_stack[i], 0 );
- pthread_mutex_init ( &m_spin_msg[i], 0 );
- }
-
- timespec start, finish;
- if ( task_id==0 ) {
- clock_gettime ( CLOCK_REALTIME, &start );
- }
-
- for ( uint8_t i=0; i<m_nb_thread-1; i++ ) {
- if ( ( rc = pthread_create ( &m_list_thread[i], NULL,threadHandler,this ) ) ) {
- cout<<"error: pthread_create, rc: "<<rc<<endl;
+/*
+ * Creation of threads
+ */
+void MCHybridSOG::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++ ) {
- pthread_join ( m_list_thread[i], NULL );
+ for (int i = 0; i < m_nb_thread - 1; i++) {
+ m_list_thread[i]->join();
+ delete m_list_thread[i];
}
-
-
-
- int sum_nbStates=0;
- int sum_nbArcs=0;
- int nbstate=g.m_nbStates;
-
- int nbarcs=g.m_nbArcs;
- unsigned long total_size_mess=0;
- MPI_Reduce ( &nbstate, &sum_nbStates, 1, MPI_INT, MPI_SUM, 0, m_comm_world );
- MPI_Reduce ( &nbarcs, &sum_nbArcs, 1, MPI_INT, MPI_SUM, 0, m_comm_world );
- MPI_Reduce ( &m_size_mess, &total_size_mess, 1, MPI_INT, MPI_SUM, 0, m_comm_world );
-
- if ( task_id==0 ) {
- clock_gettime ( CLOCK_REALTIME, &finish );
-
- tps = ( finish.tv_sec - start.tv_sec );
- tps += ( finish.tv_nsec - start.tv_nsec ) / 1000000000.0;
- std::cout << " TIME OF CONSTRUCTION OF THE SOG "
- << tps
- << " seconds\n";
-
- cout<<"NB AGGREGATES****** "<<sum_nbStates<<endl;
- cout<<"NB ARCS****** "<<sum_nbArcs<<endl;
- cout<<" Size of message ***** "<<total_size_mess<<" bytes"<<endl;
- }
- //MPI_Finalize();
-
-
}
-uint8_t MCHybridSOG::minCharge()
-{
- uint8_t pos=1;
- int min_charge=m_charge[1];
- for ( uint8_t i=1; i<m_nb_thread; i++ ) {
- if ( m_charge[i]<min_charge ) {
- min_charge=m_charge[i];
- pos=i;
- }
- }
- return pos;
-}
-
-
-
-
-
-MCHybridSOG::~MCHybridSOG()
-{
- //dtor
-}
+MCHybridSOG::~MCHybridSOG()=default;
/******************************************convert char ---> MDD ********************************************/
-MDD MCHybridSOG::decodage_message ( const char *chaine )
-{
- MDD M=lddmc_false;
- unsigned int nb_marq= ( ( unsigned char ) chaine[1]-1 );
- nb_marq= ( nb_marq<<7 ) | ( ( unsigned char ) chaine[0]>>1 );
-
- unsigned int index=2;
+MDD MCHybridSOG::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 );
+ 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 );
+ MDD N = SylvanWrapper::lddmc_cube(list_marq, m_nbPlaces);
+ M = SylvanWrapper::lddmc_union_mono(M, N);
}
return M;
}
-void * MCHybridSOG::threadHandler ( void *context )
-{
- return ( ( MCHybridSOG* ) context )->doCompute();
+void *MCHybridSOG::threadHandler(void *context) {
+ return ((MCHybridSOG *) context)->doCompute();
}
-
-
-void MCHybridSOG::get_md5 ( const string& chaine,unsigned char *md_chaine )
-{
- pthread_spin_lock ( &m_spin_md5 );
- MD5 ( chaine.c_str(), chaine.size(),md_chaine );
- pthread_spin_unlock ( &m_spin_md5 );
-}
-
-void MCHybridSOG::sendSuccToMC()
-{
- uint32_t nb_succ=m_aggWaiting->getSuccessors()->size();
- uint32_t message_size=nb_succ*20+4;
+void MCHybridSOG::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;
+ 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();
- //cout<<" pcontainer "<<pcontainer<<endl;
- memcpy ( mess_tosend+i_message,&pcontainer,2 );
- i_message+=2;
- memcpy ( mess_tosend+i_message,& ( elt.second ),2 );
- i_message+=2;
+ 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;
}
-
- MPI_Send ( mess_tosend,message_size,MPI_BYTE,n_tasks, TAG_ACK_SUCC,MPI_COMM_WORLD );
+ read_message();
+ MPI_Send(mess_tosend, message_size, MPI_BYTE, n_tasks, TAG_ACK_SUCC, MPI_COMM_WORLD);
}
-/*
-set<uint16_t> MCHybridSOG::getMarkedPlaces ( LDDState *agg )
-{
- set<uint16_t> result;
- MDD mdd=agg->getLDDValue();
- uint16_t depth=0;
- while ( mdd>lddmc_true ) {
- //printf("mddd : %d \n",mdd);
- mddnode_t node=GETNODE ( mdd );
- if ( m_place_proposition.find ( depth ) !=m_place_proposition.end() )
- if ( mddnode_getvalue ( node ) ==1 ) {
- result.insert ( depth );
- }
-
- mdd=mddnode_getdown ( node );
- depth++;
-
- }
- return result;
-}*/
-
-/*
-set<uint16_t> MCHybridSOG::getUnmarkedPlaces ( LDDState *agg )
-{
- set<uint16_t> result;
- MDD mdd=agg->getLDDValue();
-
- uint16_t depth=0;
- while ( mdd>lddmc_true ) {
- //printf("mddd : %d \n",mdd);
- mddnode_t node=GETNODE ( mdd );
- if ( m_place_proposition.find ( depth ) !=m_place_proposition.end() )
- if ( mddnode_getvalue ( node ) ==0 ) {
- result.insert ( depth );
-
- }
- mdd=mddnode_getdown ( node );
- depth++;
-
- }
- return result;
-}*/
// Send propositions to Model checker
-void MCHybridSOG::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 );
- //cout<<"************* Pos to send :"<<pos<<endl;
- 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;
+void MCHybridSOG::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.begin(); it!=unmarked_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 );
+ uint8_t divblock = agg->isDiv();
+ divblock = divblock | (agg->isDeadLock() << 1);
+ memcpy(mess_to_send + indice, &divblock, 1);
indice++;
- MPI_Send ( mess_to_send,indice,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD );
-}
+ 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/MCHybridSOG.h b/src/MCHybridSOG.h
index 0251407e2fda74efca7076dc3db9a578a169e16f..43517640e9a6c2f1e29b94111b0a8fe09e18265d 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -8,7 +8,7 @@
//#include "MDGraph.h"
//#include "bvec.h"
#include <pthread.h>
-#include <stdio.h>
+#include <cstdio>
#include <sys/types.h>
#include <unistd.h>
#include "LDDGraph.h"
@@ -16,7 +16,7 @@
#include <mpi.h>
#include <sha2.h>
-#include <stdio.h>
+
#include <sys/ipc.h>
#include <sys/shm.h>
#include <sys/types.h>
@@ -26,14 +26,14 @@
#include <iostream>
#include <queue>
#include <string>
-//#include <boost/serialization/string.hpp>
-#include <time.h>
+#include <ctime>
#include <chrono>
#include "CommonSOG.h"
#include <atomic>
#include <thread>
#include <mutex>
#include <condition_variable>
+#include "SafeDequeue.h"
// namespace mpi = boost::mpi;
//#define MASTER 0
@@ -46,7 +46,7 @@ extern int n_tasks, task_id;
typedef pair<string *, unsigned int> MSG;
typedef stack<MSG> pile_msg;
-
+enum class state {waitInitial,waitingBuild,waitingSucc};
// typedef vector<Trans> vec_trans;
class MCHybridSOG : public CommonSOG
{
@@ -55,69 +55,39 @@ public:
void buildFromNet(int index);
/// principal functions to construct the SOG
void computeDSOG(LDDGraph &g);
- virtual ~MCHybridSOG();
+ ~MCHybridSOG() 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_bool m_waitingBuild;
- atomic_bool m_waitingSucc;
+ atomic<bool> m_waitingAgregate;// (false);
+ atomic<state> m_waitingBuildSucc;
char m_id_md5[16];
LDDState * m_aggWaiting=nullptr;
-
-
- /// \ hash function
- void get_md5(const string &chaine, unsigned char *md_chaine);
-
- /// minimum charge function for the load balancing between thread
- inline uint8_t minCharge();
-
-
-
int m_nbmetastate;
+ SafeDequeue<Pair> m_common_stack;
+ SafeDequeue<MSG> m_received_msg;
+ SafeDequeue<MSG> m_tosend_msg;
- pile m_st[128];
- pile_msg m_msg[128];
-
- // void DisplayMessage(const char *chaine);
-
- // int n_tasks, task_id;
-
- int m_charge[128];
- int m_init;
-
-
+ 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 read_state_message();
void send_state_message();
-
- pthread_t m_list_thread[128];
-
- atomic<uint8_t> m_id_thread;
- //pthread_mutex_t m_mutex_stack[128];
- pthread_mutex_t m_spin_stack[128];
- pthread_mutex_t m_spin_msg[128];
-
- pthread_spinlock_t m_spin_md5;
-
-
+ 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;
- /*set<uint16_t> getUnmarkedPlaces(LDDState *agg);
- set<uint16_t> getMarkedPlaces(LDDState *agg);*/
};
diff --git a/src/ModelCheckBaseMT.h b/src/ModelCheckBaseMT.h
index 4139741c8408827e2564f7789fe759ace72d65b2..83bacc64d5003a7cc363b59005bba53206148763 100644
--- a/src/ModelCheckBaseMT.h
+++ b/src/ModelCheckBaseMT.h
@@ -9,6 +9,7 @@ public:
virtual LDDState * getInitialMetaState();
virtual void buildSucc(LDDState *agregate);
void loadNet();
+
virtual ~ModelCheckBaseMT();
protected:
std::condition_variable m_condBuild;
diff --git a/src/ModelCheckThReq.cpp b/src/ModelCheckThReq.cpp
index d65eaf79f8818ea0aea3f2d837a414920fc4a18c..2e87f52296ea142955e50f41f4138a39664da27e 100644
--- a/src/ModelCheckThReq.cpp
+++ b/src/ModelCheckThReq.cpp
@@ -1,6 +1,8 @@
#include "ModelCheckThReq.h"
#include <unistd.h>
+#include <thread>
+#define LEVEL 3
ModelCheckThReq::ModelCheckThReq(const NewNet &R, int nbThread) : ModelCheckBaseMT(R, nbThread) {
}
@@ -26,6 +28,7 @@ void ModelCheckThReq::preConfigure() {
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;
@@ -91,33 +94,32 @@ void ModelCheckThReq::preConfigure() {
delete[] prec;
delete[] postc;
}
+
/**
* Creates builder threads
*/
-void ModelCheckThReq::ComputeTh_Succ()
-{
+void ModelCheckThReq::ComputeTh_Succ() {
int rc;
- m_id_thread=0;
+ m_id_thread = 0;
//cout<<"Enter : "<<__func__ <<endl;
- pthread_mutex_init(&m_mutex, NULL);
- pthread_mutex_init(&m_graph_mutex,NULL);
- pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);
- pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread+1);
- for (int i=0; i<m_nb_thread; i++)
- {
- if ((rc = pthread_create(&m_list_thread[i], NULL,threadHandler,this)))
- {
- cout<<"error: pthread_create, rc: "<<rc<<endl;
+ pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread + 1);
+ for ( int i = 0; i < m_nb_thread; i++ ) {
+ m_list_thread[i]= new thread ( threadHandler,this );
+ if ( m_list_thread[i]==nullptr ) {
+ cout << "error: pthread creation failed" << endl;
}
}
+
}
/*
* Build initial aggregate
*/
-LDDState * ModelCheckThReq::getInitialMetaState() {
- //cout<<"Enter : "<<__func__ <<endl;
- if (m_graph->getInitialAggregate()!= nullptr) return m_graph->getInitialAggregate();
+LDDState *ModelCheckThReq::getInitialMetaState() {
+
+ if (m_graph->getInitialAggregate() != nullptr) {
+ return m_graph->getInitialAggregate();
+ }
ComputeTh_Succ();
LDDState *c = new LDDState;
MDD initial_meta_state = Accessible_epsilon(m_initialMarking);
@@ -125,100 +127,114 @@ LDDState * ModelCheckThReq::getInitialMetaState() {
c->m_lddstate = initial_meta_state;
m_graph->setInitialState(c);
m_graph->insert(c);
- Set fire = firable_obs(initial_meta_state);
- int j = 0;
- for (auto it = fire.begin(); it != fire.end(); it++, j++)
- m_st[j % m_nb_thread].push(couple_th(c, *it));
- pthread_barrier_wait(&m_barrier_threads);
- pthread_barrier_wait(&m_barrier_builder);
c->setVisited();
+ Set fire = firable_obs(initial_meta_state);
+ c->m_nbSuccessorsToBeProcessed = fire.size();
+ c->setMCurrentLevel(LEVEL);
+
+ c->setDiv(Set_Div(initial_meta_state));
+ c->setDeadLock(Set_Bloc(initial_meta_state));
+ if (!fire.empty()) {
+ for (auto it = fire.begin(); it != fire.end(); it++)
+ m_common_stack.push(couple_th(c, *it));
+ std::unique_lock<std::mutex> lk(m_mutexBuildCompleted);
+ m_datacondBuildCompleted.wait(lk, [c] { return c->isCompletedSucc(); });
+ lk.unlock();
+ } else c->setCompletedSucc();
return c;
}
/*
- * Build successors of @aggregate using PThreads
+ * Build successors of @agregate
*/
void ModelCheckThReq::buildSucc(LDDState *agregate) {
- if (!agregate->isVisited())
- {
- //SylvanWrapper::displayMDDTableInfo();
+ if (!agregate->isVisited()) {
agregate->setVisited();
- Set fire=firable_obs(agregate->getLDDValue());
- int j=0;
- for(auto it=fire.begin(); it!=fire.end(); it++,j++)
- m_st[j%m_nb_thread].push(couple_th(agregate,*it));
- pthread_barrier_wait(&m_barrier_threads);
- pthread_barrier_wait(&m_barrier_builder);
+ if (agregate->getMCurrentLevel() == 0) {
+ Set fire = firable_obs(agregate->m_lddstate);
+ agregate->setMCurrentLevel(LEVEL);
+ agregate->m_nbSuccessorsToBeProcessed = fire.size();
+ if (!fire.empty()) {
+ agregate->m_nbSuccessorsToBeProcessed = fire.size();
+ for (auto it = fire.begin(); it != fire.end(); it++)
+ m_common_stack.push(couple_th(agregate, *it));
+ std::unique_lock<std::mutex> lk(m_mutexBuildCompleted);
+ m_datacondBuildCompleted.wait(lk, [agregate] { return agregate->isCompletedSucc(); });
+ lk.unlock();
+
+ } else agregate->setCompletedSucc();
+ } else {
+ std::unique_lock<std::mutex> lk(m_mutexBuildCompleted);
+ m_datacondBuildCompleted.wait(lk, [agregate] { return agregate->isCompletedSucc(); });
+ lk.unlock();
+ }
}
}
-void * ModelCheckThReq::threadHandler(void *context)
-{
- return ((ModelCheckThReq*)context)->Compute_successors();
+void *ModelCheckThReq::threadHandler(void *context) {
+ return ((ModelCheckThReq *) context)->Compute_successors();
}
+void *ModelCheckThReq::Compute_successors() {
-void * ModelCheckThReq::Compute_successors()
-{
- int id_thread;
- id_thread=m_id_thread++;
- LDDState* reached_class=nullptr;
- // cout<<"Before do : "<<__func__ <<endl;
- do
- {
- pthread_barrier_wait(&m_barrier_threads);
- while (!m_st[id_thread].empty())
- {
- couple_th elt=m_st[id_thread].top();
- m_st[id_thread].pop();
- LDDState *aggregate=elt.first;
- MDD meta_state=aggregate->getLDDValue();
- int transition=elt.second;
- MDD complete_state=Accessible_epsilon(get_successor(meta_state,transition));
- reached_class=new LDDState;
- reached_class->m_lddstate=complete_state;
- reached_class->setDiv(Set_Div(complete_state));
- reached_class->setDeadLock(Set_Bloc(complete_state));
- pthread_mutex_lock(&m_graph_mutex);
- LDDState* pos=m_graph->find(reached_class);
- if(!pos)
+ couple_th elt;
+ LDDState *pos, *aggregate;
+ do {
+ while (!m_finish && m_common_stack.try_pop(elt)) {
+ aggregate = elt.first;
+ int transition = elt.second;
+ MDD meta_state = aggregate->m_lddstate;
+ MDD complete_state = Accessible_epsilon(get_successor(meta_state, transition));
+ bool res;
+ pos = m_graph->insertFindByMDD(complete_state, res);
{
- m_graph->insert(reached_class);
- aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(reached_class,transition));
- reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(aggregate,transition));
- pthread_mutex_unlock(&m_graph_mutex);
- m_graph->addArc();
+ std::unique_lock guard(m_graph_mutex);
+ aggregate->Successors.insert(aggregate->Successors.begin(), LDDEdge(pos, transition));
+ pos->Predecessors.insert(pos->Predecessors.begin(),
+ LDDEdge(aggregate, transition));
}
- else
- { aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(pos,transition));
- pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(aggregate,transition));
- pthread_mutex_unlock(&m_graph_mutex);
- m_graph->addArc();
- delete reached_class;
+ if (!res) {
+ pos->setDiv(Set_Div(complete_state));
+ pos->setDeadLock(Set_Bloc(complete_state));
}
+ aggregate->decNbSuccessors();
+ if (aggregate->m_nbSuccessorsToBeProcessed == 0) {
+ aggregate->setCompletedSucc();
+ m_datacondBuildCompleted.notify_one();
+ }
+
+ if (aggregate->getMCurrentLevel() > 0 && pos->getMCurrentLevel() == 0) {
+ pos->setMCurrentLevel(aggregate->getMCurrentLevel() - 1);
+ if (aggregate->getMCurrentLevel() > 1) {
+ Set fire = firable_obs(pos->getLDDValue());
+ pos->m_nbSuccessorsToBeProcessed = fire.size();
+ if (!fire.empty()) {
+ for (auto it = fire.begin(); it != fire.end(); it++)
+ m_common_stack.push(couple_th(pos, *it));
+ } else {
+ pos->setCompletedSucc();
+ m_datacondBuildCompleted.notify_one();
+ }
+
+ }
+
+ }
+ m_graph->addArc();
}
- //cout<<"Before barrier : "<<__func__ <<endl;
- pthread_barrier_wait(&m_barrier_builder);
- //m_finish=m_finish;
- //cout<<"After barrier : "<<__func__ <<endl;
- }
- while (!m_finish);
- //cout<<"Quit : "<<__func__ <<" ; "<<id_thread<<endl;
+ } while (!m_finish);
+
+
}
ModelCheckThReq::~ModelCheckThReq() {
- //cout<<"1 : "<<__func__ <<endl;
- pthread_barrier_wait(&m_barrier_threads);
- m_finish=true;
- pthread_barrier_wait(&m_barrier_builder);
- /*for (int i = 0; i < m_nb_thread; i++)
- {
- pthread_join(m_list_thread[i], NULL);
- }*/
- //cout<<"3 : "<<__func__ <<endl;
+ //pthread_barrier_wait(&m_barrier_threads);
+ for (int i = 0; i < m_nb_thread; i++) {
+ m_list_thread[i]->join();
+ delete m_list_thread[i];
+ }
}
diff --git a/src/ModelCheckThReq.h b/src/ModelCheckThReq.h
index db4ef2aec484d1649c507ff88331e8750addea37..51dfb7be8efe673af6f332a222bc5728a0b9829d 100644
--- a/src/ModelCheckThReq.h
+++ b/src/ModelCheckThReq.h
@@ -3,29 +3,28 @@
#include "ModelCheckBaseMT.h"
#include <atomic>
#include <mutex>
+#include <thread>
+#include "SafeDequeue.h"
typedef pair<LDDState *, int> couple_th;
-typedef stack<pair<LDDState *,int>> pile_t;
+//typedef stack<pair<LDDState *,int>> pile_t;
class ModelCheckThReq : public ModelCheckBaseMT {
public:
ModelCheckThReq(const NewNet &R,int nbThread);
- ~ModelCheckThReq();
-
+ ~ModelCheckThReq() override;
void buildSucc(LDDState *agregate) override;
static void *threadHandler(void *context);
void *Compute_successors();
void ComputeTh_Succ();
- LDDState * getInitialMetaState();
+ LDDState * getInitialMetaState() override;
private:
- void preConfigure();
- pile_t m_st[128];
+ void preConfigure() override;
+ SafeDequeue<couple_th> m_common_stack;
atomic<uint8_t> m_id_thread;
- pthread_mutex_t m_mutex;
- pthread_mutex_t m_graph_mutex;
- pthread_barrier_t m_barrier_threads,m_barrier_builder;
- pthread_t m_list_thread[128];
- volatile atomic<bool> m_finish=false;
-
+ thread* m_list_thread[128];
+ mutable std::mutex m_mutexBuildCompleted;
+ std::condition_variable m_datacondBuildCompleted;
+ pthread_barrier_t m_barrier_threads;
};
#endif
diff --git a/src/ModelCheckerCPPThread.cpp b/src/ModelCheckerCPPThread.cpp
index 6ad7a5afba07a6105f39b4d052e369c055d44e85..3f43d7131aee0ed79204e7b909925cb22e6fdc66 100644
--- a/src/ModelCheckerCPPThread.cpp
+++ b/src/ModelCheckerCPPThread.cpp
@@ -6,23 +6,23 @@
#include <unistd.h>
#include "SylvanWrapper.h"
+
#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
using namespace std;
-ModelCheckerCPPThread::ModelCheckerCPPThread ( const NewNet &R, int nbThread ) :
- ModelCheckBaseMT ( R, nbThread )
-{
+ModelCheckerCPPThread::ModelCheckerCPPThread(const NewNet &R, int nbThread) :
+ ModelCheckBaseMT(R, nbThread) {
}
+
size_t
-getMaxMemoryV3()
-{
- long pages = sysconf ( _SC_PHYS_PAGES );
- long page_size = sysconf ( _SC_PAGE_SIZE );
+getMaxMemoryV3() {
+ long pages = sysconf(_SC_PHYS_PAGES);
+ long page_size = sysconf(_SC_PAGE_SIZE);
return pages * page_size;
}
-void ModelCheckerCPPThread::preConfigure()
-{
+
+void ModelCheckerCPPThread::preConfigure() {
/*lace_init ( 1, 0 );
lace_startup ( 0, NULL, NULL );
@@ -30,7 +30,7 @@ void ModelCheckerCPPThread::preConfigure()
if ( max > getMaxMemoryV3() ) {
max = getMaxMemoryV3() /10*9;
}*/
- SylvanWrapper::sylvan_set_limits ( 16LL<<30, 10, 0 );
+ SylvanWrapper::sylvan_set_limits(16LL << 30, 10, 0);
//sylvan_init_package();
SylvanWrapper::sylvan_init_package();
@@ -54,46 +54,46 @@ void ModelCheckerCPPThread::preConfigure()
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++ ) {
+ 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 );
+ 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++ ) {
+ for (vector<Transition>::const_iterator t = m_net->transitions.begin(); t != m_net->transitions.end(); t++) {
// Initialisation
- for ( i = 0; i < m_nbPlaces; i++ ) {
+ 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 );
+ 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 );
+ 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++ ) {
+ for (set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++) {
MDD Precond = lddmc_true;
- Precond = Precond & ( ( *it ) >= prec[*it] );
+ 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 ) );
+ 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;
@@ -103,113 +103,93 @@ void ModelCheckerCPPThread::preConfigure()
}
+void ModelCheckerCPPThread::Compute_successors() {
+ int id_thread;
+ id_thread = m_id_thread++;
-void ModelCheckerCPPThread::Compute_successors()
-{
- int id_thread;
-
- id_thread = m_id_thread++;
-
//cout<<" I'm here thread id " <<m_id_thread<<endl;
- Set fire;
-
- if ( id_thread == 0 ) {
- LDDState *c = new LDDState;
- MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
- SylvanWrapper::lddmc_refs_push ( Complete_meta_state );
-
- fire = firable_obs ( Complete_meta_state );
+ Set fire;
+
+ if (id_thread == 0) {
+ auto *c = new LDDState;
+ MDD Complete_meta_state = Accessible_epsilon(m_initialMarking);
+ SylvanWrapper::lddmc_refs_push(Complete_meta_state);
+
+ fire = firable_obs(Complete_meta_state);
c->m_lddstate = Complete_meta_state;
- c->setDeadLock ( Set_Bloc ( Complete_meta_state ) );
- c->setDiv ( Set_Div ( Complete_meta_state ) );
- m_graph->setInitialState ( c );
- m_graph->insert ( c );
- m_common_stack.push ( Pair ( couple ( c, Complete_meta_state ), fire ) );
+ c->setDeadLock(Set_Bloc(Complete_meta_state));
+ c->setDiv(Set_Div(Complete_meta_state));
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
+ m_common_stack.push(Pair(couple(c, Complete_meta_state), fire));
m_condStack.notify_one();
m_finish_initial = true;
}
- LDDState *reached_class;
+
//pthread_barrier_wait ( &m_barrier_builder );
Pair e;
- do {
- std::unique_lock<std::mutex> lk ( m_mutexStack );
- m_condStack.wait(lk,std::bind(&ModelCheckerCPPThread::hasToProcess,this));
+ do {
+ std::unique_lock<std::mutex> lk(m_mutexStack);
+ m_condStack.wait(lk, std::bind(&ModelCheckerCPPThread::hasToProcess, this));
lk.unlock();
-
- if ( m_common_stack.try_pop ( e ) && !m_finish ) {
- while ( !e.second.empty() && !m_finish ) {
- int t = *e.second.begin();
- e.second.erase ( t );
- MDD reduced_meta = Accessible_epsilon ( get_successor ( e.first.second, t ) );
- SylvanWrapper::lddmc_refs_push ( reduced_meta );
- reached_class = new LDDState();
- reached_class->m_lddstate = reduced_meta;
- LDDState *pos = m_graph->find ( reached_class );
- if ( !pos ) {
- m_graph->addArc();
- m_graph->insert ( reached_class );
- fire = firable_obs ( reduced_meta );
- reached_class->setDeadLock ( Set_Bloc ( reduced_meta ) );
- reached_class->setDiv ( Set_Div ( reduced_meta ) );
- m_common_stack.push ( Pair ( couple ( reached_class, reduced_meta ), fire ) );
- m_condStack.notify_one();
- 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();
- } else {
- delete reached_class;
- m_graph->addArc();
- m_graph_mutex.lock();
- e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( pos, t ) );
- pos->Predecessors.insert ( pos->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
- m_graph_mutex.unlock();
- }
-
- }
- e.first.first->setCompletedSucc();m_condBuild.notify_one();
- } //end advance
-
- } while ( !m_finish );
-
+ if (m_common_stack.try_pop(e) && !m_finish) {
+ while (!e.second.empty() && !m_finish) {
+ int t = *e.second.begin();
+ e.second.erase(t);
+ MDD reduced_meta = Accessible_epsilon(get_successor(e.first.second, t));
+ SylvanWrapper::lddmc_refs_push(reduced_meta);
+ bool res;
+ LDDState *pos = m_graph->insertFindByMDD(reduced_meta, res);
+ m_graph->addArc();
+ if (!res) {
+ fire = firable_obs(reduced_meta);
+ pos->setDeadLock(Set_Bloc(reduced_meta));
+ pos->setDiv(Set_Div(reduced_meta));
+ m_common_stack.push(Pair(couple(pos, reduced_meta), fire));
+ m_condStack.notify_one();
+ }
+ m_graph_mutex.lock();
+ e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(pos, t));
+ pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
+ m_graph_mutex.unlock();
+ }
+ e.first.first->setCompletedSucc();
+ m_condBuild.notify_one();
+ } //end advance
+
+ } while (!m_finish);
}
-void ModelCheckerCPPThread::threadHandler ( void *context )
-{
+void ModelCheckerCPPThread::threadHandler(void *context) {
SylvanWrapper::lddmc_refs_init();
- ( ( ModelCheckerCPPThread* ) context )->Compute_successors();
+ ((ModelCheckerCPPThread *) context)->Compute_successors();
}
-void ModelCheckerCPPThread::ComputeTh_Succ()
-{
+void ModelCheckerCPPThread::ComputeTh_Succ() {
m_id_thread = 0;
-
- pthread_barrier_init ( &m_barrier_builder, NULL, m_nb_thread + 1 );
-
- m_finish=false;
- for ( int i = 0; i < m_nb_thread; i++ ) {
- int rc;
- m_list_thread[i]= new thread ( threadHandler,this );
- if ( m_list_thread==nullptr ) {
- cout << "error: pthread_create, rc: " << rc << endl;
+ pthread_barrier_init(&m_barrier_builder, nullptr, m_nb_thread + 1);
+ m_finish = false;
+ for (int i = 0; i < m_nb_thread; i++) {
+ m_list_thread[i] = new thread(threadHandler, this);
+ if (m_list_thread[i] == nullptr) {
+ cout << "error: pthread creation failed. " << endl;
}
}
}
-ModelCheckerCPPThread::~ModelCheckerCPPThread()
-{
+ModelCheckerCPPThread::~ModelCheckerCPPThread() {
m_finish = true;
m_condStack.notify_all();
- //pthread_barrier_wait ( &m_barrier_builder );
- for ( int i = 0; i < m_nb_thread; i++ ) {
+ for (int i = 0; i < m_nb_thread; i++) {
m_list_thread[i]->join();
delete m_list_thread[i];
}
}
+
bool ModelCheckerCPPThread::hasToProcess() const {
return m_finish || !m_common_stack.empty();
}
diff --git a/src/ModelCheckerCPPThread.h b/src/ModelCheckerCPPThread.h
index 204e6c085fba978f3ad41ec5b6f8479c62e8dee2..da9683768beaba9a60e020b82bfc50762f76a636 100644
--- a/src/ModelCheckerCPPThread.h
+++ b/src/ModelCheckerCPPThread.h
@@ -27,8 +27,7 @@ private:
SafeDequeue<Pair> m_common_stack;
atomic<uint8_t> m_id_thread;
std::mutex m_mutex;
- pthread_barrier_t m_barrier_builder;
- volatile bool m_finish=false;
+ pthread_barrier_t m_barrier_builder;
std::condition_variable m_condStack;
std::mutex m_mutexStack;
thread* m_list_thread[128];
diff --git a/src/NewNet.cpp b/src/NewNet.cpp
index b73c7574631b6e82200d4e184fa799ea981266a7..3ab3187e71b48f86cf2af6b566e998147bbe3bf6 100644
--- a/src/NewNet.cpp
+++ b/src/NewNet.cpp
@@ -1,17 +1,8 @@
#include "NewNet.h"
#include <spot/misc/version.hh>
-#include <spot/twaalgos/dot.hh>
-#include <spot/tl/parse.hh>
-#include <spot/tl/print.hh>
-#include <spot/twaalgos/translate.hh>
-#include <spot/twaalgos/emptiness.hh>
-
-
#include <algorithm>
-#include <ext/hash_map>
#include <iomanip>
#include <iostream>
-#include <fstream>
#include <map>
#include <string>
#include <vector>
@@ -135,7 +126,7 @@ NewNet::NewNet(const char *f, const set<string> & f_trans)
m_placeName.clear();
transitionName.clear();
}
- if (f_trans.size() > 0)
+ if (!f_trans.empty())
{
cout<<"Transition set of formula is not empty\n";
for (set<string>::iterator p=f_trans.begin(); p!=f_trans.end(); p++)
@@ -240,7 +231,7 @@ bool NewNet::Set_Formula_Trans(const char *f)
for (i = 0; i < nb_formula_trans; i++)
{
cout << " z: " << z << endl;
- if (z == NULL)
+ if (z == nullptr)
{
cout << "error in formula trans format " << endl;
return false;
@@ -256,8 +247,8 @@ bool NewNet::Set_Formula_Trans(const char *f)
else
Formula_Trans.insert(pos);
/*cout<<"insertion de :"<<transitions[pos].name<<endl;*/
- z = strtok(NULL, " \t\n");
- if (z == NULL)
+ z = strtok(nullptr, " \t\n");
+ if (z == nullptr)
{
nb = fread(Buff, 1, TAILLEBUFF - 1, in);
Buff[nb] = '\0';
@@ -275,7 +266,7 @@ bool NewNet::Set_Interface_Trans(const char *f)
int pos_trans(TRANSITIONS, string);
char Buff[TAILLEBUFF], *z;
in = fopen(f, "r");
- if (in == NULL)
+ if (in == nullptr)
{
cout << "file " << f << " doesn't exist" << endl;
exit(1);
@@ -289,7 +280,7 @@ bool NewNet::Set_Interface_Trans(const char *f)
for (i = 0; i < int_trans; i++)
{
cout << " z: " << z << endl;
- if (z == NULL)
+ if (z == nullptr)
{
cout << "error in interface format " << endl;
return false;
@@ -304,8 +295,8 @@ bool NewNet::Set_Interface_Trans(const char *f)
}
else
InterfaceTrans.insert(pos);
- z = strtok(NULL, " \t\n");
- if (z == NULL)
+ z = strtok(nullptr, " \t\n");
+ if (z == nullptr)
{
nb = fread(Buff, 1, TAILLEBUFF - 1, in);
Buff[nb] = '\0';
@@ -344,7 +335,7 @@ ostream &operator<<(ostream &os, const Set &s)
{
bool b = false;
- if (s.size())
+ if (!s.empty())
{
for (Set::const_iterator i = s.begin(); !(i == s.end()); i++)
{
diff --git a/src/SafeDequeue.cpp b/src/SafeDequeue.cpp
index 429c78fe2027bc326b8269105566be80c769eeea..fdcb4655d56b2083db1317a36fdbb79c977d9f18 100644
--- a/src/SafeDequeue.cpp
+++ b/src/SafeDequeue.cpp
@@ -16,6 +16,7 @@
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
+#include <iostream>
#include "SafeDequeue.h"
template<typename T>
@@ -46,22 +47,6 @@ void SafeDequeue<T>::push ( T new_value )
}
-/*template<typename T>
-void SafeDequeue<T>::wait_and_pop ( T& value )
-{
-
-}*/
-
-template<typename T>
-std::shared_ptr<T> SafeDequeue<T>::wait_and_pop()
-{
- std::unique_lock<std::mutex> lk ( mut );
- data_cond.wait ( lk,[this] {return !data_queue.empty();} );
- std::shared_ptr<T> res ( std::make_shared<T> ( data_queue.front() ) );
- data_queue.pop();
- return res;
-}
-
template<typename T>
bool SafeDequeue<T>::try_pop ( T& value )
{
@@ -75,17 +60,7 @@ bool SafeDequeue<T>::try_pop ( T& value )
}
-template<typename T>
-std::shared_ptr<T> SafeDequeue<T>::try_pop()
-{
- std::lock_guard<std::mutex> lk ( mut );
- if ( data_queue.empty() ) {
- return std::shared_ptr<T>();
- }
- std::shared_ptr<T> res ( std::make_shared<T> ( data_queue.front() ) );
- data_queue.pop();
- return res;
-}
+
template<typename T>
bool SafeDequeue<T>::empty() const
@@ -98,3 +73,4 @@ bool SafeDequeue<T>::empty() const
template class SafeDequeue<Pair>;
typedef pair<string *, unsigned int> MSG;
template class SafeDequeue<MSG>;
+template class SafeDequeue<couple_th>;
diff --git a/src/SafeDequeue.h b/src/SafeDequeue.h
index 607f0851d35d32f32a28e54ace7aeaf09d892248..d2ffdd42689250a6ec3f3d14b081c262af91046d 100644
--- a/src/SafeDequeue.h
+++ b/src/SafeDequeue.h
@@ -27,6 +27,7 @@
typedef pair<LDDState *, MDD> couple;
typedef pair<couple, Set> Pair;
+typedef pair<LDDState *, int> couple_th;
struct empty_queue: std::exception {
~empty_queue() {};
const char* what() const noexcept {return "";}
@@ -62,16 +63,6 @@ class SafeDequeue {
SafeDequeue& operator= ( const SafeDequeue& ) = delete;
void push ( T new_value );
bool try_pop ( T& value );
- std::shared_ptr<T> try_pop();
- void wait_and_pop ( T& value ) {
- std::unique_lock<std::mutex> lk ( mut );
- data_cond.wait ( lk,[this] {return !data_queue.empty();} );
- value=data_queue.front();
- data_queue.pop();
- };
-
-
- std::shared_ptr<T> wait_and_pop();
bool empty() const;
};
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 74b7e603255476e2ff2a546b56ddbcae3fd85902..e48c97f5281f2dfd6d944bea4d2bd12bc08bcd37 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -4,7 +4,7 @@
#include "SogKripkeIteratorTh.h"
-SogKripkeIteratorTh::SogKripkeIteratorTh ( const LDDState* lddstate, bdd cnd ) :m_lddstate ( lddstate ), kripke_succ_iterator ( cnd )
+SogKripkeIteratorTh::SogKripkeIteratorTh ( LDDState* lddstate, bdd cnd ) :m_lddstate ( lddstate ), kripke_succ_iterator ( cnd )
{
for ( int i=0; i<m_lddstate->getSuccessors()->size(); i++ ) {
m_lsucc.push_back ( m_lddstate->getSuccessors()->at ( i ) );
@@ -50,21 +50,16 @@ SogKripkeStateTh* SogKripkeIteratorTh::dst() const
bdd SogKripkeIteratorTh::cond() const
{
- //cout<<"entering "<<__func__<<endl;
if ( m_lsucc.at ( m_current_edge ).second==-1 ) {
return bddtrue;
}
spot::formula f=spot::formula::ap (string(m_builder->getTransition ( m_lsucc.at ( m_current_edge ).second )));
spot::bdd_dict *p=m_dict_ptr->get();
bdd result=bdd_ithvar ( ( p->var_map.find ( f ) )->second );
- //cout<<"leaving "<<__func__<<endl;
return result & spot::kripke_succ_iterator::cond();
}
-/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
- //cout<<"Iterator acc()\n";
- return 0U;
-}*/
+
SogKripkeIteratorTh::~SogKripkeIteratorTh()
{
//dtor
@@ -79,4 +74,4 @@ void SogKripkeIteratorTh::recycle ( LDDState* aggregate, bdd cond )
ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
LDDState SogKripkeIteratorTh::m_deadlock;
-LDDState SogKripkeIteratorTh::m_div;
+//LDDState SogKripkeIteratorTh::m_div;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
index c5307b4c2549d541dc53ca7998de158de6258cfb..b3069a160b1926ebb89e47562e67b1a5640c7dfd 100644
--- a/src/SogKripkeIteratorTh.h
+++ b/src/SogKripkeIteratorTh.h
@@ -8,11 +8,11 @@ class SogKripkeIteratorTh : public spot::kripke_succ_iterator
{
public:
static LDDState m_deadlock;
- static LDDState m_div;
+ //static LDDState m_div;
static ModelCheckBaseMT * m_builder;
static spot::bdd_dict_ptr* m_dict_ptr;
// sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
- SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd);
+ SogKripkeIteratorTh(LDDState* lddstate, bdd cnd);
virtual ~SogKripkeIteratorTh();
bool first() override;
bool next() override;
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index f2836b17d8c46cfff59a25b6038211d598b619aa..7391a23938268f0bbbc980baff00133c7b90f650 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -19,10 +19,10 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder)
SogKripkeIteratorTh::m_deadlock.setLDDValue(1);
SogKripkeIteratorTh::m_deadlock.setVisited();
SogKripkeIteratorTh::m_deadlock.setCompletedSucc();
- SogKripkeIteratorTh::m_div.setLDDValue(0);
+ /*SogKripkeIteratorTh::m_div.setLDDValue(0);
SogKripkeIteratorTh::m_div.setVisited();
SogKripkeIteratorTh::m_div.setCompletedSucc();
- SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));
+ SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));*/
}
SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
@@ -38,7 +38,7 @@ SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *bu
state* SogKripkeTh::get_init_state() const {
LDDState *ss=m_builder->getInitialMetaState();
- return new SogKripkeStateTh(ss);//new SpotSogState();
+ return new SogKripkeStateTh(ss);
}
// Allows to print state label representing its id
@@ -48,7 +48,7 @@ std::string SogKripkeTh::format_state(const spot::state* s) const
auto ss = static_cast<const SogKripkeStateTh*>(s);
std::ostringstream out;
out << "( " << ss->getLDDState()->getLDDValue() << ")";
- // cout << " ( " << ss->getLDDState()->getLDDValue() << ")";
+
return out.str();
}
diff --git a/src/SylvanCacheWrapper.h b/src/SylvanCacheWrapper.h
index 0e651e286432d22f1224c49822ed9ba90cb4f9bb..2a3a255238b2a7f38adb614d21be693aab38197c 100644
--- a/src/SylvanCacheWrapper.h
+++ b/src/SylvanCacheWrapper.h
@@ -14,19 +14,19 @@ extern "C" {
#endif /* __cplusplus */
// MDD operations
-static const uint64_t CACHE_MDD_RELPROD = (20LL<<40);
-static const uint64_t CACHE_MDD_MINUS = (21LL<<40);
-static const uint64_t CACHE_MDD_UNION = (22LL<<40);
-static const uint64_t CACHE_MDD_INTERSECT = (23LL<<40);
-static const uint64_t CACHE_MDD_PROJECT = (24LL<<40);
-static const uint64_t CACHE_MDD_JOIN = (25LL<<40);
-static const uint64_t CACHE_MDD_MATCH = (26LL<<40);
-static const uint64_t CACHE_MDD_RELPREV = (27LL<<40);
-static const uint64_t CACHE_MDD_SATCOUNT = (28LL<<40);
-static const uint64_t CACHE_MDD_DIVIDE = (29LL<<40);
-static const uint64_t CACHE_LDD_MINUS = (30LL<<40);
-static const uint64_t CACHE_LDD_FIRE = (31LL<<40);
-static const uint64_t CACHE_LDD_UNION = (32LL<<40);
+static const uint64_t CACHE_MDD_RELPROD = (10LL<<40);
+static const uint64_t CACHE_MDD_MINUS = (11LL<<40);
+static const uint64_t CACHE_MDD_UNION = (12LL<<40);
+static const uint64_t CACHE_MDD_INTERSECT = (13LL<<40);
+static const uint64_t CACHE_MDD_PROJECT = (14LL<<40);
+static const uint64_t CACHE_MDD_JOIN = (15LL<<40);
+static const uint64_t CACHE_MDD_MATCH = (16LL<<40);
+static const uint64_t CACHE_MDD_RELPREV = (17LL<<40);
+static const uint64_t CACHE_MDD_SATCOUNT = (18LL<<40);
+static const uint64_t CACHE_MDD_DIVIDE = (19LL<<40);
+static const uint64_t CACHE_LDD_MINUS = (20LL<<40);
+static const uint64_t CACHE_LDD_FIRE = (21LL<<40);
+static const uint64_t CACHE_LDD_UNION = (22LL<<40);
#ifdef __cplusplus
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 77a128120a3eba5614baa37e7dfd60f88e073cb0..8c6cd3d1ca7cd5f143171e943f7cc98b8b7dc77b 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -13,6 +13,7 @@
#include <sys/mman.h> // for mmap
#include <iostream>
#include <string>
+#include <stack>
#include "SylvanCacheWrapper.h"
#include "SylvanWrapper.h"
@@ -38,18 +39,18 @@ MDD lddmc_true = 1;
uint64_t SylvanWrapper::getMarksCount(MDD cmark) {
//typedef pair<string,MDD> Pair_stack;
- vector<MDD> local_stack;
+ stack<MDD> local_stack;
uint64_t compteur = 0;
MDD explore_mdd;
- local_stack.push_back(cmark);
+ local_stack.push(cmark);
do {
- explore_mdd = local_stack.back();
- local_stack.pop_back();
+ explore_mdd = local_stack.top();
+ local_stack.pop();
compteur++;
while (explore_mdd != lddmc_false && explore_mdd != lddmc_true) {
mddnode_t n_val = GETNODE(explore_mdd);
if (mddnode_getright(n_val) != lddmc_false) {
- local_stack.push_back(mddnode_getright(n_val));
+ local_stack.push(mddnode_getright(n_val));
}
//unsigned int val = mddnode_getvalue ( n_val );
explore_mdd = mddnode_getdown(n_val);
@@ -136,7 +137,7 @@ llmsset2_t SylvanWrapper::llmsset_create(size_t initial_size, size_t max_size) {
// that is a problem with multiple tables.
// so, for now, do NOT use multiple tables!!
- /*LACE_ME;*/
+
INIT_THREAD_LOCAL(my_region);
llmsset_reset_region();
@@ -241,10 +242,7 @@ void SylvanWrapper::sylvan_init_package(void) {
}
void SylvanWrapper::sylvan_init_ldd() {
- /*sylvan_register_quit(lddmc_quit);
- sylvan_gc_add_mark(TASK(lddmc_gc_mark_external_refs));
- sylvan_gc_add_mark(TASK(lddmc_gc_mark_protected));
- sylvan_gc_add_mark(TASK(lddmc_gc_mark_serialize));*/
+
//m_lddmc_protected_created=0; // Should be initialized in the constructor
refs_create(&m_lddmc_refs, 1024);
if (!m_lddmc_protected_created) {
@@ -252,7 +250,7 @@ void SylvanWrapper::sylvan_init_ldd() {
m_lddmc_protected_created = 1;
}
- //LACE_ME;
+
lddmc_refs_init();
}
@@ -262,8 +260,7 @@ void SylvanWrapper::lddmc_refs_init_task() {
s->pend = s->pbegin + 1024;
s->rcur = s->rbegin = (MDD *) malloc(sizeof(MDD) * 1024);
s->rend = s->rbegin + 1024;
- /* s->scur = s->sbegin = (lddmc_refs_task_t)malloc(sizeof(struct lddmc_refs_task) * 1024);
- s->send = s->sbegin + 1024;*/
+
SET_THREAD_LOCAL(lddmc_refs_key, s);
}
@@ -392,11 +389,7 @@ MDD SylvanWrapper::lddmc_makenode(uint32_t value, MDD ifeq, MDD ifneq) {
}
}
- /*if (created) {
- sylvan_stats_count(LDD_NODES_CREATED);
- }
- else sylvan_stats_count(LDD_NODES_REUSED);*/
return (MDD) index;
}
@@ -634,7 +627,7 @@ MDD SylvanWrapper::lddmc_union_mono(MDD a, MDD b) {
/* Access cache */
MDD result;
if (SylvanCacheWrapper::cache_get3(CACHE_LDD_UNION, a, b, 0, &result)) {
- // std::cout<<"Cache succeeded!"<<std::endl;
+ //cout<<"cache get "<<__func__ <<endl;
return result;
}
@@ -711,7 +704,6 @@ MDD SylvanWrapper::lddmc_make_copynode(MDD ifeq, MDD ifneq) {
bool SylvanWrapper::isSingleMDD(MDD mdd) {
mddnode_t node;
-
while (mdd > lddmc_true) {
node = GETNODE(mdd);
if (mddnode_getright(node) != lddmc_false) return false;
@@ -721,7 +713,7 @@ bool SylvanWrapper::isSingleMDD(MDD mdd) {
}
// Renvoie le nbre de noeuds à un niveau donné
-int SylvanWrapper::get_mddnbr(MDD mdd, int level) {
+int SylvanWrapper::get_mddnbr(MDD mdd, unsigned int level) {
mddnode_t node;
for (int j = 0; j < level; j++) {
node = GETNODE(mdd);
@@ -816,7 +808,7 @@ MDD SylvanWrapper::ldd_minus(MDD a, MDD b) {
}
-MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, MDD minus, MDD plus) {
+MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, const MDD minus,const MDD plus) {
// for an empty set of source states, or an empty transition relation, return the empty set
if (cmark == lddmc_true) return lddmc_true;
if (minus == lddmc_false || plus == lddmc_false) return lddmc_false;
@@ -825,6 +817,7 @@ MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, MDD minus, MDD plus) {
MDD _cmark = cmark, _minus = minus, _plus = plus;
if (SylvanCacheWrapper::cache_get3(CACHE_LDD_FIRE, cmark, minus, plus, &result)) {
+
return result;
}
MDD cache_cmark = cmark;
@@ -911,40 +904,38 @@ MDD SylvanWrapper::lddmc_project(const MDD mdd, const MDD proj) {
int SylvanWrapper::isGCRequired() {
return (m_g_created > llmsset_get_size(m_nodes) / 2);
}
-
+/*
+ * Convert MDD cmark to a string
+ */
void SylvanWrapper::convert_wholemdd_stringcpp(MDD cmark, string &res) {
typedef pair<string, MDD> Pair_stack;
- vector<Pair_stack> local_stack;
-
+ stack<Pair_stack> local_stack;
unsigned int compteur = 0;
MDD explore_mdd = cmark;
-
string chaine;
-
res = " ";
- local_stack.push_back(Pair_stack(chaine, cmark));
+ local_stack.push(Pair_stack(chaine, cmark));
do {
- Pair_stack element = local_stack.back();
+ Pair_stack element = local_stack.top();
chaine = element.first;
explore_mdd = element.second;
- local_stack.pop_back();
+ local_stack.pop();
compteur++;
while (explore_mdd != lddmc_false && explore_mdd != lddmc_true) {
mddnode_t n_val = GETNODE(explore_mdd);
if (mddnode_getright(n_val) != lddmc_false) {
- local_stack.push_back(Pair_stack(chaine, mddnode_getright(n_val)));
+ local_stack.push(Pair_stack(chaine, mddnode_getright(n_val)));
}
unsigned int val = mddnode_getvalue(n_val);
-
chaine.push_back((unsigned char) (val) + 1);
explore_mdd = mddnode_getdown(n_val);
}
- /*printchaine(&chaine);printf("\n");*/
res += chaine;
- } while (local_stack.size() != 0);
+ } while (!local_stack.empty());
//delete chaine;
compteur = (compteur << 1) | 1;
+ //cout<<"compteur "<<compteur<<endl;
res[1] = (unsigned char) ((compteur >> 8) + 1);
res[0] = (unsigned char) (compteur & 255);
@@ -952,7 +943,6 @@ void SylvanWrapper::convert_wholemdd_stringcpp(MDD cmark, string &res) {
void SylvanWrapper::sylvan_gc_seq() {
if (m_g_created > llmsset_get_size(m_nodes) / 1000) {
- cout<<"Cache executed"<<endl;
SylvanCacheWrapper::cache_clear();
llmsset_clear_data(m_nodes);
ldd_gc_mark_protected();
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
index 97aeb28dbe46a65304c5679d6e6e5714105efb4e..58030b764c5223763089741028ff6b6272f10d15 100644
--- a/src/SylvanWrapper.h
+++ b/src/SylvanWrapper.h
@@ -6,6 +6,7 @@
#define PMC_SOG_SYLVANWRAPPER_H
#include <cstdint>
#include <cstddef>
+#include <string>
/**
* Lockless hash table (set) to store 16-byte keys.
@@ -121,7 +122,7 @@ public:
static void sylvan_set_limits(size_t memorycap, int table_ratio, int initial_ratio);
- static void sylvan_init_package(void);
+ static void sylvan_init_package();
inline static mddnode_t GETNODE(MDD mdd) { return ((mddnode_t) llmsset_index_to_ptr(m_nodes, mdd)); }
@@ -176,7 +177,7 @@ public:
static bool isSingleMDD(MDD mdd);
- static int get_mddnbr(MDD mdd, int level);
+ static int get_mddnbr(MDD mdd, unsigned int level);
static MDD ldd_divide_rec(MDD a, int level);
@@ -184,7 +185,7 @@ public:
static MDD ldd_minus(MDD a, MDD b);
- static MDD lddmc_firing_mono(MDD cmark, MDD minus, MDD plus);
+ static MDD lddmc_firing_mono(MDD cmark, const MDD minus, const MDD plus);
static size_t lddmc_nodecount_mark(MDD mdd);
diff --git a/src/TransSylvan.cpp b/src/TransSylvan.cpp
index c72581f05ccdd6ec3767888f9bcddc91380cd9be..fd9e0c8070564657e3c818452a1ae95334e8d63b 100644
--- a/src/TransSylvan.cpp
+++ b/src/TransSylvan.cpp
@@ -1,6 +1,3 @@
-#include <cstdint>
-#include <cstddef>
-#include <string>
#include "SylvanWrapper.h"
#include "TransSylvan.h"
@@ -9,22 +6,12 @@ TransSylvan::TransSylvan(const MDD &_minus, const MDD &_plus):m_minus(_minus),m_
//ctor
}
-TransSylvan::~TransSylvan()
-{
- //dtor
-}
-void TransSylvan::setMinus(MDD _minus) {
- m_minus=_minus;
-}
-
-void TransSylvan::setPlus(MDD _plus) {
- m_plus=_plus;
-}
+TransSylvan::~TransSylvan()=default;
-MDD TransSylvan::getMinus() {
+MDD TransSylvan::getMinus() const {
return m_minus;
}
-MDD TransSylvan::getPlus() {
+MDD TransSylvan::getPlus() const {
return m_plus;
}
diff --git a/src/TransSylvan.h b/src/TransSylvan.h
index 0c9849c431a8700ea0a764de31386cd87ecb8676..ca24694cbe3817c38d0fc306006782ae0c1db7fd 100755
--- a/src/TransSylvan.h
+++ b/src/TransSylvan.h
@@ -7,12 +7,8 @@ class TransSylvan {
public:
TransSylvan(const MDD &_minus, const MDD &_plus);
virtual ~TransSylvan();
- void setMinus(MDD _minus);
- void setPlus(MDD _plus);
- MDD getMinus();
- MDD getPlus();
-
- protected:
+ [[nodiscard]] MDD getMinus() const;
+ [[nodiscard]] MDD getPlus() const;
private:
MDD m_minus, m_plus;
};
diff --git a/src/main.cpp b/src/main.cpp
index c0948776fb20e0b77aff46c7bee8d21d5d1b86ba..842624afab5845280b961252ec25da8a7ded4037 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -31,7 +31,7 @@
#include "SogKripkeTh.h"
#include "HybridKripke.h"
#include "SylvanWrapper.h"
-
+#include "PMCSOGConfig.h"
// #include "RdPBDD.h"
using namespace std;
@@ -78,9 +78,8 @@ void displayCheckResult(bool res) {
else
cout << "Property is violated..." << endl;
}
-void displayTime(auto startTime, auto finalTime) {
- cout << "Verification duration : " << std::chrono::duration_cast < std::chrono::milliseconds
- > (finalTime - startTime).count() << " milliseconds\n";
+void displayTime(auto startTime,auto finalTime) {
+ cout << "Verification duration : " << std::chrono::duration_cast < std::chrono::milliseconds> (finalTime - startTime).count() << " milliseconds\n";
}
/***********************************************/
@@ -96,13 +95,18 @@ int main(int argc, char **argv) {
}
nb_th = atoi(argv[2]) == 0 ? 1 : atoi(argv[2]);
-
- cout << "Net file : " << argv[3] << endl;
- cout << "Formula file : " << formula << endl;
- cout << "Checking algorithm : " << algorithm << endl;
-
- cout << "thread : " << argv[2] << endl;
-
+ MPI_Init(&argc, &argv);
+ MPI_Comm_size(MPI_COMM_WORLD, &n_tasks);
+ MPI_Comm_rank(MPI_COMM_WORLD, &task_id);
+ if (!task_id) {
+ cout << "PMC-SOG : Parallel Model Checking tool based on Symbolic Observation Graphs " << endl;
+ cout << "Version " <<PMCSOG_VERSION_MAJOR<<"."<<PMCSOG_VERSION_MINOR<<"."<<PMCSOG_VERSION_PATCH<<endl;
+ cout << "(c) 2018 - 2020"<<endl;
+ cout << "Net file : " << argv[3] << endl;
+ cout << "Formula file : " << formula << endl;
+ cout << "Checking algorithm : " << algorithm << endl;
+ cout << "#threads : " << nb_th << endl;
+ }
if (nb_th == 0) {
cout << "number of thread <= 0 " << endl;
exit(0);
@@ -111,13 +115,8 @@ int main(int argc, char **argv) {
cout << "______________________________________\n";
cout << "Fetching formula..." << endl;
set<string> list_propositions = buildPropositions(formula);
-
NewNet Rnewnet(argv[3], list_propositions);
- MPI_Init(&argc, &argv);
- MPI_Comm_size(MPI_COMM_WORLD, &n_tasks);
- MPI_Comm_rank(MPI_COMM_WORLD, &task_id);
-
if (n_tasks == 1) {
if (n_tasks == 1 && (!strcmp(argv[1], "otfPR") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP"))) {
@@ -133,22 +132,8 @@ int main(int argc, char **argv) {
spot::twa_graph_ptr af = spot::translator(d).run(not_f);
cout << "Formula automata built.\n";
- /*cout << "Want to save the graph in a dot file ?";
- char c;
- cin >> c;
- if (c == 'y') {
- fstream file;
- string st(formula);
- st += ".dot";
- file.open(st.c_str(), fstream::out);
- spot::print_dot(file, af);
- file.close();
- }
- cout << "Loading net information..." << endl;*/
ModelCheckBaseMT *mcl;
- /*if (!strcmp(argv[1], "otfL"))
- mcl = new ModelCheckLace(Rnewnet, nb_th);
- else*/
+
if (!strcmp(argv[1], "otfP"))
mcl = new ModelCheckerTh(Rnewnet, nb_th);
else if (!strcmp(argv[1], "otfC"))
@@ -177,13 +162,6 @@ int main(int argc, char **argv) {
auto finalTime = std::chrono::steady_clock::now();
displayTime(startTime, finalTime);
displayCheckResult(res);
- /****************************/
-
- /*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();
@@ -191,24 +169,9 @@ int main(int argc, char **argv) {
auto finalTime = std::chrono::steady_clock::now();
displayTime(startTime, finalTime);
displayCheckResult(res);
- /*
- if (!resauto run = k->intersecting_run(af)) {
- cout << "formula is violated by the following run:\n" << *run << endl;
- cout << "==================================" << endl;
- /*run->highlight(5); // 5 is a color number.
- fstream file;
- file.open("violated.dot",fstream::out);
- cout<<"Property is violated!"<<endl;
- cout<<"Check the dot file."<<endl;
- spot::print_dot(file, k, ".kA");
- file.close();*/
- /*} else {
- std::cout << "formula is verified\n";
- auto finalTime = std::chrono::high_resolution_clock::now();
- displayTime(startTime, finalTime);
-
- }*/
}
+ mcl->finish();
+ cout<<"Number of built aggregates: "<<mcl->getGraph()->m_GONodes.size()<<endl;
delete mcl;
}
diff --git a/src/md5_hash.h b/src/md5_hash.h
new file mode 100644
index 0000000000000000000000000000000000000000..086defced6893f4f689f8b8e1b181f8561859168
--- /dev/null
+++ b/src/md5_hash.h
@@ -0,0 +1,204 @@
+//
+// Created by chiheb on 10/12/2020.
+//
+
+#ifndef PMC_SOG_MD5_HASH_H
+#define PMC_SOG_MD5_HASH_H
+
+
+#include <string>
+#include <array>
+
+// info and algorithm: https://en.wikipedia.org/wiki/MD5
+class md5_hash
+{
+public:
+
+ /**
+ * \param message message to processing
+ * \return get md5-hash from message
+ */
+ [[nodiscard]] static void compute(const std::string& message,unsigned char *result)
+ {
+ // These vars will contain the hash
+ uint32_t a0 = 0x67452301, b0 = 0xefcdab89, c0 = 0x98badcfe, d0 = 0x10325476;
+ size_t new_len = message.size() + 1;
+
+ //Pre-processing:
+ //append "1" bit to message
+ //append "0" bits until message length in bits ≡ 448 (mod 512)
+ //append length mod (2^64) to message
+ while (new_len % (512 / 8) != 448 / 8)
+ new_len++;
+
+ std::string msg_copy = message; msg_copy.resize(new_len + 8);
+ msg_copy[message.size()] = 0x80; // append the "1" bit; most significant bit is "first"
+
+ std::array<uint8_t, 4> bytes = md5_hash::uint32_to_4_bytes(message.size() * 8);
+ for (size_t i = new_len; i < new_len + 4; i++)
+ msg_copy[i] = bytes[i - new_len];
+
+ bytes = md5_hash::uint32_to_4_bytes(message.size() >> 29);
+ for (size_t i = new_len + 4; i < new_len + 8; i++)
+ msg_copy[i] = bytes[i - new_len - 4];
+
+ // process the message in successive 512-bit chunks
+ for (size_t i = 0; i < new_len; i += (512 / 8))
+ {
+ uint32_t w[16];
+
+ for (size_t j = 0; j < 16; j++)
+ {
+ const std::array<uint8_t, 4> array {
+ static_cast<uint8_t>(msg_copy[i + j * 4]),
+ static_cast<uint8_t>(msg_copy[i + j * 4 + 1]),
+ static_cast<uint8_t>(msg_copy[i + j * 4 + 2]),
+ static_cast<uint8_t>(msg_copy[i + j * 4 + 3]),
+ };
+
+ w[j] = md5_hash::uint32_from_4_bytes(array);
+ }
+
+ uint32_t a = a0, b = b0, c = c0, d = d0;
+
+ for (size_t j = 0; j < 64; j++)
+ {
+ uint32_t f, g;
+
+ // F(B, C, D)= (B and C) or (not B and D)
+ // G(B, C, D)= (B and D) or (C and not D)
+ // H(B, C, D)= B xor C xor D
+ // I(B, C, D)= C xor (B or not D)
+ if (j < 16)
+ {
+ f = (b & c) | ((~b) & d);
+ g = j;
+ }
+ else if (j < 32)
+ {
+ f = (d & b) | (c & (~d));
+ g = (5 * j + 1) % 16;
+ }
+ else if (j < 48)
+ {
+ f = b ^ c ^ d;
+ g = (3 * j + 5) % 16;
+ }
+ else
+ {
+ f = c ^ (b | (~d));
+ g = (7 * j) % 16;
+ }
+
+ const uint32_t temp = d;
+ d = c;
+ c = b;
+ b = b + md5_hash::rotate_left((a + f + md5_hash::k[j] + w[g]), md5_hash::r[j]);
+ a = temp;
+ }
+
+ // add this chunk's hash to result so far:
+ a0 += a;
+ b0 += b;
+ c0 += c;
+ d0 += d;
+ }
+
+ const std::array<uint8_t, 4> a0_arr = md5_hash::uint32_to_4_bytes(a0);
+ const std::array<uint8_t, 4> b0_arr = md5_hash::uint32_to_4_bytes(b0);
+ const std::array<uint8_t, 4> c0_arr = md5_hash::uint32_to_4_bytes(c0);
+ const std::array<uint8_t, 4> d0_arr = md5_hash::uint32_to_4_bytes(d0);
+
+ // append results bytes
+
+ result[0] = a0_arr[0];
+ result[1] = a0_arr[1];
+ result[2] = a0_arr[2];
+ result[3] = a0_arr[3];
+
+ result[4]=b0_arr[0];
+ result[5]=b0_arr[1];
+ result[6]=b0_arr[2];
+ result[7]=b0_arr[3];
+
+ result[8]=c0_arr[0];
+ result[9]=c0_arr[1];
+ result[10]=c0_arr[2];
+ result[11]=c0_arr[3];
+
+ result[12]=d0_arr[0];
+ result[13]=d0_arr[1];
+ result[14]=d0_arr[2];
+ result[15]=d0_arr[3];
+
+
+ // return result;
+ }
+private:
+ md5_hash() = default;
+
+ // rol command: https://www.aldeid.com/wiki/X86-assembly/Instructions/rol
+ static uint32_t rotate_left(const uint32_t x, const int32_t n)
+ {
+ return (x << n) | (x >> (32 - n));
+ }
+
+ // cast unsigned integer to to a four-element array
+ static std::array<uint8_t, 4> uint32_to_4_bytes(uint32_t value)
+ {
+ std::array<uint8_t, 4> bytes{};
+
+ bytes[0] = static_cast<uint8_t>(value);
+ bytes[1] = static_cast<uint8_t>(value >> 8);
+ bytes[2] = static_cast<uint8_t>(value >> 16);
+ bytes[3] = static_cast<uint8_t>(value >> 24);
+
+ return bytes;
+ }
+
+ // cast a four-element array to unsigned integer
+ static uint32_t uint32_from_4_bytes(std::array<uint8_t, 4> bytes)
+ {
+ uint32_t value = 0;
+
+ value = (value << 8) + bytes[3];
+ value = (value << 8) + bytes[2];
+ value = (value << 8) + bytes[1];
+ value = (value << 8) + bytes[0];
+
+ return value;
+ }
+
+ // table, computed by this code:
+ /*
+ for i from 0 to 63
+ K[i] : = floor(232 × abs(sin(i + 1)))
+ */
+ constexpr static uint32_t k[64] = {
+ 0xd76aa478, 0xe8c7b756, 0x242070db, 0xc1bdceee ,
+ 0xf57c0faf, 0x4787c62a, 0xa8304613, 0xfd469501 ,
+ 0x698098d8, 0x8b44f7af, 0xffff5bb1, 0x895cd7be ,
+ 0x6b901122, 0xfd987193, 0xa679438e, 0x49b40821 ,
+ 0xf61e2562, 0xc040b340, 0x265e5a51, 0xe9b6c7aa ,
+ 0xd62f105d, 0x02441453, 0xd8a1e681, 0xe7d3fbc8 ,
+ 0x21e1cde6, 0xc33707d6, 0xf4d50d87, 0x455a14ed ,
+ 0xa9e3e905, 0xfcefa3f8, 0x676f02d9, 0x8d2a4c8a ,
+ 0xfffa3942, 0x8771f681, 0x6d9d6122, 0xfde5380c ,
+ 0xa4beea44, 0x4bdecfa9, 0xf6bb4b60, 0xbebfbc70 ,
+ 0x289b7ec6, 0xeaa127fa, 0xd4ef3085, 0x04881d05 ,
+ 0xd9d4d039, 0xe6db99e5, 0x1fa27cf8, 0xc4ac5665 ,
+ 0xf4292244, 0x432aff97, 0xab9423a7, 0xfc93a039 ,
+ 0x655b59c3, 0x8f0ccc92, 0xffeff47d, 0x85845dd1 ,
+ 0x6fa87e4f, 0xfe2ce6e0, 0xa3014314, 0x4e0811a1 ,
+ 0xf7537e82, 0xbd3af235, 0x2ad7d2bb, 0xeb86d391
+ };
+
+ // specifies the per-round shift amounts
+ constexpr static uint32_t r[64] = {
+ 7, 12, 17, 22, 7, 12, 17, 22, 7, 12, 17, 22, 7, 12, 17, 22,
+ 5, 9, 14, 20, 5, 9, 14, 20, 5, 9, 14, 20, 5, 9, 14, 20,
+ 4, 11, 16, 23, 4, 11, 16, 23, 4, 11, 16, 23, 4, 11, 16, 23,
+ 6, 10, 15, 21, 6, 10, 15, 21, 6, 10, 15, 21, 6, 10, 15, 21
+ };
+};
+#endif //PMC_SOG_MD5_HASH_H