From 8039841c2a02e4d42d37d9e4086dc6d6c01bb272 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sat, 29 Jan 2022 01:22:34 +0100
Subject: [PATCH] Add and Test POR construction
---
src/CommonSOG.cpp | 34 +++--
src/CommonSOG.h | 3 -
src/NewNet.cpp | 320 +++++++++++++++---------------------------
src/SylvanWrapper.cpp | 3 -
src/main.cpp | 9 +-
src/threadSOG.cpp | 60 +++-----
6 files changed, 156 insertions(+), 273 deletions(-)
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 148067b..75a2c9a 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -28,7 +28,7 @@ MDD CommonSOG::Accessible_epsilon(const MDD& From) {
// Return the set of firable observable transitions from an agregate
Set CommonSOG::firable_obs(const MDD& State) {
Set res;
- for (auto i: m_observable) {
+ for (const 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);
@@ -137,7 +137,6 @@ bool CommonSOG::Set_Div(const MDD &M) const {
/**** Detetc deadlocks ****/
bool CommonSOG::Set_Bloc(const MDD &M) const {
-
MDD cur {lddmc_true};
for (const auto & i: m_tb_relation) {
cur = cur & (i.getMinus());
@@ -161,7 +160,6 @@ LDDGraph *CommonSOG::m_graph;
//}
string_view CommonSOG::getPlace(int pos) {
-
return string_view{m_graph->getPlace(pos)};
}
@@ -239,25 +237,28 @@ 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;
}
}
return false;
};
+ // cout<<"Transition to deal with : "<<transition<<endl;
if (SylvanWrapper::isFirable(S,m_tb_relation[transition].getMinus())) {
- for (auto i = 0; i < m_transitions.size(); i++) {
+ //cout<<"Checked\n";
+ for ( auto i = 0; i < m_transitions.size(); ++i) {
if (i != transition) {
auto &preT1 = m_transitions[i].pre;
auto &preT2 = m_transitions[transition].pre;
- if (!haveCommonPre(preT1, preT2)) ample.insert(i);
+ if (haveCommonPre(preT1, preT2)) ample.insert(i);
}
}
} else {
- for (auto i = 0; i < m_transitions.size(); i++) {
+ for (auto i = 0; i < m_transitions.size(); ++i) {
if (i != transition) {
auto &postT1 = m_transitions[i].post;
auto &preT2 = m_transitions[transition].pre;
- if (!haveCommonPre(postT1, preT2)) ample.insert(i);
+ if (haveCommonPre(postT1, preT2)) ample.insert(i);
}
}
}
@@ -271,15 +272,17 @@ Set CommonSOG::computeAmple(const MDD &s) {
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 &t : enabledT) {
+ for (const auto &t : ample) {
+ //for (int i=0;i<m_transitions.size();++i) {
AddConflict(s,t,ample);
}
+ //cout<<"Size of ample : "<<ample.size()<<endl;
return ample;
}
@@ -297,7 +300,7 @@ MDD CommonSOG::saturatePOR(const MDD &s, Set& tObs,bool &div,bool &dead) {
if (ample.empty()) dead=true;
else {
for (const auto & t : ample) {
- MDD succ= get_successor(s,t);
+ MDD succ= get_successor(From,t);
if (m_transitions[t].mObservable) {
tObs.insert(t);
}
@@ -305,6 +308,16 @@ MDD CommonSOG::saturatePOR(const MDD &s, Set& tObs,bool &div,bool &dead) {
//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);
+ }
+ }
+ }
}
else {
To=SylvanWrapper::lddmc_union_mono(To,succ);
@@ -317,5 +330,6 @@ MDD CommonSOG::saturatePOR(const MDD &s, Set& tObs,bool &div,bool &dead) {
From=To;
Reach2=SylvanWrapper::lddmc_union_mono(Reach2,To);
} while (Reach1!=Reach2);
+ // cout<<"Size of obs : "<<tObs.size()<<endl;
return Reach1;
}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index d1065fb..9ef0205 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -23,7 +23,6 @@ class LDDGraph;
class CommonSOG {
public:
CommonSOG();
-
virtual ~CommonSOG();
static LDDGraph *getGraph();
@@ -37,9 +36,7 @@ public:
}
static string_view getPlace(int pos);
-
void finish() { m_finish = true; }
-
virtual void computeDSOG(LDDGraph &g) {};
protected:
static void initializeLDD();
diff --git a/src/NewNet.cpp b/src/NewNet.cpp
index ed28d03..4c9a4be 100644
--- a/src/NewNet.cpp
+++ b/src/NewNet.cpp
@@ -14,77 +14,63 @@ using namespace std;
/* class Node */
/***********************************************************/
-void Node::addPre(int node, int valuation)
-{
+void Node::addPre(int node, int valuation) {
pair<int, int> x(node, valuation);
pre.push_back(x);
}
-void Node::addPost(int node, int valuation)
-{
+void Node::addPost(int node, int valuation) {
pair<int, int> x(node, valuation);
post.push_back(x);
}
-void Node::addInhibitor(int node, int valuation)
-{
+void Node::addInhibitor(int node, int valuation) {
pair<int, int> x(node, valuation);
inhibitor.push_back(x);
}
-void Node::addPreAuto(int node, int valuation)
-{
+void Node::addPreAuto(int node, int valuation) {
pair<int, int> x(node, valuation);
preAuto.push_back(x);
}
-void Node::addPostAuto(int node, int valuation)
-{
+void Node::addPostAuto(int node, int valuation) {
pair<int, int> x(node, valuation);
postAuto.push_back(x);
}
-void Node::addReset(int node)
-{
+void Node::addReset(int node) {
reset.push_back(node);
}
/***********************************************************/
/* class RdPE */
/***********************************************************/
-NewNet::NewNet(const char *f, const char *Formula_trans, const char *Int_trans)
-{
+NewNet::NewNet(const char *f, const char *Formula_trans, const char *Int_trans) {
cout << "CREATION D'UN NOUVEAU SOUS-RESEAU \n";
- if (create(f))
- {
+ if (create(f)) {
for (vector<class Place>::iterator p = places.begin(); p != places.end();
- p++)
- {
+ p++) {
sort(p->pre.begin(), p->pre.end());
sort(p->post.begin(), p->post.end());
}
for (vector<class Transition>::iterator p = transitions.begin();
- p != transitions.end(); p++)
- {
+ p != transitions.end(); p++) {
sort(p->pre.begin(), p->pre.end());
sort(p->post.begin(), p->post.end());
}
- }
- else
- {
+ } else {
places.clear();
transitions.clear();
m_placeName.clear();
transitionName.clear();
}
- if (strlen(Formula_trans) > 0)
- {
- cout<<"transitions de la formule non vide \n";
+ if (strlen(Formula_trans) > 0) {
+ cout << "transitions de la formule non vide \n";
Set_Formula_Trans(Formula_trans);
- if (strlen(Int_trans) > 0)
- {
+ if (strlen(Int_trans) > 0) {
Set_Interface_Trans(Int_trans);
// cout<<"transitions de l'interface non vide \n";
}
@@ -93,113 +79,97 @@ NewNet::NewNet(const char *f, const char *Formula_trans, const char *Int_trans)
Formula_Trans.begin(), Formula_Trans.end(),
inserter(Observable, Observable.begin()));
Set_Non_Observables();
- }
- else
+ } else
for (unsigned int i = 0; i < transitions.size(); i++)
Observable.insert(i);
cout << "FIN CREATION \n";
}
+
/***************************** Constructor for Model checker******************/
-NewNet::NewNet(const char *f, const set<string> & f_trans)
-{
+NewNet::NewNet(const char *f, const set<string> &f_trans) {
cout << "CREATION D'UN NOUVEAU SOUS-RESEAU \n";
- if (create(f))
- {
+ if (create(f)) {
for (vector<class Place>::iterator p = places.begin(); p != places.end();
- p++)
- {
+ p++) {
sort(p->pre.begin(), p->pre.end());
sort(p->post.begin(), p->post.end());
}
for (vector<class Transition>::iterator p = transitions.begin();
- p != transitions.end(); p++)
- {
+ p != transitions.end(); p++) {
sort(p->pre.begin(), p->pre.end());
sort(p->post.begin(), p->post.end());
}
- }
- else
- {
+ } else {
places.clear();
transitions.clear();
m_placeName.clear();
transitionName.clear();
}
- 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++)
- {
- cout<<"Transition observable :"<<*p<<endl;
+ 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++) {
+ cout << "Transition observable :" << *p << endl;
}
setListObservable(f_trans);
//for(Set::iterator p=Formula_Trans.begin();p!=Formula_Trans
cout << "______________66666666666666666666666______________________\n";
- cout<<"Formula trans size "<<Formula_Trans.size()<<endl;
- cout<<"Interface trans size "<<InterfaceTrans.size()<<endl;
+ cout << "Formula trans size " << Formula_Trans.size() << endl;
+ cout << "Interface trans size " << InterfaceTrans.size() << endl;
set_union(InterfaceTrans.begin(), InterfaceTrans.end(),
Formula_Trans.begin(), Formula_Trans.end(),
inserter(Observable, Observable.begin()));
Set_Non_Observables();
- }
- else
+ } else
for (unsigned int i = 0; i < transitions.size(); i++) {
Observable.insert(i);
- transitions[i].mObservable=true;
+ transitions[i].mObservable = true;
}
cout << "FIN CREATION \n";
}
/*---------------------------------Init Set of transitions
* ------------------------------*/
-void NewNet::setListObservable(const set<string> & list_t)
-{
+void NewNet::setListObservable(const set<string> &list_t) {
int pos_trans(TRANSITIONS T, string trans);
Observable.clear();
- for (auto it=m_placeName.begin();it!=m_placeName.end();it++) {
- pair<int,string> elt((*it).second,(*it).first);
+ for (auto it = m_placeName.begin(); it != m_placeName.end(); it++) {
+ pair<int, string> elt((*it).second, (*it).first);
m_placePosName.insert(elt);
}
- for (auto it=transitionName.begin();it!=transitionName.end();it++) {
- pair<int,string> elt((*it).second,(*it).first);
+ for (auto it = transitionName.begin(); it != transitionName.end(); it++) {
+ pair<int, string> elt((*it).second, (*it).first);
m_transitionPosName.insert(elt);
}
- for (set<string>::const_iterator i=list_t.begin(); i!=list_t.end(); i++)
- {
+ for (set<string>::const_iterator i = list_t.begin(); i != list_t.end(); i++) {
int pos = pos_trans(transitions, *i);
- if (pos==-1)
- {
- cout<<"Error: "<<*i<<" is not a transition!"<<endl;
+ if (pos == -1) {
+ cout << "Error: " << *i << " is not a transition!" << endl;
// Check if the proposition corresponds to a place
map<string, uint16_t>::iterator pi = m_placeName.find(*i);
- assert (pi!=m_placeName.end());
+ assert (pi != m_placeName.end());
m_formula_place.insert(pi->second);
m_lplaceAP.insert(*i);
// Adding adjacent transitions of a place as observable transitions
- Place p=places.at(pi->second);
- for (auto iter=p.post.begin(); iter!=p.post.end(); iter++)
- {
+ Place p = places.at(pi->second);
+ for (auto iter = p.post.begin(); iter != p.post.end(); iter++) {
Observable.insert((*iter).first);
- auto it=m_transitionPosName.find((*iter).first);
+ auto it = m_transitionPosName.find((*iter).first);
m_ltransitionAP.insert(it->second);
}
- for (auto iter=p.pre.begin(); iter!=p.pre.end(); iter++)
- {
+ for (auto iter = p.pre.begin(); iter != p.pre.end(); iter++) {
Observable.insert((*iter).first);
- auto it=m_transitionPosName.find((*iter).first);
+ auto it = m_transitionPosName.find((*iter).first);
m_ltransitionAP.insert(it->second);
}
- }
- else
- {
+ } else {
Formula_Trans.insert(pos);
- map<string ,uint16_t>::iterator ti=transitionName.find(*i);
+ map<string, uint16_t>::iterator ti = transitionName.find(*i);
Observable.insert(pos);
}
}
@@ -208,8 +178,7 @@ void NewNet::setListObservable(const set<string> & list_t)
/*---------------------------------Set_formula_trans()------------------*/
-bool NewNet::Set_Formula_Trans(const char *f)
-{
+bool NewNet::Set_Formula_Trans(const char *f) {
FILE *in;
int i, nb;
@@ -219,8 +188,7 @@ bool NewNet::Set_Formula_Trans(const char *f)
in = fopen(f, "r");
- if (in == NULL)
- {
+ if (in == NULL) {
cout << "file " << f << " doesn't exist" << endl;
exit(1);
}
@@ -230,28 +198,23 @@ bool NewNet::Set_Formula_Trans(const char *f)
Buff[nb] = '\0';
z = strtok(Buff, " \t\n");
cout << "taille " << TAILLEBUFF << " buff " << Buff << " z: " << z << endl;
- for (i = 0; i < nb_formula_trans; i++)
- {
+ for (i = 0; i < nb_formula_trans; i++) {
cout << " z: " << z << endl;
- if (z == nullptr)
- {
+ if (z == nullptr) {
cout << "error in formula trans format " << endl;
return false;
}
string tmp(z);
int pos = pos_trans(transitions, tmp);
- if (pos == -1)
- {
- cout << z << " Error??? : observale transition " << tmp
+ if (pos == -1) {
+ cout << z << " Error??? : observable transition " << tmp
<< " doesn't exist \n";
// return false;
- }
- else
+ } else
Formula_Trans.insert(pos);
/*cout<<"insertion de :"<<transitions[pos].name<<endl;*/
z = strtok(nullptr, " \t\n");
- if (z == nullptr)
- {
+ if (z == nullptr) {
nb = fread(Buff, 1, TAILLEBUFF - 1, in);
Buff[nb] = '\0';
z = strtok(Buff, " \t\n");
@@ -260,16 +223,15 @@ bool NewNet::Set_Formula_Trans(const char *f)
fclose(in);
return true;
}
+
/*---------------------------------Set_Interface_trans()------------------*/
-bool NewNet::Set_Interface_Trans(const char *f)
-{
+bool NewNet::Set_Interface_Trans(const char *f) {
FILE *in;
int i, nb;
int pos_trans(TRANSITIONS, string);
char Buff[TAILLEBUFF], *z;
in = fopen(f, "r");
- if (in == nullptr)
- {
+ if (in == nullptr) {
cout << "file " << f << " doesn't exist" << endl;
exit(1);
}
@@ -279,27 +241,22 @@ bool NewNet::Set_Interface_Trans(const char *f)
Buff[nb] = '\0';
z = strtok(Buff, " \t\n");
cout << "taille " << TAILLEBUFF << " buff " << Buff << " z: " << z << endl;
- for (i = 0; i < int_trans; i++)
- {
+ for (i = 0; i < int_trans; i++) {
cout << " z: " << z << endl;
- if (z == nullptr)
- {
+ if (z == nullptr) {
cout << "error in interface format " << endl;
return false;
}
string tmp(z);
int pos = pos_trans(transitions, tmp);
// if(Formula_Trans.find(pos)==Formula_Trans.end())
- if (pos == -1)
- {
+ if (pos == -1) {
cout << z << " Error??? : interface transition doesn't exist \n";
// return false;
- }
- else
+ } else
InterfaceTrans.insert(pos);
z = strtok(nullptr, " \t\n");
- if (z == nullptr)
- {
+ if (z == nullptr) {
nb = fread(Buff, 1, TAILLEBUFF - 1, in);
Buff[nb] = '\0';
z = strtok(Buff, " \t\n");
@@ -308,39 +265,34 @@ bool NewNet::Set_Interface_Trans(const char *f)
fclose(in);
return true;
}
+
/*---------------------------------Set_Non_Observables()------------------*/
-void NewNet::Set_Non_Observables()
-{
+void NewNet::Set_Non_Observables() {
NonObservable.clear();
for (unsigned int i = 0; i < transitions.size(); i++)
- if (Observable.find(i) == Observable.end())
- {
+ if (Observable.find(i) == Observable.end()) {
NonObservable.insert(i);
}
}
+
/*-----------------------pos_trans()--------------------*/
-int pos_trans(TRANSITIONS T, string trans)
-{
+int pos_trans(TRANSITIONS T, string trans) {
int pos = 0;
// cout<<"on cherche "<<trans<<" dans :\n";
- for (TRANSITIONS::const_iterator i = T.begin(); !(i == T.end()); i++, pos++)
- {
- // cout<<i->name<<" ";
+ for (auto i = T.begin(); !(i == T.end()); i++, pos++) {
if (i->name == trans)
return pos;
}
// cout<<"Non trouve :\n";
return -1;
}
+
/* ------------------------------ operator<< -------------------------------- */
-ostream &operator<<(ostream &os, const Set &s)
-{
+ostream &operator<<(ostream &os, const Set &s) {
bool b = false;
- if (!s.empty())
- {
- for (Set::const_iterator i = s.begin(); !(i == s.end()); i++)
- {
+ if (!s.empty()) {
+ for (Set::const_iterator i = s.begin(); !(i == s.end()); i++) {
if (b)
os << ", ";
else
@@ -349,70 +301,57 @@ ostream &operator<<(ostream &os, const Set &s)
b = true;
}
os << "}";
- }
- else
+ } else
os << "empty set";
return os;
}
+
/*----------------------------------------------------------------------*/
-bool NewNet::addPlace(const string &place, int marking, int capacity)
-{
- map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
- if (pi == m_placeName.end())
- {
+bool NewNet::addPlace(const string &place, int marking, int capacity) {
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end()) {
m_placeName[string(place)] = places.size();
Place p(place, marking, capacity);
places.push_back(p);
return true;
- }
- else
+ } else
return false;
}
-bool NewNet::addQueue(const string &place, int capacity)
-{
- map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
- if (pi == m_placeName.end())
- {
+bool NewNet::addQueue(const string &place, int capacity) {
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end()) {
m_placeName[place] = places.size();
Place p(place, -1, capacity);
places.push_back(p);
return true;
- }
- else
+ } else
return false;
}
-bool NewNet::addLossQueue(const string &place, int capacity)
-{
+bool NewNet::addLossQueue(const string &place, int capacity) {
map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
- if (pi == m_placeName.end())
- {
+ if (pi == m_placeName.end()) {
m_placeName[place] = places.size();
Place p(place, -2, capacity);
places.push_back(p);
return true;
- }
- else
+ } else
return false;
}
-bool NewNet::addTrans(const string &trans)
-{
- map<string,uint16_t>::const_iterator ti = transitionName.find(trans);
- if (ti == transitionName.end())
- {
+bool NewNet::addTrans(const string &trans) {
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end()) {
transitionName[trans] = transitions.size();
Transition t(trans);
transitions.push_back(t);
return true;
- }
- else
+ } else
return false;
}
-bool NewNet::addPre(const string &place, const string &trans, int valuation)
-{
+bool NewNet::addPre(const string &place, const string &trans, int valuation) {
int p, t;
map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
if (pi == m_placeName.end() || places[pi->second].isQueue())
@@ -429,8 +368,7 @@ bool NewNet::addPre(const string &place, const string &trans, int valuation)
return true;
}
-bool NewNet::addPost(const string &place, const string &trans, int valuation)
-{
+bool NewNet::addPost(const string &place, const string &trans, int valuation) {
int p, t;
map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
if (pi == m_placeName.end() || places[pi->second].isQueue())
@@ -447,15 +385,14 @@ bool NewNet::addPost(const string &place, const string &trans, int valuation)
return true;
}
-bool NewNet::addPreQueue(const string &place, const string &trans, int valuation)
-{
+bool NewNet::addPreQueue(const string &place, const string &trans, int valuation) {
int p, t;
- map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
if (pi == m_placeName.end() || !places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string , uint16_t>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -466,15 +403,14 @@ bool NewNet::addPreQueue(const string &place, const string &trans, int valuation
}
bool NewNet::addPostQueue(const string &place, const string &trans,
- int valuation)
-{
+ int valuation) {
int p, t;
- map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
if (pi == m_placeName.end() || !places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string , uint16_t>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -485,8 +421,7 @@ bool NewNet::addPostQueue(const string &place, const string &trans,
}
bool NewNet::addInhibitor(const string &place, const string &trans,
- int valuation)
-{
+ int valuation) {
int p, t;
map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
if (pi == m_placeName.end())
@@ -504,8 +439,7 @@ bool NewNet::addInhibitor(const string &place, const string &trans,
}
bool NewNet::addPreAuto(const string &place, const string &trans,
- const string &valuation)
-{
+ const string &valuation) {
int p, t, v;
map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
if (pi == m_placeName.end() || places[pi->second].isQueue())
@@ -528,8 +462,7 @@ bool NewNet::addPreAuto(const string &place, const string &trans,
}
bool NewNet::addPostAuto(const string &place, const string &trans,
- const string &valuation)
-{
+ const string &valuation) {
int p, t, v;
map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
if (pi == m_placeName.end() || places[pi->second].isQueue())
@@ -551,8 +484,7 @@ bool NewNet::addPostAuto(const string &place, const string &trans,
return true;
}
-bool NewNet::addReset(const string &place, const string &trans)
-{
+bool NewNet::addReset(const string &place, const string &trans) {
int p, t;
auto pi = m_placeName.find(place);
if (pi == m_placeName.end())
@@ -570,8 +502,7 @@ bool NewNet::addReset(const string &place, const string &trans)
}
/* Visualisation */
-ostream &operator<<(ostream &os, const NewNet &R)
-{
+ostream &operator<<(ostream &os, const NewNet &R) {
/* affichage nombre de places et de transitions */
os << "***************************" << endl;
os << "Nombre de places :" << R.nbPlace() << endl;
@@ -581,75 +512,44 @@ ostream &operator<<(ostream &os, const NewNet &R)
os << "********** places **********" << endl;
int i = 0;
for (vector<class Place>::const_iterator p = R.places.begin();
- p != R.places.end(); p++, i++)
- {
- if (p->isQueue())
- {
+ p != R.places.end(); p++, i++) {
+ if (p->isQueue()) {
os << "queue " << setw(4) << i << ":" << p->name << ", cp(" << p->capacity
<< ")";
if (p->isLossQueue())
cout << " loss";
cout << endl;
- }
- else
+ } else
os << "place " << setw(4) << i << ":" << p->name << ":" << p->marking
<< " <..>, cp(" << p->capacity << ")" << endl;
}
os << "********** transitions de la formule **********" << endl;
for (Set::const_iterator h = R.Formula_Trans.begin();
- !(h == R.Formula_Trans.end()); h++)
+ !(h == R.Formula_Trans.end()); h++)
cout << R.transitions[*h].name << endl;
os << "********** transitions de l'interface **********" << endl;
for (Set::const_iterator h = R.InterfaceTrans.begin();
- !(h == R.InterfaceTrans.end()); h++)
+ !(h == R.InterfaceTrans.end()); h++)
cout << R.transitions[*h].name << endl;
os << "Nombre de transitions observable:" << R.Observable.size() << endl;
os << "********** transitions observables **********" << endl;
for (Set::const_iterator h = R.Observable.begin(); !(h == R.Observable.end());
- h++)
+ h++)
cout << R.transitions[*h].name << endl;
os << "Nombre de transitions non observees:" << R.NonObservable.size()
<< endl;
os << "********** transitions non observees **********" << endl;
for (Set::const_iterator h = R.NonObservable.begin();
- !(h == R.NonObservable.end()); h++)
+ !(h == R.NonObservable.end()); h++)
cout << R.transitions[*h].name << endl;
i = 0;
os << "Nombre global de transitions :" << R.nbTransition() << endl;
os << "********** transitions **********" << endl;
for (TRANSITIONS::const_iterator t = R.transitions.begin();
- t != R.transitions.end(); t++, i++)
- {
+ t != R.transitions.end(); t++, i++) {
os << setw(4) << i << ":" << t->name << endl;
- // os<<" IN { ";
- // for (vector< pair<int,int> >::const_iterator
- // a=p->pre.begin();a!=p->pre.end();a++)
- // if (R.places[a->first].isQueue())
- // os<<R.places[a->first].name<<":<"<<a->second<<">;";
- // else
- // os<<R.places[a->first].name<<":"<<a->second<<";";
- // for (vector< pair<int,int> >::const_iterator
- // a=p->inhibitor.begin();a!=p->inhibitor.end();a++)
- // os<<R.places[a->first].name<<"<"<<a->second<<";";
- // for (vector< pair<int,int> >::const_iterator
- // a=p->preAuto.begin();a!=p->preAuto.end();a++)
- // os<<R.places[a->first].name<<":"<<R.places[a->second].name<<";";
- // for (vector<int>::const_iterator
- // a=p->reset.begin();a!=p->reset.end();a++) os<<R.places[*a].name<<":
- // reset;"; os<<" }"<<endl;
-
- // os<<" OUT { ";
- // for (vector< pair<int,int> >::const_iterator
- // a=p->post.begin();a!=p->post.end();a++)
- // if (R.places[a->first].isQueue())
- // os<<R.places[a->first].name<<":<"<<a->second<<">;";
- // else
- // os<<R.places[a->first].name<<":"<<a->second<<";";
- // for (vector< pair<int,int> >::const_iterator
- // a=p->postAuto.begin();a!=p->postAuto.end();a++)
- // os<<R.places[a->first].name<<":"<<R.places[a->second].name<<";";
- // os<<" }"<<endl;
+
}
return (os);
}
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 8ae7993..3c82d62 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -831,10 +831,7 @@ bool SylvanWrapper::isFirable(MDD cmark, MDD minus) {
if (cmark == lddmc_false || result) return result;
n_cmark = GETNODE(cmark);
}
-
return result;
-
-
}
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
diff --git a/src/main.cpp b/src/main.cpp
index 0924cee..a48ee49 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -63,7 +63,7 @@ set<string> buildPropositions(const string &fileName) {
return transitionSet;
}
spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, nullptr);
- for (const auto i : *p_list) {
+ for (const auto & i : *p_list) {
transitionSet.insert(i.ap_name());
}
print_spin_ltl(std::cout, fo) << '\n';
@@ -188,16 +188,19 @@ int main(int argc, char **argv) {
g.printCompleteInformation();
} else {
cout << "*******************Multithread version****************** \n" << endl;
+ cout << "Count of threads to be created: " << nb_th << endl;
if (!strcmp(argv[1], "p")) {
cout << "Construction with pthread library." << endl;
- cout << "Count of threads to be created: " << nb_th << endl;
DR.computeDSOG(g, 0);
g.printCompleteInformation();
} else if (!strcmp(argv[1], "pc")) {
cout << "Canonized construction with pthread library." << endl;
- cout << "Count of threads to be created: " << nb_th << endl;
DR.computeDSOG(g, 1);
g.printCompleteInformation();
+ } else {
+ cout << "Partial Order Reduction with pthread library." << endl;
+ DR.computeDSOG(g, 2);
+ g.printCompleteInformation();
}
cout << "Perform Model checking ?";
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index df7e288..5a401cf 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -39,11 +39,6 @@ threadSOG::threadSOG(const NewNet &R, int nbThread, bool uselace, bool init) {
m_init = init;
int i;
- vector<Place>::const_iterator it_places;
-
-
-
-
//_______________
m_transitions = R.transitions;
@@ -63,13 +58,17 @@ threadSOG::threadSOG(const NewNet &R, int nbThread, bool uselace, bool init) {
cout << "Observable transitions:" << endl;
- for (const auto &it: m_observable) { cout << it << " "; }
+ for (const auto &it: m_observable) {
+ m_transitions[it].mObservable=true;
+ cout << it << " ";
+ }
cout << endl;
m_nbPlaces = R.places.size();
cout << "Nombre de places : " << m_nbPlaces << endl;
cout << "Derniere place : " << R.places[m_nbPlaces - 1].name << endl;
auto *liste_marques = new uint32_t[R.places.size()];
+ auto it_places= R.places.begin();
for (i = 0, it_places = R.places.begin(); it_places != R.places.end(); ++i, ++it_places) {
liste_marques[i] = it_places->marking;
}
@@ -126,14 +125,6 @@ void threadSOG::computeSeqSOG(LDDGraph &g) {
//-------------------------------------------------------------------
//-------------------------------------------------------------------
- int nb_failed = 0;
- // cout<<"COMPUTE CANONICAL DETERMINISTIC GRAPH_________________________ \n";
- //cout<<"nb MDD var : "<<bdd_varnum()<<endl;
- // double d,tps;
- //d=(double)clock() / (double)CLOCKS_PER_SEC;
-
-
-
typedef pair<LDDState *, MDD> couple;
typedef pair<couple, Set> Pair;
typedef stack<Pair> pile;
@@ -188,7 +179,6 @@ void threadSOG::computeSeqSOG(LDDGraph &g) {
auto *pos = g.find(reached_class);
//nbnode=sylvan_pathcount(reached_class->m_lddstate);
if (!pos) {
- // cout<<"not found"<<endl;
reached_class->m_boucle = Set_Div(Complete_meta_state);
fire = firable_obs(Complete_meta_state);
st.push(Pair(couple(reached_class, Complete_meta_state), fire));
@@ -200,7 +190,6 @@ void threadSOG::computeSeqSOG(LDDGraph &g) {
g.insert(reached_class);
} else {
// cout<<" found"<<endl;
- nb_failed++;
delete reached_class;
e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(pos, t));
pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
@@ -338,10 +327,7 @@ void *threadSOG::doCompute() {
}
if (id_thread) {
-
-
if (--m_gc == 0) m_gc_mutex.unlock();
-
}
}
}
@@ -354,25 +340,18 @@ void *threadSOG::doCompute() {
/************ Canonised construction based on Pthread library ***********************************/
void *threadSOG::doComputeCanonized() {
int id_thread;
- int nb_it = 0, nb_failed = 0;
id_thread = m_id_thread++;
Set fire;
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;
- // cout<<bddtable<<M0<<endl;
-
MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
//#ldd_refs_push(Complete_meta_state);
MDD canonised_initial = Canonize(Complete_meta_state, 0);
//#ldd_refs_push(canonised_initial);
fire = firable_obs(Complete_meta_state);
-
-
c->m_lddstate = canonised_initial;
//m_TabMeta[m_nbmetastate]=c->m_lddstate;
//max_meta_state_size=bdd_pathcount(Complete_meta_state);
@@ -382,17 +361,12 @@ void *threadSOG::doComputeCanonized() {
m_graph->insert(c);
//m_graph->nbMarking+=bdd_pathcount(c->m_lddstate);
m_charge[0] = 1;
-
}
LDDState *reached_class;
-
do {
-
while (!m_st[id_thread].empty()) {
-
- nb_it++;
m_terminaison[id_thread] = false;
pthread_spin_lock(&m_spin_stack[id_thread]);
Pair e = m_st[id_thread].top();
@@ -466,14 +440,12 @@ void *threadSOG::doComputeCanonized() {
pthread_spin_unlock(&m_spin_stack[m_min_charge]);
m_charge[m_min_charge]++;
} else {
- nb_failed++;
m_graph->addArc();
m_graph_mutex.unlock();
e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(pos, t));
pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
delete reached_class;
-
}
if (id_thread) {
@@ -518,12 +490,12 @@ void threadSOG::computeDSOG(LDDGraph &g,uint8_t&& method){
}
for (int i = 0; i < m_nb_thread - 1; ++i) {
-
m_list_thread[i] = new std::thread(threadHandler, this,method);
if (m_list_thread[i] == nullptr) {
cout << "error: creating threads #" << i << endl;
}
}
+
switch (method) {
case 0 : doCompute();
break;
@@ -551,8 +523,10 @@ void threadSOG::computeDSOG(LDDGraph &g,uint8_t&& method){
}
void *threadSOG::threadHandler(void *context,const uint8_t& method) {
+
switch (method) {
- case 0 : return ((threadSOG *) context)->doCompute();
+ case 0:
+ return ((threadSOG *) context)->doCompute();
case 1:
return ((threadSOG *) context)->doComputeCanonized();
case 2:
@@ -583,17 +557,14 @@ void *threadSOG::doComputePOR() {
clock_gettime(CLOCK_REALTIME, &start);
// printf("*******************PARALLEL*******************\n");
m_min_charge = 0;
-
auto *c = new LDDState;
- //cout<<"Marquage initial is being built..."<<endl;
- // cout<<bddtable<<M0<<endl;
MDD Complete_meta_state{saturatePOR(m_initialMarking, fireObs, _div, _dead)};
+ cout<<"Size of obs : "<<fireObs.size()<<endl;
c->m_lddstate = Complete_meta_state;
-
- m_st[0].push(Pair(couple(c, Complete_meta_state), fireObs));
+ Set cpy=fireObs;
+ m_st[0].push(Pair(couple(c, Complete_meta_state), cpy));
m_graph->setInitialState(c);
m_graph->insert(c);
- //m_graph->nbMarking+=bdd_pathcount(c->m_lddstate);
m_charge[0] = 1;
}
@@ -616,8 +587,8 @@ void *threadSOG::doComputePOR() {
m_gc_mutex.lock();
}
}
-
- MDD Complete_meta_state{saturatePOR(get_successor(e.first.second, t), fireObs, _div, _dead)};
+ Set cpy=fireObs;
+ MDD Complete_meta_state{saturatePOR(get_successor(e.first.second, t), cpy, _div, _dead)};
/* if (id_thread==0)
{
m_gc_mutex.lock();
@@ -648,7 +619,8 @@ void *threadSOG::doComputePOR() {
m_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), fireObs));
+ 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 {
--
GitLab