diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 26f1d64e8f247f28c2f49bd22dcf439eaacd1617..75f543caf8688ac67a8a55cdc045f40a1066ef3e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -75,6 +75,7 @@ add_executable(mc-sog main.cpp
SylvanCacheWrapper.cpp SylvanCacheWrapper.h
MCMultiCore/ModelCheckerCPPThread.cpp MCMultiCore/ModelCheckerCPPThread.h
MCMultiCore/ModelCheckerTh.cpp MCMultiCore/ModelCheckerTh.h
+ MCMultiCore/MCThReqPor.cpp MCMultiCore/MCThReqPor.h
threadSOG.cpp threadSOG.h
HybridSOG.cpp HybridSOG.h
Hybrid/MCHybrid/MCHybridSOG.cpp Hybrid/MCHybrid/MCHybridSOG.h
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 8fc570effdf183765ba814ba2962194f1c9c4fd6..d3e397eeee434c5c082c97023fade5805eee958f 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -35,7 +35,7 @@ Set CommonSOG::firable_obs(MDD State) {
return res;
}
-MDD CommonSOG::get_successor(MDD From, int t) {
+MDD CommonSOG::get_successor(const MDD& From, const int& t) {
return SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(t)].getMinus(), m_tb_relation[(t)].getPlus());
}
@@ -123,18 +123,15 @@ MDD CommonSOG::Canonize(MDD s, unsigned int level) {
/**** Detect divergence in an agregate ****/
bool CommonSOG::Set_Div(MDD &M) const {
-
if (m_nonObservable.empty()) {
return false;
}
- Set::const_iterator i;
- MDD Reached, From;
-
- From = M;
+ MDD Reached, From {M};
do {
Reached = lddmc_false;
- for (i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
- MDD To = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ for (auto i : m_nonObservable )
+ {
+ MDD To = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(i)].getMinus(), m_tb_relation[(i)].getPlus());
Reached = SylvanWrapper::lddmc_union_mono(Reached, To);
}
@@ -151,9 +148,7 @@ bool CommonSOG::Set_Bloc(MDD &M) const {
MDD cur = lddmc_true;
for (auto i : m_tb_relation) {
-
cur = cur & (i.getMinus());
-
}
return ((M & cur) != lddmc_false);
//BLOCAGE
@@ -252,5 +247,28 @@ void CommonSOG::loadNetFromFile() {
}
delete[] prec;
delete[] postc;
+}
+
+void CommonSOG::AddConflict(const MDD &S, const int &transition,Set &le) {
+ // if ()
+ MDD img= get_successor(S,transition);
+ if (img!=lddmc_true && img!=lddmc_false) {
+ for (auto i=0; i<m_transitions.size();i++) {
+ if (i!=transition) {
+ auto interPre = [this](const int & t1,const int &t2)-> bool {
+ auto & preT1=m_transitions[t1].pre;
+ auto & preT2=m_transitions[t2].pre;
+ bool found=false;
+ for (auto elt : preT1);
+ return true;
+ };
+ }
+ }
+ }
+
+
+
+}
+bool CommonSOG::isFirable(const int &transition) {
}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index da68e0bca4175c46ab6abb45f3ec3a9983cee92e..5118d65c98009d383aa1e64983d24509a0013cd1 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -50,7 +50,7 @@ class CommonSOG
vector<class Transition> m_transitions;
MDD Accessible_epsilon(MDD From);
Set firable_obs(MDD State);
- MDD get_successor(MDD From, int t);
+ MDD get_successor(const MDD& From,const int& t);
MDD ImageForward(MDD From);
MDD Canonize(MDD s, unsigned int level);
bool Set_Div(MDD &M) const;
@@ -59,8 +59,10 @@ class CommonSOG
std::mutex m_graph_mutex,m_gc_mutex;
atomic<uint8_t> m_gc;
volatile bool m_finish=false;
+ // Functions for POR
+ void AddConflict(const MDD& S,const int &transition,Set& ample);
private:
-
+ bool isFirable(const int &transition);
};
#endif // COMMONSOG_H
diff --git a/src/Hybrid/MCHybrid/MCHybridSOG.cpp b/src/Hybrid/MCHybrid/MCHybridSOG.cpp
index dd5980c880e47078723d403fc9c0925f77b1d1ec..121d3645b27362345f27ab67ced29f5cf1e09622 100644
--- a/src/Hybrid/MCHybrid/MCHybridSOG.cpp
+++ b/src/Hybrid/MCHybrid/MCHybridSOG.cpp
@@ -112,7 +112,7 @@ void *MCHybridSOG::doCompute() {
/******************************* Construction des aggregats ************************************/
else {
- while (m_Terminated == false) {
+ while (!m_Terminated) {
std::unique_lock<std::mutex> lk(m_mutexCond);
m_condStack.wait(lk, [this] { return !m_common_stack.empty() || !m_received_msg.empty() || m_Terminated; });
lk.unlock();
diff --git a/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp b/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
index 5ef9a912762f00d710c2dfe7420e2e0721f30a6e..7bbd91e84fc736288487fbef7334b8ba8e3e2229 100644
--- a/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
+++ b/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
@@ -22,8 +22,7 @@
#define REDUCE 1
using namespace std;
-MCHybridSOGReq::MCHybridSOGReq(const NewNet &R, MPI_Comm &comm_world, bool init) {
- m_comm_world = comm_world;
+MCHybridSOGReq::MCHybridSOGReq(const NewNet &R, MPI_Comm &comm_world, bool init):m_comm_world(comm_world) {
initializeLDD();
m_net = &R;
m_init = init;
@@ -425,8 +424,8 @@ void MCHybridSOGReq::sendPropToMC(size_t pos) {
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);
+ for (auto it : marked_places) {
+ memcpy(mess_to_send + indice, &(it), 2);
indice += 2;
}
memcpy(mess_to_send + indice, &s_up, 2);
diff --git a/src/MCMultiCore/MCThReqPor.cpp b/src/MCMultiCore/MCThReqPor.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..719c200edbdfa2d49c96f34e32240d693377531b
--- /dev/null
+++ b/src/MCMultiCore/MCThReqPor.cpp
@@ -0,0 +1,159 @@
+#include "MCThReqPor.h"
+#include <unistd.h>
+#include <thread>
+
+#define LEVEL 3
+
+MCThReqPor::MCThReqPor(const NewNet &R, int nbThread) : ModelCheckBaseMT(R, nbThread) {
+}
+
+
+void MCThReqPor::preConfigure() {
+ //cout<<"Enter : "<<__func__ <<endl;
+ initializeLDD();
+ loadNetFromFile();
+}
+
+/**
+ * Creates builder threads
+ */
+void MCThReqPor::ComputeTh_Succ() {
+
+ m_id_thread = 0;
+ //cout<<"Enter : "<<__func__ <<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 *MCThReqPor::getInitialMetaState() {
+
+ if (m_graph->getInitialAggregate() != nullptr) {
+ return m_graph->getInitialAggregate();
+ }
+ ComputeTh_Succ();
+ LDDState *c = new LDDState;
+ MDD initial_meta_state = Accessible_epsilon(m_initialMarking);
+ SylvanWrapper::lddmc_refs_push(initial_meta_state);
+ c->m_lddstate = initial_meta_state;
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
+ 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 @agregate
+ */
+void MCThReqPor::buildSucc(LDDState *agregate) {
+ if (!agregate->isVisited()) {
+ agregate->setVisited();
+ 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 *MCThReqPor::threadHandler(void *context) {
+ return ((MCThReqPor *) context)->Compute_successors();
+}
+
+
+void *MCThReqPor::Compute_successors() {
+ 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);
+ {
+ 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));
+ }
+ 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();
+
+ }
+ } while (!m_finish);
+
+
+}
+
+
+MCThReqPor::~MCThReqPor() {
+ //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/MCMultiCore/MCThReqPor.h b/src/MCMultiCore/MCThReqPor.h
new file mode 100644
index 0000000000000000000000000000000000000000..8b4c345956bac779ddc089a44919caebd77cff75
--- /dev/null
+++ b/src/MCMultiCore/MCThReqPor.h
@@ -0,0 +1,30 @@
+#ifndef MCTHREQPOR_H
+#define MCTHREQPOR_H
+#include "ModelCheckBaseMT.h"
+#include <atomic>
+#include <mutex>
+#include <thread>
+#include "misc/SafeDequeue.h"
+
+typedef pair<LDDState *, int> couple_th;
+//typedef stack<pair<LDDState *,int>> pile_t;
+class MCThReqPor : public ModelCheckBaseMT {
+public:
+ MCThReqPor(const NewNet &R,int nbThread);
+ ~MCThReqPor() override;
+ void buildSucc(LDDState *agregate) override;
+ static void *threadHandler(void *context);
+ void *Compute_successors();
+ void ComputeTh_Succ();
+ LDDState * getInitialMetaState() override;
+private:
+ void preConfigure() override;
+ SafeDequeue<couple_th> m_common_stack;
+ atomic<uint8_t> m_id_thread;
+ 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/MCMultiCore/ModelCheckerCPPThread.cpp b/src/MCMultiCore/ModelCheckerCPPThread.cpp
index bb0dfae40e3c431ae4f11f16822263b8b7083006..82dc224cc72d6d3f8f6792821c8ef8ed39bb9085 100644
--- a/src/MCMultiCore/ModelCheckerCPPThread.cpp
+++ b/src/MCMultiCore/ModelCheckerCPPThread.cpp
@@ -96,6 +96,7 @@ void ModelCheckerCPPThread::threadHandler(void *context) {
void ModelCheckerCPPThread::ComputeTh_Succ() {
m_id_thread = 0;
+
pthread_barrier_init(&m_barrier_builder, nullptr, m_nb_thread + 1);
m_finish = false;
for (int i = 0; i < m_nb_thread; i++) {