diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 75f543caf8688ac67a8a55cdc045f40a1066ef3e..9f3909bb640b559cf8234ec3e03059d4e15b6543 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -76,12 +76,15 @@ add_executable(mc-sog main.cpp
MCMultiCore/ModelCheckerCPPThread.cpp MCMultiCore/ModelCheckerCPPThread.h
MCMultiCore/ModelCheckerTh.cpp MCMultiCore/ModelCheckerTh.h
MCMultiCore/MCThReqPor.cpp MCMultiCore/MCThReqPor.h
+ MCMultiCore/MCCPPThPor.cpp MCMultiCore/MCCPPThPor.h
threadSOG.cpp threadSOG.h
HybridSOG.cpp HybridSOG.h
Hybrid/MCHybrid/MCHybridSOG.cpp Hybrid/MCHybrid/MCHybridSOG.h
MCMultiCore/ModelCheckThReq.cpp MCMultiCore/ModelCheckThReq.h
Hybrid/MCHybridReq/MCHybridSOGReq.cpp
Hybrid/MCHybridReq/MCHybridSOGReq.h
+ Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp
+ Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h
misc/md5_hash.h)
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index e0f1eebec390efa864c15a26ebb19277c9cbd7ad..950ed44199970b3d0a09dbb245e0992eef2daf17 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -43,7 +43,7 @@ MDD CommonSOG::get_successor(const MDD &From, const int &t) {
}
MDD CommonSOG::get_pred(const MDD &From, const int &t) {
- return SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(t)].getPlus(), m_tb_relation[t].getMinus());
+ return SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[t].getPlus(), m_tb_relation[t].getMinus());
}
MDD CommonSOG::ImageForward(const MDD& From) {
@@ -188,7 +188,9 @@ void CommonSOG::loadNetFromFile() {
m_transitionName = &m_net->transitionName;
m_placeName = &m_net->m_placePosName;
-
+ for (const auto& t : m_observable) {
+ m_transitions[t].mObservable=true;
+ }
cout << "Nombre de places : " << m_nbPlaces << endl;
cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
@@ -236,11 +238,19 @@ void CommonSOG::loadNetFromFile() {
}
delete[] prec;
delete[] postc;
+ for (auto elt : m_transitions){
+ cout<<"New transition"<<endl;
+ for (auto pre:elt.pre) {
+ cout<<pre.first<<" ";
+ }
+ cout<<"\n";
+ }
}
void CommonSOG::AddConflict2(const MDD &S, const int &transition, Set &le) {
auto haveCommonPre = [&](vector<pair<int, int>> &preT1, vector<pair<int, int>> &preT2) -> bool {
for (auto &elt1: preT1) {
for (auto &elt2: preT2) {
+ if (elt1.first<elt2.first) break;
if (elt1.first == elt2.first) return true;
}
}
@@ -248,25 +258,32 @@ void CommonSOG::AddConflict2(const MDD &S, const int &transition, Set &le) {
};
if (SylvanWrapper::lddmc_intersect(S, get_pred(get_successor(S,transition),transition))==S) {
for(auto i = 0; i < m_transitions.size(); ++i) {
- auto &preT1 = m_transitions[i].pre;
- auto &preT2 = m_transitions[transition].pre;
- if (haveCommonPre(preT1, preT2)) ample.insert(i);
+ if (i!=transition) {
+ auto &preT1 = m_transitions[i].pre;
+ auto &preT2 = m_transitions[transition].pre;
+ if (haveCommonPre(preT1, preT2)) ample.insert(i);
+ }
+
}
}
else {
- if (!SylvanWrapper::isFirable(S,transition)) {
+ if (!SylvanWrapper::SylvanWrapper::lddmc_firing_mono(S,m_tb_relation[transition].getMinus(),m_tb_relation[transition].getPlus())) {
for(auto i = 0; i < m_transitions.size(); ++i) {
- auto &preT = m_transitions[transition].pre;
- auto &postT1 = m_transitions[i].post;
- if (haveCommonPre(preT, postT1)) ample.insert(i);
+ if (i!=transition) {
+ auto &preT = m_transitions[transition].pre;
+ auto &postT1 = m_transitions[i].post;
+ if (haveCommonPre(preT, postT1)) ample.insert(i);
+ }
}
}
else {
for(auto i = 0; i < m_transitions.size(); ++i) {
- auto &preT = m_transitions[transition].pre;
- auto &postT1 = m_transitions[i].post;
- auto &preT1 = m_transitions[i].pre;
- if (haveCommonPre(preT, postT1) || haveCommonPre(preT,preT1)) ample.insert(i);
+ if (i!=transition) {
+ auto &preT = m_transitions[transition].pre;
+ auto &postT1 = m_transitions[i].post;
+ auto &preT1 = m_transitions[i].pre;
+ if (haveCommonPre(preT, postT1) || haveCommonPre(preT, preT1)) ample.insert(i);
+ }
}
}
}
@@ -275,12 +292,12 @@ void CommonSOG::AddConflict(const MDD &S, const int &transition, Set &le) {
auto haveCommonPre = [&](vector<pair<int, int>> &preT1, vector<pair<int, int>> &preT2) -> bool {
for (auto &elt1: preT1) {
for (auto &elt2: preT2) {
+ if (elt1.first<elt2.first) break;
if (elt1.first == elt2.first) return true;
}
}
return false;
};
- // cout<<"Transition to deal with : "<<transition<<endl;
if (SylvanWrapper::isFirable(S,m_tb_relation[transition].getMinus())) {
//cout<<"Checked\n";
for ( auto i = 0; i < m_transitions.size(); ++i) {
@@ -303,7 +320,6 @@ void CommonSOG::AddConflict(const MDD &S, const int &transition, Set &le) {
Set CommonSOG::computeAmple(const MDD &s) {
Set ample;
-
// Compute enabled transitions in s
for (auto index=0;index<m_tb_relation.size();++index) {
if (SylvanWrapper::isFirable(s,m_tb_relation[index].getMinus())) {
@@ -323,17 +339,16 @@ Set CommonSOG::computeAmple2(const MDD &S) {
MDD pre,img;
do {
- for (auto index=0;index<m_tb_relation.size();++index) {
- if (SylvanWrapper::isFirable(S,m_tb_relation[index].getMinus())) {
+ for (auto index=0;index<m_tb_relation.size();++index) {
+ if (SylvanWrapper::lddmc_firing_mono(S,m_tb_relation[index].getMinus(),m_tb_relation[index].getPlus())) {
ample.insert(index); break;
}
}
+
for (const auto& t: ample) {
AddConflict2(S, t, ample);
}
- //AddConflict2(S, *ample.begin(), ample);
-
- img=lddmc_true;
+ img=lddmc_false;
for (const auto& t : ample)
img=SylvanWrapper::lddmc_union_mono(img,SylvanWrapper::lddmc_firing_mono(S,m_tb_relation[t].getMinus(),m_tb_relation[t].getPlus()));
pre=lddmc_false;
@@ -351,32 +366,26 @@ MDD CommonSOG::saturatePOR(const MDD &s, Set& tObs,bool &div,bool &dead) {
set<MDD> myStack;
myStack.insert(s);
tObs.clear();
- MDD To=lddmc_false;
+ MDD To {lddmc_false};
do {
Reach1=Reach2;
-
- ample=computeAmple(From);
+ ample=computeAmple2(From);
if (ample.empty()) {
dead=true;
}
else {
for (const auto & t : ample) {
MDD succ=SylvanWrapper::lddmc_firing_mono(From,m_tb_relation[t].getMinus(),m_tb_relation[t].getPlus());
- if (succ!=lddmc_true && succ!=lddmc_false) {
+ if (succ!=lddmc_false) {
//cout<<"Transition of ample : "<<t<<endl;
if (m_transitions[t].mObservable) {
- //cout<<"Obs detected "<<t<<endl;
tObs.insert(t);
} else {
- //if (!SylvanWrapper::isFirable(From,m_tb_relation[t].getMinus())) exit(0);
-// //cout<<"From :"<<From<<"by transition "<<t<<" succ : "<<succ<<endl;
- //Compute div
- if (myStack.find(succ) != myStack.end()) {
+ if (myStack.find(succ) != myStack.end()) {
div = true;
- //cout<<"loop"<<endl;
for (uint16_t i = 0; i < m_tb_relation.size(); ++i) {
MDD newM=SylvanWrapper::lddmc_firing_mono(From,m_tb_relation[i].getMinus(),m_tb_relation[i].getPlus());
- if (newM!=lddmc_false && newM!=lddmc_true) {
+ if (newM!=lddmc_false) {
if (m_transitions[i].mObservable) {
tObs.insert(i);
} else {
diff --git a/src/Hybrid/MCHybrid/MCHybridSOG.cpp b/src/Hybrid/MCHybrid/MCHybridSOG.cpp
index 121d3645b27362345f27ab67ced29f5cf1e09622..524f02905e8e45eb402c724d15a8183f74da8898 100644
--- a/src/Hybrid/MCHybrid/MCHybridSOG.cpp
+++ b/src/Hybrid/MCHybrid/MCHybridSOG.cpp
@@ -385,7 +385,7 @@ void MCHybridSOG::computeDSOG(LDDGraph &g) {
m_nbsend = 0;
m_gc = 0;
- for (uint8_t i = 0; i < m_nb_thread - 1; i++) {
+ 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;
@@ -411,8 +411,8 @@ MDD MCHybridSOG::decodage_message(const char *chaine) {
//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++) {
+ 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++;
}
@@ -462,7 +462,7 @@ void MCHybridSOG::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++) {
+ for (auto it = marked_places.begin(); it != marked_places.end();++it) {
memcpy(mess_to_send + indice, &(*it), 2);
indice += 2;
}
diff --git a/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp b/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
index 7bbd91e84fc736288487fbef7334b8ba8e3e2229..1d5685103ba1130e3f1614948bed3172b86bb570 100644
--- a/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
+++ b/src/Hybrid/MCHybridReq/MCHybridSOGReq.cpp
@@ -22,7 +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;
diff --git a/src/Hybrid/MCHybridReq/MCHybridSOGReq.h b/src/Hybrid/MCHybridReq/MCHybridSOGReq.h
index c5c8bbaf08288d0de5701957360ab48eae0c127d..e4862fcc760229c43ca84d67b6feace76523d171 100644
--- a/src/Hybrid/MCHybridReq/MCHybridSOGReq.h
+++ b/src/Hybrid/MCHybridReq/MCHybridSOGReq.h
@@ -52,14 +52,13 @@ class MCHybridSOGReq : public CommonSOG
{
public:
MCHybridSOGReq(const NewNet &, MPI_Comm &, bool init = false);
- void buildFromNet(int index);
/// principal functions to construct the SOG
- void computeDSOG(LDDGraph &g);
+ void computeDSOG(LDDGraph &g) override;
~MCHybridSOGReq() override;
static void *threadHandler(void *context);
- void *doCompute();
+ virtual void *doCompute();
+
protected:
-private:
std::condition_variable m_condStack;
mutable std::mutex m_mutexCond;
MPI_Comm m_comm_world;
diff --git a/src/Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp b/src/Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..b17834993a34f5a3c624ab6b13db8365798e80c1
--- /dev/null
+++ b/src/Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp
@@ -0,0 +1,225 @@
+#include "MCHybridSOGReqPOR.h"
+//#define DEBUG_GC
+
+#include <cstdio>
+#include <openssl/md5.h>
+#include "misc/md5_hash.h"
+
+#define LENGTH_ID 16
+//#define LENGTH_MSG 180
+#define TAG_STATE 1
+#define TAG_FINISH 2
+#define TAG_INITIAL 3
+#define TAG_ASK_SUCC 4
+
+
+#define TAG_ACK_INITIAL 8
+#define TAG_ASK_STATE 9
+#define TAG_ACK_STATE 10
+#define TAG_ACK_SUCC 11
+
+//#define DEBUG_GC 1
+#define REDUCE 1
+using namespace std;
+
+MCHybridSOGReqPOR::MCHybridSOGReqPOR(const NewNet &R, MPI_Comm &comm_world, bool init):MCHybridSOGReq(R,comm_world,init) {
+
+}
+
+void *MCHybridSOGReqPOR::doCompute() {
+
+ int id_thread;
+ id_thread = m_id_thread++;
+ unsigned char Identif[20];
+ m_Terminated = false;
+ Set fireObs;
+ bool _div,_dead;
+ /****************************************** initial state ********************************************/
+ if (task_id == 0 && id_thread == 0) {
+ string *chaine = new string();
+ LDDState *c = new LDDState;
+ MDD Complete_meta_state=saturatePOR(m_initialMarking,fireObs,_div,_dead);
+ c->m_lddstate = Complete_meta_state;
+ SylvanWrapper::convert_wholemdd_stringcpp(Complete_meta_state, *chaine);
+ md5_hash::compute(*chaine, Identif);
+ auto destination = (uint16_t) (Identif[0] % n_tasks);
+ c->setProcess(destination);
+ if (destination == 0) {
+ m_nbmetastate++;
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
+ memcpy(c->m_SHA2, Identif, 16);
+ m_common_stack.push(Pair(couple(c, Complete_meta_state), fireObs));
+ m_condStack.notify_one();
+
+ } else {
+ MDD initialstate = Complete_meta_state;
+ m_graph->insertSHA(c);
+ memcpy(c->m_SHA2, Identif, 16);
+ //initialstate = Complete_meta_state;
+ SylvanWrapper::convert_wholemdd_stringcpp(initialstate, *chaine);
+ m_tosend_msg.push(MSG(chaine, destination));
+ }
+ }
+ /******************************* envoie et reception des aggregats ************************************/
+ string chaine;
+ if (id_thread == 0) {
+ do {
+ send_state_message();
+ read_message();
+ if (m_waitingBuildSucc == statereq::waitingBuild) {
+ bool res;
+ size_t pos = m_graph->findSHAPos(m_id_md5, res);
+ if (res) {
+ m_waitingBuildSucc = statereq::waitingSucc;
+ m_aggWaiting = m_graph->getLDDStateById(pos);
+ }
+ }
+ if (m_waitingBuildSucc == statereq::waitingSucc) {
+ if (m_aggWaiting->isCompletedSucc()) {
+ m_waitingBuildSucc = statereq::waitInitial;
+ sendSuccToMC();
+ }
+ }
+ if (m_waitingAgregate) {
+ bool res = false;
+ size_t pos = m_graph->findSHAPos(m_id_md5, res);
+ if (res) {
+ m_waitingAgregate = false;
+ sendPropToMC(pos);
+ }
+ }
+
+ } while (!m_Terminated);
+
+ }
+ /******************************* Construction des aggregats ************************************/
+
+ else {
+ while (!m_Terminated) {
+ {
+ std::unique_lock lk(m_mutexCond);
+ m_condStack.wait(lk,
+ [this] { return !m_common_stack.empty() || !m_received_msg.empty() || m_Terminated; });
+ }
+ /*if ( id_thread>1 ) {
+ if ( ++m_gc==1 ) {
+ m_gc_mutex.lock();
+ }
+ }*/
+ if (!m_Terminated) {
+ Pair e;
+ if (m_common_stack.try_pop(e)) {
+ while (!e.second.empty() && !m_Terminated) {
+ int t = *(e.second.begin());
+ e.second.erase(t);
+ MDD ldd_reachedclass=saturatePOR(get_successor(e.first.second, t),fireObs,_div,_dead);
+ string *message_to_send1 = new string();
+ SylvanWrapper::convert_wholemdd_stringcpp(ldd_reachedclass, *message_to_send1);
+ md5_hash::compute(*message_to_send1, Identif);
+ uint16_t destination = (uint16_t) (Identif[0] % n_tasks);
+ /**************** construction local ******/
+ if (destination == task_id) {
+ bool res = false;
+ LDDState *pos = m_graph->insertFindByMDD(ldd_reachedclass, res);
+ if (!res) {
+ pos->setProcess(task_id);
+ pos->setDiv(Set_Div(ldd_reachedclass));
+ pos->setDeadLock(_dead);
+ memcpy(pos->m_SHA2, Identif, 16);
+ m_common_stack.push(Pair(couple(pos, pos->m_lddstate), fireObs));
+ m_condStack.notify_one();
+ }
+ m_graph->addArc();
+ {
+ std::scoped_lock<std::mutex> guard(m_graph_mutex);
+ e.first.first->Successors.insert(e.first.first->Successors.begin(),
+ LDDEdge(pos, t));
+ pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
+ }
+ }
+ /**************** construction externe ******/
+ else { // send to another process
+ LDDState *reached_class = new LDDState;
+ reached_class->m_lddstate = ldd_reachedclass;
+ reached_class->setProcess(destination);
+ LDDState *posV = m_graph->insertFindSha(Identif, reached_class);
+ if (!posV) {
+ MDD reached{ldd_reachedclass};
+ string *message_to_send2 = new string();
+ SylvanWrapper::convert_wholemdd_stringcpp(reached, *message_to_send2);
+ m_graph->addArc();
+ m_graph_mutex.lock();
+ e.first.first->Successors.insert(e.first.first->Successors.begin(),
+ LDDEdge(reached_class, t));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(),
+ LDDEdge(e.first.first, t));
+ m_graph_mutex.unlock();
+ m_tosend_msg.push(MSG(message_to_send2, destination));
+
+ } else {
+ //cout<<"sha found "<<endl;
+ m_graph->addArc();
+ {
+ std::scoped_lock<std::mutex> guard(m_graph_mutex);
+ e.first.first->Successors.insert(e.first.first->Successors.begin(),
+ LDDEdge(posV, t));
+ posV->Predecessors.insert(posV->Predecessors.begin(), LDDEdge(e.first.first, t));
+ }
+ delete reached_class;
+ }
+ }
+ }
+ e.first.first->setCompletedSucc();
+ }
+
+ /******************************* Construction des aggregats � partir de pile de messages ************************************/
+ MSG popped_msg;
+ if (m_received_msg.try_pop(popped_msg)) {
+ MDD receivedLDD = decodage_message(popped_msg.first->c_str());
+ delete popped_msg.first;
+ MDD MState =saturatePOR(receivedLDD,fireObs,_div,_dead);
+ bool res = false;
+ LDDState *Agregate = m_graph->insertFindByMDD(MState, res);
+ if (!res) {
+ Agregate->setDiv(Set_Div(MState));
+ Agregate->setDeadLock(_dead);
+ Agregate->setProcess(task_id);
+ SylvanWrapper::convert_wholemdd_stringcpp(MState, chaine);
+ md5_hash::compute(chaine, Identif);
+ memcpy(Agregate->m_SHA2, Identif, 16);
+ m_common_stack.push(Pair(couple(Agregate, MState), fireObs));
+ m_condStack.notify_one();
+ }
+ }
+
+ /* if ( id_thread>1 ) {
+ if ( --m_gc==0 ) {
+ m_gc_mutex.unlock();
+ }
+
+ }*/
+ // }
+
+ }
+ } /// End else
+
+ // cout<<"Working process "<<task_id<<" leaved...thread "<<id_thread<<endl;
+
+ }
+
+ // cout<<"Finnnnnn...."<<endl;
+}
+
+
+
+
+
+
+
+
+
+
+MCHybridSOGReqPOR::~MCHybridSOGReqPOR() = default;
+
+
diff --git a/src/Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h b/src/Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h
new file mode 100644
index 0000000000000000000000000000000000000000..ddcce78a2aa104882b3b3320f1fc71f079f759fa
--- /dev/null
+++ b/src/Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h
@@ -0,0 +1,55 @@
+#ifndef MCHybridSOGReqPOR_H
+#define MCHybridSOGReqPOR_H
+
+#include <stack>
+#include <vector>
+#include "NewNet.h"
+#include <pthread.h>
+#include <cstdio>
+#include <sys/types.h>
+#include <unistd.h>
+#include "LDDGraph.h"
+#include "TransSylvan.h"
+
+#include <mpi.h>
+#include <misc/sha2.h>
+
+#include <sys/ipc.h>
+#include <sys/shm.h>
+#include <sys/types.h>
+#include <cstdlib>
+#include <sstream>
+
+#include <iostream>
+#include <queue>
+#include <string>
+#include <ctime>
+#include <chrono>
+#include "CommonSOG.h"
+#include <atomic>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+#include "misc/SafeDequeue.h"
+#include "../MCHybridReq/MCHybridSOGReq.h"
+// namespace mpi = boost::mpi;
+//#define MASTER 0
+//#define large 128
+extern unsigned int nb_th;
+extern int n_tasks, task_id;
+
+
+
+typedef pair<string *, unsigned int> MSG;
+
+typedef stack<MSG> pile_msg;
+
+class MCHybridSOGReqPOR : public MCHybridSOGReq
+{
+public:
+ MCHybridSOGReqPOR(const NewNet &, MPI_Comm &, bool init = false);
+ ~MCHybridSOGReqPOR() override;
+ void *doCompute() override;
+};
+
+#endif // MCHybridSOGReqPOR_H
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index f4267e68f4928936d82f9182373012fca800a1e7..8a3964b7eac9e802df51e6935851cd1704cc0018 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -133,11 +133,11 @@ void LDDGraph::printCompleteInformation() {
void LDDGraph::InitVisit(LDDState *S, size_t nb) {
if (nb <= m_nbStates) {
- for (LDDEdges::const_iterator i = S->Successors.begin(); !(i == S->Successors.end()); i++) {
+ for (const auto & i : S->Successors) {
- if ((*i).first->isVisited() == true) {
+ if (i.first->isVisited() == true) {
nb++;
- InitVisit((*i).first, nb);
+ InitVisit(i.first, nb);
}
}
@@ -152,10 +152,10 @@ void LDDGraph::printGraph(LDDState *s, size_t &nb) {
s->setVisited();
LDDEdges::const_iterator i;
- for (i = s->Successors.begin(); !(i == s->Successors.end()); i++) {
- if ((*i).first->isVisited() == false) {
+ for (const auto & i: s->Successors) {
+ if (i.first->isVisited() == false) {
nb++;
- printGraph((*i).first, nb);
+ printGraph(i.first, nb);
}
}
@@ -165,12 +165,19 @@ void LDDGraph::printGraph(LDDState *s, size_t &nb) {
/*** Giving a position in m_GONodes Returns an LDDState ****/
-LDDState *LDDGraph::getLDDStateById(unsigned int id) {
+LDDState *LDDGraph::getLDDStateById(const unsigned int& id) {
return m_GONodes.at(id);
}
string_view LDDGraph::getTransition(uint16_t pos) {
+ /*for (const auto & it : m_transition) {
+ if (it.second == pos) {
+ return it.first;
+ }
+ }
+ return it.first;*/
+
map<string, uint16_t>::iterator it = m_transition->begin();
while (it != m_transition->end()) {
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index 58546561806f41338d8cca03f811bbc67070aea4..3fd9c12ae637fcedd019cea46d42ec408c641fa8 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -28,7 +28,7 @@ class LDDGraph
void setPlace(map<uint16_t,string>& list_places);
void setTransition(map<string,uint16_t>& list_transitions);
MetaLDDNodes m_GONodes;
- LDDState *getLDDStateById(unsigned int id);
+ LDDState *getLDDStateById(const unsigned int& id);
LDDState *m_initialstate=nullptr;
uint64_t m_nbStates;
uint64_t m_nbMarking;
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index b92653a9f4a45ea3f00fc5abce013970832fa99a..5ea514e90eefb1e508f669c8e4d3e341b51c1eda 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -5,7 +5,7 @@
LDDState::~LDDState()=default;
-void LDDState::setLDDValue(MDD m) {
+void LDDState::setLDDValue(const MDD & m) {
m_lddstate=m;
}
MDD LDDState::getLDDValue() {
diff --git a/src/LDDState.h b/src/LDDState.h
index d9c448099af63c05e938ebd0538800c51dd82854..cabe5fa0b6298d449b1b374ca4856b24016f1931 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -22,7 +22,7 @@ class LDDState {
vector<pair<LDDState*, int>>* getSuccessors();
vector<pair<LDDState*, int> > Predecessors, Successors;
- void setLDDValue(MDD m);
+ void setLDDValue(const MDD& m);
MDD getLDDValue();
MDD m_lddstate=0;
unsigned char m_SHA2[81];
@@ -31,9 +31,9 @@ class LDDState {
bool m_blocage=false;
bool isVirtual() {return m_virtual;}
void setVirtual(){m_virtual=true;}
- void setDiv(bool di) {m_boucle=di;}
+ void setDiv(const bool& di) {m_boucle=di;}
inline bool isDiv() {return m_boucle;}
- void setDeadLock(bool de) {m_blocage=de;}
+ void setDeadLock(const bool& de) {m_blocage=de;}
bool isDeadLock() {return m_blocage;}
inline void setVisited() {m_visited=true;}
[[nodiscard]] inline bool isVisited() const {return m_visited;}
@@ -41,7 +41,7 @@ class LDDState {
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;}
+ void setProcess(const uint16_t& v) {m_process=v;}
[[nodiscard]] uint16_t getProcess() const {return m_process;}
inline void decNbSuccessors() {m_nbSuccessorsToBeProcessed--;}
protected:
diff --git a/src/MCMultiCore/MCCPPThPor.cpp b/src/MCMultiCore/MCCPPThPor.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..954f66bce72cd44b70d60ea278f9322917091f8f
--- /dev/null
+++ b/src/MCMultiCore/MCCPPThPor.cpp
@@ -0,0 +1,108 @@
+#include "MCCPPThPor.h"
+//#include "sylvan.h"
+//#include <sylvan_int.h>
+#include <functional>
+#include <iostream>
+
+
+#include "SylvanWrapper.h"
+
+#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
+
+using namespace std;
+
+MCCPPThPor::MCCPPThPor(const NewNet &R, int nbThread) :
+ ModelCheckBaseMT(R, nbThread) {
+}
+
+
+void MCCPPThPor::preConfigure() {
+ initializeLDD();
+ loadNetFromFile();
+ ComputeTh_Succ();
+}
+
+/*
+ * Compute SOG with POR reduction
+ */
+void MCCPPThPor::Compute_successors() {
+ uint16_t id_thread;
+ id_thread=m_id_thread++;
+ Set fireObs;
+ bool _div,_dead;
+ if (id_thread == 0) {
+ auto *initialNode = new LDDState;
+ initialNode->m_lddstate=saturatePOR(m_initialMarking,fireObs,_div,_dead);
+ //initialNode->setDiv(_div);
+ initialNode->setDiv(Set_Div(initialNode->m_lddstate));
+ initialNode->setDeadLock(_dead);
+ m_graph->setInitialState(initialNode);
+ m_graph->insert(initialNode);
+ m_common_stack.push(Pair(couple(initialNode, initialNode->m_lddstate), fireObs));
+ m_condStack.notify_one();
+ m_finish_initial = true;
+ }
+
+ Pair e;
+ do {
+ std::unique_lock<std::mutex> lk(m_mutexStack);
+ m_condStack.wait(lk, std::bind(&MCCPPThPor::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 reducedMS = saturatePOR(get_successor(e.first.second, t),fireObs,_div,_dead);
+ SylvanWrapper::lddmc_refs_push(reducedMS);
+ bool res;
+ LDDState *pos = m_graph->insertFindByMDD(reducedMS, res);
+ m_graph->addArc();
+ if (!res) {
+ pos->setDeadLock(_dead);
+ //pos->setDiv(Set_Div(pos->m_lddstate));
+ pos->setDiv(_div);
+ m_common_stack.push(Pair(couple(pos, reducedMS), fireObs));
+ 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 MCCPPThPor::threadHandler(void *context) {
+ SylvanWrapper::lddmc_refs_init();
+ ((MCCPPThPor *) context)->Compute_successors();
+}
+
+void MCCPPThPor::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++) {
+ m_list_thread[i] = new thread(threadHandler, this);
+ if (m_list_thread[i] == nullptr) {
+ cout << "error: pthread creation failed. " << endl;
+ }
+ }
+}
+
+MCCPPThPor::~MCCPPThPor() {
+ m_finish = true;
+ m_condStack.notify_all();
+ for (int i = 0; i < m_nb_thread; i++) {
+ m_list_thread[i]->join();
+ delete m_list_thread[i];
+ }
+}
+
+bool MCCPPThPor::hasToProcess() const {
+ return m_finish || !m_common_stack.empty();
+}
diff --git a/src/MCMultiCore/MCCPPThPor.h b/src/MCMultiCore/MCCPPThPor.h
new file mode 100644
index 0000000000000000000000000000000000000000..89b9830ba01dd7b41d9045c484ddceb25a7358e8
--- /dev/null
+++ b/src/MCMultiCore/MCCPPThPor.h
@@ -0,0 +1,34 @@
+#ifndef MCCPPThPor_H
+#define MCCPPThPor_H
+#include "ModelCheckBaseMT.h"
+#include "misc/stacksafe.h"
+#include "misc/SafeDequeue.h"
+#include <atomic>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+typedef pair<LDDState *, int> couple_th;
+
+/*
+ * Multi-threading with C++14 Library
+ */
+class MCCPPThPor : public ModelCheckBaseMT
+{
+public:
+ MCCPPThPor(const NewNet &R,int nbThread);
+ ~MCCPPThPor();
+ static void threadHandler(void *context);
+ void Compute_successors();
+ void ComputeTh_Succ();
+private:
+ void preConfigure();
+ bool hasToProcess() const;
+
+ SafeDequeue<Pair> m_common_stack;
+ atomic<uint8_t> m_id_thread;
+ pthread_barrier_t m_barrier_builder;
+ std::condition_variable m_condStack;
+ std::mutex m_mutexStack;
+ thread* m_list_thread[128];
+};
+#endif
diff --git a/src/MCMultiCore/MCThReqPor.cpp b/src/MCMultiCore/MCThReqPor.cpp
index 62d34c40cd4e12d5bc6f2516ada32eda0f4c3309..bd2d1d31932049aa27ed87587dfd7cc3acd505f3 100644
--- a/src/MCMultiCore/MCThReqPor.cpp
+++ b/src/MCMultiCore/MCThReqPor.cpp
@@ -21,7 +21,7 @@ void MCThReqPor::ComputeTh_Succ() {
m_id_thread = 0;
//cout<<"Enter : "<<__func__ <<endl;
pthread_barrier_init(&m_barrier_threads, nullptr, m_nb_thread + 1);
- for (int i = 0; i < m_nb_thread; i++) {
+ 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;
@@ -71,7 +71,7 @@ void MCThReqPor::buildSucc(LDDState *agregate) {
if (!agregate->isVisited()) {
agregate->setVisited();
if (agregate->getMCurrentLevel() == 0) {
- Set fire = firable_obs(agregate->m_lddstate);
+ Set fire = firable_obs(agregate->m_lddstate);///////////////////////////////////////////////////
agregate->setMCurrentLevel(LEVEL);
agregate->m_nbSuccessorsToBeProcessed = fire.size();
if (!fire.empty()) {
diff --git a/src/MCMultiCore/ModelCheckerCPPThread.cpp b/src/MCMultiCore/ModelCheckerCPPThread.cpp
index 58d4addbf22916de4610f61751aca93539abdcc1..bffe8d5ead5d45aba5db91fd9e7d4f7c2e364eb3 100644
--- a/src/MCMultiCore/ModelCheckerCPPThread.cpp
+++ b/src/MCMultiCore/ModelCheckerCPPThread.cpp
@@ -28,58 +28,6 @@ void ModelCheckerCPPThread::preConfigure() {
ComputeTh_Succ();
}
-/*
- * Compute SOG with POR reduction
- */
-void ModelCheckerCPPThread::ComputeSuccessorsPOR() {
- uint16_t id_thread;
- id_thread=m_id_thread++;
- Set fireObs;
- bool _div,_dead;
- if (id_thread == 0) {
- auto *initialNode = new LDDState;
- initialNode->m_lddstate=saturatePOR(m_initialMarking,fireObs,_div,_dead);
- initialNode->setDiv(_div);
- initialNode->setDeadLock(_dead);
- m_graph->setInitialState(initialNode);
- m_graph->insert(initialNode);
- m_common_stack.push(Pair(couple(initialNode, initialNode->m_lddstate), fireObs));
- m_condStack.notify_one();
- m_finish_initial = true;
- }
-
- Pair e;
- 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 reducedMS = saturatePOR(get_successor(e.first.second, t),fireObs,_div,_dead);
- SylvanWrapper::lddmc_refs_push(reducedMS);
- bool res;
- LDDState *pos = m_graph->insertFindByMDD(reducedMS, res);
- m_graph->addArc();
- if (!res) {
-
- pos->setDeadLock(_dead);
- pos->setDiv(_div);
- m_common_stack.push(Pair(couple(pos, reducedMS), fireObs));
- 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);
-}
/*
* Compute SOG without reduction
*/
diff --git a/src/MCMultiCore/ModelCheckerCPPThread.h b/src/MCMultiCore/ModelCheckerCPPThread.h
index c69bd88fa12e27b67c736577e926aadf84ca01df..c3ddbf0540c58873e6048168d15464a613fd4e08 100644
--- a/src/MCMultiCore/ModelCheckerCPPThread.h
+++ b/src/MCMultiCore/ModelCheckerCPPThread.h
@@ -19,7 +19,6 @@ public:
~ModelCheckerCPPThread();
static void threadHandler(void *context);
void Compute_successors();
- void ComputeSuccessorsPOR();
void ComputeTh_Succ();
private:
void preConfigure();
@@ -27,7 +26,7 @@ private:
SafeDequeue<Pair> m_common_stack;
atomic<uint8_t> m_id_thread;
- std::mutex m_mutex;
+ //std::mutex m_mutex;
pthread_barrier_t m_barrier_builder;
std::condition_variable m_condStack;
std::mutex m_mutexStack;
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index 7391a23938268f0bbbc980baff00133c7b90f650..f2481bd9ae224d9f3974c1fb57ba115b8834f5d4 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -27,11 +27,11 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder)
SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
- for (auto it=l_transap.begin();it!=l_transap.end();it++) {
- register_ap(*it);
+ for (const auto& it:l_transap) {
+ register_ap(it);
}
- for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
- register_ap(*it);
+ for (const auto & it: l_placeap)
+ register_ap(it);
}
@@ -53,32 +53,14 @@ std::string SogKripkeTh::format_state(const spot::state* s) const
}
SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
-
auto ss = static_cast<const SogKripkeStateTh*>(s);
LDDState *aggregate=ss->getLDDState();
bdd cond = state_condition(ss);
- /*if (iter_cache_)
- {
- auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
- it->recycle(aggregate, cond);
- iter_cache_ = nullptr; // empty the cache
- return it;
- }*/
-
- return new SogKripkeIteratorTh(aggregate,cond);
-
-
-
-
-/* auto ss = static_cast<const SogKripkeStateTh*>(s);
- //////////////////////////////////////////////
-
- return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));*/
+ return new SogKripkeIteratorTh(aggregate,cond);
}
bdd SogKripkeTh::state_condition(const spot::state* s) const
{
-
auto ss = static_cast<const SogKripkeStateTh*>(s);
vector<uint16_t> marked_place = ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
#ifdef TESTENABLE
@@ -88,21 +70,20 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
#endif
bdd result=bddtrue;
// Marked places
- for (auto it=marked_place.begin();it!=marked_place.end();it++) {
- string name=string(m_builder->getPlace(*it));
+ for (const auto& it:marked_place) {
+ string name=string(m_builder->getPlace(it));
spot::formula f=spot::formula::ap(name);
result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
vector<uint16_t> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_builder->getPlaceProposition());
- for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
- string name=string(m_builder->getPlace(*it));
+ for (const auto& it: unmarked_place) {
+ string name=string(m_builder->getPlace(it));
spot::formula f=spot::formula::ap(name);
result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
return result;
}
-
SogKripkeTh::~SogKripkeTh()
{
//dtor
diff --git a/src/SpotSogIterator.cpp b/src/SpotSogIterator.cpp
index ae61c6374b317de2060b94026dcbfdeb644b8d7f..240ccf719566697b72c2c07d4a09345429200aa0 100644
--- a/src/SpotSogIterator.cpp
+++ b/src/SpotSogIterator.cpp
@@ -9,7 +9,7 @@ SpotSogIterator::SpotSogIterator(const LDDState* lddstate):m_lddstate(lddstate)
//vector<pair<LDDState*, int>>
m_lddstate->setDiv(true);
- for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
+ for (int i=0;i<m_lddstate->getSuccessors()->size();++i) {
m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
}
/* if (lddstate->isDeadLock()) {
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 569932e49d1805890626938908cd87ce6dd951c9..5c64e27ebb93aa82b4169c60c2218d009f924c7f 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -478,7 +478,7 @@ SylvanWrapper::llmsset_lookup2(const llmsset2_t dbs, uint64_t a, uint64_t b, int
}
}
-uint64_t SylvanWrapper::llmsset_lookup(const llmsset2_t dbs, const uint64_t a, const uint64_t b, int *created) {
+uint64_t SylvanWrapper::llmsset_lookup(const llmsset2_t& dbs, const uint64_t& a, const uint64_t& b, int *created) {
return llmsset_lookup2(dbs, a, b, created, 0);
}
@@ -603,7 +603,7 @@ size_t SylvanWrapper::lddmc_nodecount_mark(MDD mdd) {
return 1 + lddmc_nodecount_mark(mddnode_getdown(n)) + lddmc_nodecount_mark(mddnode_getright(n));
}
-MDD SylvanWrapper::lddmc_union_mono(MDD a, MDD b) {
+MDD SylvanWrapper::lddmc_union_mono(MDD a,MDD b) {
/* Terminal cases */
if (a == b) return a;
if (a == lddmc_false) return b;
@@ -834,10 +834,10 @@ bool SylvanWrapper::isFirable(MDD cmark, MDD minus) {
return result;
}
-MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, const MDD minus, const 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;
+ if (minus == lddmc_false || plus == lddmc_false || cmark==lddmc_false) return lddmc_false;
MDD result;
MDD _cmark = cmark, _minus = minus, _plus = plus;
@@ -1192,7 +1192,7 @@ int SylvanWrapper::llmsset_mark(const llmsset2_t dbs, uint64_t index) {
* Intersection
*/
-MDD SylvanWrapper::lddmc_intersect(MDD a, MDD b) {
+MDD SylvanWrapper::lddmc_intersect(MDD a,MDD b) {
/* Terminal cases */
if (a == b) return a;
if (a == lddmc_false || b == lddmc_false) return lddmc_false;
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
index a1ad54c4e0bc27a6af0d3fcf53150183eba212d3..e3afa4905bf7dbacc9a904aea8430c402dc8a23b 100644
--- a/src/SylvanWrapper.h
+++ b/src/SylvanWrapper.h
@@ -173,7 +173,7 @@ public:
static size_t lddmc_nodecount(MDD mdd);
- static MDD lddmc_union_mono(MDD a, MDD b);
+ static MDD lddmc_union_mono(MDD a,MDD b);
static MDD lddmc_intersect(MDD a, MDD b);
static bool isSingleMDD(MDD mdd);
@@ -185,7 +185,7 @@ public:
static MDD ldd_minus(MDD a, MDD b);
- static MDD lddmc_firing_mono(MDD cmark, const MDD minus, const MDD plus);
+ static MDD lddmc_firing_mono(MDD cmark, const MDD& minus, const MDD& plus);
static size_t lddmc_nodecount_mark(MDD mdd);
@@ -227,7 +227,7 @@ public:
static inline uint64_t
llmsset_lookup2(const llmsset2_t dbs, uint64_t a, uint64_t b, int *created, const int custom);
- static uint64_t llmsset_lookup(const llmsset2_t dbs, const uint64_t a, const uint64_t b, int *created);
+ static uint64_t llmsset_lookup(const llmsset2_t& dbs, const uint64_t& a, const uint64_t& b, int *created);
static uint64_t llmsset_hash(const uint64_t a, const uint64_t b, const uint64_t seed);
diff --git a/src/main.cpp b/src/main.cpp
index ff38313d3c08a42525625cdfee60b3f4c37a25af..d5f27f042d76bbde3ab66fee25327428decd39c1 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -10,6 +10,7 @@
#include "MCMultiCore/ModelCheckerCPPThread.h"
#include "MCMultiCore/ModelCheckerTh.h"
#include "MCMultiCore/ModelCheckThReq.h"
+#include "MCMultiCore/MCCPPThPor.h"
#include "threadSOG.h"
#include "HybridSOG.h"
#include "Hybrid/MCHybrid/MCHybridSOG.h"
@@ -120,14 +121,16 @@ int main(int argc, char **argv) {
if (n_tasks == 1) {
- if (n_tasks == 1 && (!strcmp(argv[1], "otfPR") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP"))) {
+ if (n_tasks == 1 && (!strcmp(argv[1], "otfPR") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP") || !strcmp(argv[1], "otfPOR"))) {
cout << "Performing on the fly Model checking..." << endl;
if (!strcmp(argv[1], "otfP"))
cout << "Multi-threaded algorithm based on Pthread library!" << endl;
else if (!strcmp(argv[1], "otfPR"))
cout << "Multi-threaded algorithm (progressive) based on PThread!" << endl;
- else
+ else if (!strcmp(argv[1], "otfC"))
cout << "Multi-threaded algorithm based on C++ Thread library!" << endl;
+ else
+ cout<<"Multi-threaded algorithm (progressive) with POR!"<<endl;
cout << "Building automata for not(formula)\n";
auto d = spot::make_bdd_dict();
spot::translator obj=spot::translator(d);
@@ -140,8 +143,9 @@ int main(int argc, char **argv) {
mcl = new ModelCheckerTh(Rnewnet, nb_th);
else if (!strcmp(argv[1], "otfC"))
mcl = new ModelCheckerCPPThread(Rnewnet, nb_th);
- else
+ else if (!strcmp(argv[1], "otfPR"))
mcl=new ModelCheckThReq(Rnewnet, nb_th);
+ else mcl=new MCCPPThPor(Rnewnet, nb_th);
mcl->loadNet();
auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
cout << "Performing on the fly Modelchecking" << endl;
@@ -324,6 +328,5 @@ int main(int argc, char **argv) {
}
}
MPI_Finalize();
-
return (EXIT_SUCCESS);
}