diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 75a2c9af521f0910e16464243c6ce23b7c968cf4..e0f1eebec390efa864c15a26ebb19277c9cbd7ad 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -1,6 +1,7 @@
#include <string>
#include "SylvanWrapper.h"
#include "CommonSOG.h"
+#include <cassert>
CommonSOG::CommonSOG() = default;
@@ -41,6 +42,10 @@ 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());
}
+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());
+}
+
MDD CommonSOG::ImageForward(const MDD& From) {
MDD Res = lddmc_false;
for (auto i: m_nonObservable) {
@@ -232,13 +237,45 @@ void CommonSOG::loadNetFromFile() {
delete[] prec;
delete[] postc;
}
-
+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) return true;
+ }
+ }
+ return false;
+ };
+ 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);
+ }
+ }
+ else {
+ if (!SylvanWrapper::isFirable(S,transition)) {
+ 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);
+ }
+ }
+ 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);
+ }
+ }
+ }
+}
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) {
- // cout<<" Get0Elt1 : "<<std::get<0>(elt1)<<", Get0Elt2 : "<<std::get<0>(elt2)<<endl;
- if (std::get<0>(elt1) == std::get<0>(elt2)) return true;
+ if (elt1.first == elt2.first) return true;
}
}
return false;
@@ -256,9 +293,9 @@ void CommonSOG::AddConflict(const MDD &S, const int &transition, Set &le) {
} else {
for (auto i = 0; i < m_transitions.size(); ++i) {
if (i != transition) {
+ auto &preT = m_transitions[transition].pre;
auto &postT1 = m_transitions[i].post;
- auto &preT2 = m_transitions[transition].pre;
- if (haveCommonPre(postT1, preT2)) ample.insert(i);
+ if (haveCommonPre(preT, postT1)) ample.insert(i);
}
}
}
@@ -266,23 +303,44 @@ void CommonSOG::AddConflict(const MDD &S, const int &transition, Set &le) {
Set CommonSOG::computeAmple(const MDD &s) {
Set ample;
- Set enabledT;
+
// Compute enabled transitions in s
- for (auto index=0;index<m_tb_relation.size();index++) {
- if (SylvanWrapper::isFirable(s,m_tb_relation[index].getMinus()))
- enabledT.insert(index);
- }
- // cout<<"Size of enabledT : "<<enabledT.size()<<endl;
- if (!enabledT.empty()) {
- auto it=enabledT.begin();
- ample.insert(*it);
- enabledT.erase(it);
+ for (auto index=0;index<m_tb_relation.size();++index) {
+ if (SylvanWrapper::isFirable(s,m_tb_relation[index].getMinus())) {
+ ample.insert(index); break;
+ }
}
- for (const auto &t : ample) {
- //for (int i=0;i<m_transitions.size();++i) {
- AddConflict(s,t,ample);
+
+ for (const auto& t: ample) {
+ AddConflict(s, t, ample);
}
- //cout<<"Size of ample : "<<ample.size()<<endl;
+
+ return ample;
+}
+
+Set CommonSOG::computeAmple2(const MDD &S) {
+ Set ample;
+ MDD pre,img;
+ do {
+
+ for (auto index=0;index<m_tb_relation.size();++index) {
+ if (SylvanWrapper::isFirable(S,m_tb_relation[index].getMinus())) {
+ ample.insert(index); break;
+ }
+ }
+ for (const auto& t: ample) {
+ AddConflict2(S, t, ample);
+ }
+ //AddConflict2(S, *ample.begin(), ample);
+
+ img=lddmc_true;
+ 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;
+ for (const auto& t : ample)
+ pre=SylvanWrapper::lddmc_union_mono(pre,SylvanWrapper::lddmc_firing_mono(img,m_tb_relation[t].getPlus(),m_tb_relation[t].getMinus()));
+
+ } while (SylvanWrapper::lddmc_intersect(S, pre)!=S);
return ample;
}
@@ -292,44 +350,52 @@ MDD CommonSOG::saturatePOR(const MDD &s, Set& tObs,bool &div,bool &dead) {
Set ample;
set<MDD> myStack;
myStack.insert(s);
- tObs.erase(tObs.begin(),tObs.end());
- MDD To=lddmc_true;
+ tObs.clear();
+ MDD To=lddmc_false;
do {
Reach1=Reach2;
+
ample=computeAmple(From);
- if (ample.empty()) dead=true;
+ if (ample.empty()) {
+ dead=true;
+ }
else {
for (const auto & t : ample) {
- MDD succ= get_successor(From,t);
- if (m_transitions[t].mObservable) {
- tObs.insert(t);
- }
- else {
- //Compute div
- if (myStack.find(succ)!=myStack.end()) {
- div=true;
- for (uint16_t i=0;i<m_transitions.size();++i) {
- if (SylvanWrapper::isFirable(From,m_tb_relation[i].getMinus())) {
- if (m_transitions[i].mObservable) tObs.insert(t);
- else {
- MDD newM= get_successor(From,i);
- To=SylvanWrapper::lddmc_union_mono(To,newM);
- myStack.insert(newM);
+ MDD succ=SylvanWrapper::lddmc_firing_mono(From,m_tb_relation[t].getMinus(),m_tb_relation[t].getPlus());
+ if (succ!=lddmc_true && 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()) {
+ 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 (m_transitions[i].mObservable) {
+ tObs.insert(i);
+ } else {
+ To = SylvanWrapper::lddmc_union_mono(To, newM);
+ myStack.insert(newM);
+ }
}
}
+ } else {
+ To = SylvanWrapper::lddmc_union_mono(To, succ);
+ myStack.insert(succ);
}
}
- else {
- To=SylvanWrapper::lddmc_union_mono(To,succ);
- myStack.insert(succ);
- }
-
}
- }
+ } //end for
}
From=To;
Reach2=SylvanWrapper::lddmc_union_mono(Reach2,To);
+ To=lddmc_false;
} while (Reach1!=Reach2);
- // cout<<"Size of obs : "<<tObs.size()<<endl;
- return Reach1;
+ return Reach2;
}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 9ef020548c51729efb61d099f31b303be1dcb4b5..e1eb45bee4a0dfd3c115b99dfce56e2207675a6f 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -59,6 +59,7 @@ protected:
Set firable_obs(const MDD& State);
MDD get_successor(const MDD &From, const int &t);
+ MDD get_pred(const MDD &From, const int &t);
MDD ImageForward(const MDD& From);
@@ -81,11 +82,16 @@ private:
* Compute ample set @ample for state @s
*/
Set computeAmple(const MDD &s);
+ Set computeAmple2(const MDD &s);
/*
* Determine ample set in S for transition
*/
void AddConflict(const MDD &S, const int &transition, Set &le);
+ /*
+ * New version
+ */
+ void AddConflict2(const MDD &S, const int &transition, Set &le);
};
diff --git a/src/MCMultiCore/MCThReqPor.cpp b/src/MCMultiCore/MCThReqPor.cpp
index 719c200edbdfa2d49c96f34e32240d693377531b..62d34c40cd4e12d5bc6f2516ada32eda0f4c3309 100644
--- a/src/MCMultiCore/MCThReqPor.cpp
+++ b/src/MCMultiCore/MCThReqPor.cpp
@@ -1,5 +1,4 @@
#include "MCThReqPor.h"
-#include <unistd.h>
#include <thread>
#define LEVEL 3
@@ -21,11 +20,11 @@ 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;
+ pthread_barrier_init(&m_barrier_threads, nullptr, 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;
}
}
@@ -40,23 +39,24 @@ LDDState *MCThReqPor::getInitialMetaState() {
return m_graph->getInitialAggregate();
}
ComputeTh_Succ();
- LDDState *c = new LDDState;
- MDD initial_meta_state = Accessible_epsilon(m_initialMarking);
+ auto *c = new LDDState;
+ Set fireObs;
+ bool _dead, _div;
+ MDD initial_meta_state = saturatePOR(m_initialMarking, fireObs, _div, _dead);
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()) {
+ c->m_nbSuccessorsToBeProcessed = fireObs.size();
+ c->setMCurrentLevel(LEVEL);
- for (auto it = fire.begin(); it != fire.end(); it++)
- m_common_stack.push(couple_th(c, *it));
+ c->setDiv(_div);
+ c->setDeadLock(_dead);
+ if (!fireObs.empty()) {
+ for (const auto &it: fireObs)
+ 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();
@@ -76,8 +76,8 @@ void MCThReqPor::buildSucc(LDDState *agregate) {
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));
+ for (const auto &elt: fire)
+ m_common_stack.push(couple_th(agregate, elt));
std::unique_lock<std::mutex> lk(m_mutexBuildCompleted);
m_datacondBuildCompleted.wait(lk, [agregate] { return agregate->isCompletedSucc(); });
lk.unlock();
@@ -100,12 +100,15 @@ void *MCThReqPor::threadHandler(void *context) {
void *MCThReqPor::Compute_successors() {
couple_th elt;
LDDState *pos, *aggregate;
+ Set fireObs;
+ bool _div, _dead;
do {
while (!m_finish && m_common_stack.try_pop(elt)) {
aggregate = elt.first;
- int transition = elt.second;
+ int &transition = elt.second;
MDD meta_state = aggregate->m_lddstate;
- MDD complete_state = Accessible_epsilon(get_successor(meta_state, transition));
+ MDD complete_state = saturatePOR(get_successor(meta_state, transition), fireObs, _div,
+ _dead);//Accessible_epsilon(get_successor(meta_state, transition));
bool res;
pos = m_graph->insertFindByMDD(complete_state, res);
{
@@ -115,8 +118,8 @@ void *MCThReqPor::Compute_successors() {
LDDEdge(aggregate, transition));
}
if (!res) {
- pos->setDiv(Set_Div(complete_state));
- pos->setDeadLock(Set_Bloc(complete_state));
+ pos->setDiv(_div);
+ pos->setDeadLock(_dead);
}
aggregate->decNbSuccessors();
if (aggregate->m_nbSuccessorsToBeProcessed == 0) {
@@ -127,11 +130,11 @@ void *MCThReqPor::Compute_successors() {
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));
+
+ pos->m_nbSuccessorsToBeProcessed = fireObs.size();
+ if (!fireObs.empty()) {
+ for (const auto &e: fireObs)
+ m_common_stack.push(couple_th(pos, e));
} else {
pos->setCompletedSucc();
m_datacondBuildCompleted.notify_one();
@@ -151,7 +154,7 @@ void *MCThReqPor::Compute_successors() {
MCThReqPor::~MCThReqPor() {
//pthread_barrier_wait(&m_barrier_threads);
- for (int i = 0; i < m_nb_thread; i++) {
+ for (auto i = 0; i < m_nb_thread; ++i) {
m_list_thread[i]->join();
delete m_list_thread[i];
}
diff --git a/src/MCMultiCore/ModelCheckerTh.cpp b/src/MCMultiCore/ModelCheckerTh.cpp
index c07d838944763c6f42c2f8dccc5d8f2f25dabc0e..1ee9bd8d727a51480a1bc64d2a8b1b251ef82460 100644
--- a/src/MCMultiCore/ModelCheckerTh.cpp
+++ b/src/MCMultiCore/ModelCheckerTh.cpp
@@ -115,9 +115,6 @@ void* ModelCheckerTh::Compute_successors() {
}
m_terminaison[id_thread] = true;
} while (isNotTerminated() && !m_finish);
-
-
-
}
void* ModelCheckerTh::threadHandler(void *context) {
diff --git a/src/ModelCheckBaseMT.h b/src/ModelCheckBaseMT.h
index 83bacc64d5003a7cc363b59005bba53206148763..f849b09df103c8959fa4f3462d7772532aa24435 100644
--- a/src/ModelCheckBaseMT.h
+++ b/src/ModelCheckBaseMT.h
@@ -9,7 +9,6 @@ public:
virtual LDDState * getInitialMetaState();
virtual void buildSucc(LDDState *agregate);
void loadNet();
-
virtual ~ModelCheckBaseMT();
protected:
std::condition_variable m_condBuild;
@@ -17,6 +16,5 @@ protected:
private:
virtual void preConfigure()=0;
std::mutex m_mutexBuild;
-
};
#endif
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 3c82d62aa464d755d9e12bfed3e0179ce6546e8d..569932e49d1805890626938908cd87ce6dd951c9 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -390,7 +390,6 @@ MDD SylvanWrapper::lddmc_makenode(uint32_t value, MDD ifeq, MDD ifneq) {
}
-
return (MDD) index;
}
@@ -806,12 +805,13 @@ MDD SylvanWrapper::ldd_minus(MDD a, MDD b) {
SylvanCacheWrapper::cache_put(CACHE_LDD_MINUS, a, b, result);
return result;
}
+
/*
* Check whether transition removing @minus tokens is firable in marking @cmark
*/
bool SylvanWrapper::isFirable(MDD cmark, MDD minus) {
if (cmark == lddmc_true) return true;
- bool result {false};
+ bool result{false};
MDD _cmark = cmark, _minus = minus;
mddnode_t n_cmark = GETNODE(_cmark);
mddnode_t n_minus = GETNODE(_minus);
@@ -822,10 +822,10 @@ bool SylvanWrapper::isFirable(MDD cmark, MDD minus) {
uint32_t value_minus = mddnode_getvalue(n_minus);
if (value >= value_minus) {
- MDD _mark=mddnode_getdown(n_cmark);
- if (_mark==lddmc_true) return true;
- MDD _minus=mddnode_getdown(n_minus);
- result=isFirable(_mark, _minus);
+ MDD _mark = mddnode_getdown(n_cmark);
+ if (_mark == lddmc_true) return true;
+ MDD _minus = mddnode_getdown(n_minus);
+ result = isFirable(_mark, _minus);
}
cmark = mddnode_getright(n_cmark);
if (cmark == lddmc_false || result) return result;
@@ -833,7 +833,8 @@ 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;
@@ -848,8 +849,6 @@ MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, const MDD minus,const MDD plus)
mddnode_t n_cmark = GETNODE(_cmark);
mddnode_t n_plus = GETNODE(_plus);
mddnode_t n_minus = GETNODE(_minus);
-
-
result = lddmc_false;
for (;;) {
@@ -928,6 +927,7 @@ 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
*/
@@ -977,11 +977,9 @@ void SylvanWrapper::sylvan_gc_seq() {
}
-void SylvanWrapper::sylvan_rehash_all()
-{
+void SylvanWrapper::sylvan_rehash_all() {
// clear hash array
llmsset_clear_hashes_seq(m_nodes);
-
// rehash marked nodes
if (llmsset_rehash_seq(m_nodes) != 0) {
fprintf(stderr, "sylvan_gc_rehash error: not all nodes could be rehashed!\n");
@@ -990,25 +988,23 @@ void SylvanWrapper::sylvan_rehash_all()
}
-int SylvanWrapper::llmsset_rehash_seq (llmsset2_t dbs)
-{
- return llmsset_rehash_par_seq( dbs, 0, dbs->table_size);
+int SylvanWrapper::llmsset_rehash_seq(llmsset2_t dbs) {
+ return llmsset_rehash_par_seq(dbs, 0, dbs->table_size);
}
-int SylvanWrapper::llmsset_rehash_par_seq(llmsset2_t dbs, size_t first, size_t count)
-{
+int SylvanWrapper::llmsset_rehash_par_seq(llmsset2_t dbs, size_t first, size_t count) {
if (count > 512) {
- int bad = llmsset_rehash_par_seq(dbs, first + count/2, count - count/2);
- return bad + llmsset_rehash_par_seq(dbs, first, count/2);
+ int bad = llmsset_rehash_par_seq(dbs, first + count / 2, count - count / 2);
+ return bad + llmsset_rehash_par_seq(dbs, first, count / 2);
} else {
int bad = 0;
uint64_t *ptr = dbs->bitmap2 + (first / 64);
uint64_t mask = 0x8000000000000000LL >> (first & 63);
- for (size_t k=0; k<count; k++) {
+ for (size_t k = 0; k < count; k++) {
if (*ptr & mask) {
- if (llmsset_rehash_bucket(dbs, first+k) == 0) bad++;
+ if (llmsset_rehash_bucket(dbs, first + k) == 0) bad++;
}
mask >>= 1;
if (mask == 0) {
@@ -1021,9 +1017,8 @@ int SylvanWrapper::llmsset_rehash_par_seq(llmsset2_t dbs, size_t first, size_t
}
-int SylvanWrapper::llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx)
-{
- const uint64_t * const d_ptr = ((uint64_t*)dbs->data) + 2*d_idx;
+int SylvanWrapper::llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx) {
+ const uint64_t *const d_ptr = ((uint64_t *) dbs->data) + 2 * d_idx;
const uint64_t a = d_ptr[0];
const uint64_t b = d_ptr[1];
@@ -1033,7 +1028,7 @@ int SylvanWrapper::llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx)
else hash_rehash = llmsset_hash(a, b, hash_rehash);
const uint64_t step = (((hash_rehash >> 20) | 1) << 3);
const uint64_t new_v = (hash_rehash & MASK_HASH) | d_idx;
- int i=0;
+ int i = 0;
uint64_t idx, last;
#if LLMSSET_MASK
@@ -1047,9 +1042,9 @@ int SylvanWrapper::llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx)
if (*bucket == 0 && cas(bucket, 0, new_v)) return 1;
// find next idx on probe sequence
- idx = (idx & CL_MASK) | ((idx+1) & CL_MASK_R);
+ idx = (idx & CL_MASK) | ((idx + 1) & CL_MASK_R);
if (idx == last) {
- if (++i == *(volatile int16_t*)&dbs->threshold) {
+ if (++i == *(volatile int16_t *) &dbs->threshold) {
// failed to find empty spot in probe sequence
// solution: increase probe sequence length...
__sync_fetch_and_add(&dbs->threshold, 1);
@@ -1068,22 +1063,17 @@ int SylvanWrapper::llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx)
}
-int SylvanWrapper::is_custom_bucket(const llmsset2_t dbs, uint64_t index)
-{
- uint64_t *ptr = dbs->bitmapc + (index/64);
- uint64_t mask = 0x8000000000000000LL >> (index&63);
+int SylvanWrapper::is_custom_bucket(const llmsset2_t dbs, uint64_t index) {
+ uint64_t *ptr = dbs->bitmapc + (index / 64);
+ uint64_t mask = 0x8000000000000000LL >> (index & 63);
return (*ptr & mask) ? 1 : 0;
}
-
-
-
-
-void SylvanWrapper::llmsset_clear_hashes_seq( llmsset2_t dbs)
-{
+void SylvanWrapper::llmsset_clear_hashes_seq(llmsset2_t dbs) {
// just reallocate...
- if (mmap(dbs->table, dbs->max_size * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS | MAP_FIXED, -1, 0) != (void*)-1) {
+ if (mmap(dbs->table, dbs->max_size * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS | MAP_FIXED, -1, 0) !=
+ (void *) -1) {
#if defined(madvise) && defined(MADV_RANDOM)
madvise(dbs->table, sizeof(uint64_t[dbs->max_size]), MADV_RANDOM);
#endif
@@ -1094,7 +1084,6 @@ void SylvanWrapper::llmsset_clear_hashes_seq( llmsset2_t dbs)
}
-
void SylvanWrapper::llmsset_destroy_unmarked(llmsset2_t dbs) {
if (dbs->destroy_cb == NULL) return; // no custom function
llmsset_destroy(dbs, 0, dbs->table_size);
@@ -1199,6 +1188,64 @@ int SylvanWrapper::llmsset_mark(const llmsset2_t dbs, uint64_t index) {
}
}
+/*
+ * Intersection
+ */
+
+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;
+ assert(a != lddmc_true && b != lddmc_true);
+
+/* Test gc */
+//sylvan_gc_test();
+
+
+
+/* Get nodes */
+ mddnode_t na = LDD_GETNODE(a);
+ mddnode_t nb = LDD_GETNODE(b);
+ uint32_t na_value = mddnode_getvalue(na);
+ uint32_t nb_value = mddnode_getvalue(nb);
+
+/* Skip nodes if possible */
+ while (na_value != nb_value) {
+ if (na_value < nb_value) {
+ a = mddnode_getright(na);
+ if (a == lddmc_false) return lddmc_false;
+ na = LDD_GETNODE(a);
+ na_value = mddnode_getvalue(na);
+ }
+ if (nb_value < na_value) {
+ b = mddnode_getright(nb);
+ if (b == lddmc_false) return lddmc_false;
+ nb = LDD_GETNODE(b);
+ nb_value = mddnode_getvalue(nb);
+ }
+ }
+
+/* Access cache */
+ MDD result;
+ if (SylvanCacheWrapper::cache_get3(CACHE_MDD_INTERSECT, a, b, 0, &result)) {
+
+ return result;
+ }
+
+/* Perform recursive calculation */
+
+ MDD down = lddmc_intersect( mddnode_getdown(na), mddnode_getdown(nb));
+ //lddmc_refs_push(down);
+ MDD right = lddmc_intersect(mddnode_getright(na), mddnode_getright(nb));
+ //ldd_refs_pop(1);
+ result = lddmc_makenode(na_value, down, right);
+
+/* Write to cache */
+ SylvanCacheWrapper::cache_put3(CACHE_MDD_INTERSECT, a, b, 0, result);
+
+ return result;
+}
+
size_t SylvanWrapper::m_table_min = 0;
size_t SylvanWrapper::m_table_max = 0;
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
index 0848011068c00149352ded4d68e57cfe1f4de444..a1ad54c4e0bc27a6af0d3fcf53150183eba212d3 100644
--- a/src/SylvanWrapper.h
+++ b/src/SylvanWrapper.h
@@ -174,7 +174,7 @@ public:
static size_t lddmc_nodecount(MDD mdd);
static MDD lddmc_union_mono(MDD a, MDD b);
-
+ static MDD lddmc_intersect(MDD a, MDD b);
static bool isSingleMDD(MDD mdd);
static int get_mddnbr(MDD mdd, unsigned int level);
diff --git a/src/main.cpp b/src/main.cpp
index a48ee4932ed01f7668fa252ca250c22e3a540812..ff38313d3c08a42525625cdfee60b3f4c37a25af 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -98,6 +98,7 @@ int main(int argc, char **argv) {
MPI_Init(&argc, &argv);
MPI_Comm_size(MPI_COMM_WORLD, &n_tasks);
MPI_Comm_rank(MPI_COMM_WORLD, &task_id);
+ n_tasks=1;
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;
@@ -323,6 +324,6 @@ int main(int argc, char **argv) {
}
}
MPI_Finalize();
- exit(0);
+
return (EXIT_SUCCESS);
}
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 5a401cf091ffaa3b611a64d1e89dadd46244d211..2a83ad421284d8d63344476496de3c09512e9693 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -215,10 +215,11 @@ void *threadSOG::doCompute() {
int id_thread;
id_thread = m_id_thread++;
Set fire;
+ int min_charge=0;
if (id_thread == 0) {
clock_gettime(CLOCK_REALTIME, &start);
// printf("*******************PARALLEL*******************\n");
- m_min_charge = 0;
+
auto *c = new LDDState;
//cout<<"Marquage initial is being built..."<<endl;
@@ -311,12 +312,12 @@ void *threadSOG::doCompute() {
fire = firable_obs(Complete_meta_state);
//if (max_succ<fire.size()) max_succ=fire.size();
//pthread_mutex_unlock(&m_mutex);
- m_min_charge = minCharge();
+ min_charge = minCharge();
//m_min_charge=(m_min_charge+1) % m_nb_thread;
- pthread_spin_lock(&m_spin_stack[m_min_charge]);
- m_st[m_min_charge].push(Pair(couple(reached_class, Complete_meta_state), fire));
- pthread_spin_unlock(&m_spin_stack[m_min_charge]);
- m_charge[m_min_charge]++;
+ pthread_spin_lock(&m_spin_stack[min_charge]);
+ m_st[min_charge].push(Pair(couple(reached_class, Complete_meta_state), fire));
+ pthread_spin_unlock(&m_spin_stack[min_charge]);
+ m_charge[min_charge]++;
} else {
m_graph->addArc();
m_graph_mutex.unlock();
@@ -342,10 +343,11 @@ void *threadSOG::doComputeCanonized() {
int id_thread;
id_thread = m_id_thread++;
Set fire;
+ uint16_t min_charge;
if (id_thread == 0) {
clock_gettime(CLOCK_REALTIME, &start);
// printf("*******************PARALLEL*******************\n");
- m_min_charge = 0;
+
auto *c = new LDDState;
MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
//#ldd_refs_push(Complete_meta_state);
@@ -433,12 +435,12 @@ void *threadSOG::doComputeCanonized() {
fire = firable_obs(Complete_meta_state);
//if (max_succ<fire.size()) max_succ=fire.size();
//pthread_mutex_unlock(&m_mutex);
- m_min_charge = minCharge();
+ min_charge = minCharge();
//m_min_charge=(m_min_charge+1) % m_nb_thread;
- pthread_spin_lock(&m_spin_stack[m_min_charge]);
- m_st[m_min_charge].push(Pair(couple(reached_class, Complete_meta_state), fire));
- pthread_spin_unlock(&m_spin_stack[m_min_charge]);
- m_charge[m_min_charge]++;
+ pthread_spin_lock(&m_spin_stack[min_charge]);
+ m_st[min_charge].push(Pair(couple(reached_class, Complete_meta_state), fire));
+ pthread_spin_unlock(&m_spin_stack[min_charge]);
+ m_charge[min_charge]++;
} else {
m_graph->addArc();
m_graph_mutex.unlock();
@@ -553,16 +555,17 @@ void *threadSOG::doComputePOR() {
id_thread = m_id_thread++;
Set fireObs;
bool _div, _dead;
+ MDD Complete_meta_state;
+ int min_charge = 0;
if (id_thread == 0) {
clock_gettime(CLOCK_REALTIME, &start);
- // printf("*******************PARALLEL*******************\n");
- m_min_charge = 0;
auto *c = new LDDState;
- MDD Complete_meta_state{saturatePOR(m_initialMarking, fireObs, _div, _dead)};
- cout<<"Size of obs : "<<fireObs.size()<<endl;
+ Complete_meta_state=saturatePOR(m_initialMarking, fireObs, _div, _dead);
+ cout<<Complete_meta_state<<endl;
+ //cout<<"Size of Obs : "<<fireObs.size()<<endl;
c->m_lddstate = Complete_meta_state;
- Set cpy=fireObs;
- m_st[0].push(Pair(couple(c, Complete_meta_state), cpy));
+
+ m_st[0].push(Pair(couple(c, Complete_meta_state), fireObs));
m_graph->setInitialState(c);
m_graph->insert(c);
m_charge[0] = 1;
@@ -587,8 +590,10 @@ void *threadSOG::doComputePOR() {
m_gc_mutex.lock();
}
}
- Set cpy=fireObs;
- MDD Complete_meta_state{saturatePOR(get_successor(e.first.second, t), cpy, _div, _dead)};
+ MDD succ=get_successor(e.first.second, t);
+ Complete_meta_state=saturatePOR(succ, fireObs, _div, _dead);
+
+ //cout<<"Marks : "<<SylvanWrapper::getMarksCount(Complete_meta_state)<<endl;
/* if (id_thread==0)
{
m_gc_mutex.lock();
@@ -602,32 +607,24 @@ void *threadSOG::doComputePOR() {
m_gc_mutex.unlock();
}*/
reached_class->m_lddstate = Complete_meta_state;
- //reached_class->m_lddstate=reduced_meta;
- //nbnode=bdd_pathcount(reached_class->m_lddstate);
-
- //pthread_spin_lock(&m_accessible);
m_graph_mutex.lock();
LDDState *pos = m_graph->find(reached_class);
if (!pos) {
m_graph->addArc();
m_graph->insert(reached_class);
- m_graph_mutex.unlock();
-
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_min_charge = minCharge();
- //m_min_charge=(m_min_charge+1) % m_nb_thread;
- pthread_spin_lock(&m_spin_stack[m_min_charge]);
- Set cpy=fireObs;
- m_st[m_min_charge].push(Pair(couple(reached_class, Complete_meta_state), cpy));
- pthread_spin_unlock(&m_spin_stack[m_min_charge]);
- m_charge[m_min_charge]++;
- } else {
m_graph_mutex.unlock();
+ min_charge = minCharge();
+ pthread_spin_lock(&m_spin_stack[min_charge]);
+ m_st[min_charge].push(Pair(couple(reached_class, Complete_meta_state), fireObs));
+ pthread_spin_unlock(&m_spin_stack[min_charge]);
+ m_charge[min_charge]++;
+ } else {
m_graph->addArc();
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;
}
if (id_thread) {
diff --git a/src/threadSOG.h b/src/threadSOG.h
index 562e62c7da5636e7d0f8f92dc28185d3ab0b2c66..f0d4f750f600c3969cb5ba14fa6999f0d6595508 100644
--- a/src/threadSOG.h
+++ b/src/threadSOG.h
@@ -35,7 +35,7 @@ class threadSOG : public CommonSOG {
pile m_st[128];
int m_charge[128];
bool m_terminaison[128];
- int m_min_charge;
+
int m_init;
std::atomic<int> m_id_thread;
pthread_mutex_t m_mutex;