diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index d3e397eeee434c5c082c97023fade5805eee958f..c0267d9a73b761a7c8aa9fd530a3034d1d62fac5 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -2,10 +2,11 @@
#include "SylvanWrapper.h"
#include "CommonSOG.h"
-CommonSOG::CommonSOG() =default;
-CommonSOG::~CommonSOG() =default;
+CommonSOG::CommonSOG() = default;
-LDDGraph *CommonSOG::getGraph() {
+CommonSOG::~CommonSOG() = default;
+
+LDDGraph *CommonSOG::getGraph() {
return m_graph;
}
@@ -16,7 +17,8 @@ MDD CommonSOG::Accessible_epsilon(MDD From) {
M1 = M2;
for (auto i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
//fireTransition
- MDD succ = SylvanWrapper::lddmc_firing_mono(M2, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ MDD succ = SylvanWrapper::lddmc_firing_mono(M2, m_tb_relation[(*i)].getMinus(),
+ m_tb_relation[(*i)].getPlus());
M2 = SylvanWrapper::lddmc_union_mono(M2, succ);
}
} while (M1 != M2);
@@ -26,7 +28,7 @@ MDD CommonSOG::Accessible_epsilon(MDD From) {
// Return the set of firable observable transitions from an agregate
Set CommonSOG::firable_obs(MDD State) {
Set res;
- for (auto i : m_observable) {
+ for (auto i: m_observable) {
MDD succ = SylvanWrapper::lddmc_firing_mono(State, m_tb_relation[i].getMinus(), m_tb_relation[i].getPlus());
if (succ != lddmc_false) {
res.insert(i);
@@ -35,14 +37,14 @@ Set CommonSOG::firable_obs(MDD State) {
return res;
}
-MDD CommonSOG::get_successor(const MDD& From, const int& t) {
+MDD CommonSOG::get_successor(const MDD &From, const int &t) {
return SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(t)].getMinus(), m_tb_relation[(t)].getPlus());
}
MDD CommonSOG::ImageForward(MDD From) {
MDD Res = lddmc_false;
- for (auto i : m_nonObservable) {
+ for (auto i: m_nonObservable) {
MDD succ = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[i].getMinus(), m_tb_relation[i].getPlus());
Res = SylvanWrapper::lddmc_union_mono(Res, succ);
}
@@ -126,17 +128,17 @@ bool CommonSOG::Set_Div(MDD &M) const {
if (m_nonObservable.empty()) {
return false;
}
- MDD Reached, From {M};
+ MDD Reached, From{M};
do {
Reached = lddmc_false;
- for (auto i : m_nonObservable )
- {
- MDD To = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(i)].getMinus(), m_tb_relation[(i)].getPlus());
+ for (auto i: m_nonObservable) {
+ MDD To = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(i)].getMinus(),
+ m_tb_relation[(i)].getPlus());
Reached = SylvanWrapper::lddmc_union_mono(Reached, To);
}
if (Reached == From) {
- return true;
+ return true;
}
From = Reached;
} while (Reached != lddmc_false);
@@ -147,7 +149,7 @@ bool CommonSOG::Set_Div(MDD &M) const {
bool CommonSOG::Set_Bloc(MDD &M) const {
MDD cur = lddmc_true;
- for (auto i : m_tb_relation) {
+ for (auto i: m_tb_relation) {
cur = cur & (i.getMinus());
}
return ((M & cur) != lddmc_false);
@@ -155,7 +157,6 @@ bool CommonSOG::Set_Bloc(MDD &M) const {
}
-
LDDGraph *CommonSOG::m_graph;
@@ -164,14 +165,14 @@ LDDGraph *CommonSOG::m_graph;
}*/
//string_view CommonSOG::getTransition(int pos) {
- // cout<<"yes it is : "<<m_transitions.at(pos).name<<endl;
- // cout<<"Ok "<<m_graph->getTransition(pos)<<endl;
+// cout<<"yes it is : "<<m_transitions.at(pos).name<<endl;
+// cout<<"Ok "<<m_graph->getTransition(pos)<<endl;
// return string_view {m_transitions.at(pos).name};
//}
string_view CommonSOG::getPlace(int pos) {
- return string_view {m_graph->getPlace(pos)};
+ return string_view{m_graph->getPlace(pos)};
}
void CommonSOG::initializeLDD() {
@@ -249,26 +250,34 @@ void CommonSOG::loadNetFromFile() {
delete[] postc;
}
-void CommonSOG::AddConflict(const MDD &S, const int &transition,Set &le) {
- // if ()
- MDD img= get_successor(S,transition);
- if (img!=lddmc_true && img!=lddmc_false) {
- for (auto i=0; i<m_transitions.size();i++) {
- if (i!=transition) {
- auto interPre = [this](const int & t1,const int &t2)-> bool {
- auto & preT1=m_transitions[t1].pre;
- auto & preT2=m_transitions[t2].pre;
- bool found=false;
- for (auto elt : preT1);
- return true;
- };
+void CommonSOG::AddConflict(const MDD &S, const int &transition, Set &le) {
+ auto haveCommonPre = [&](vector<pair<int, int>> &preT1, vector<pair<int, int>> &preT2) -> bool {
+ bool found = false;
+ for (auto &elt1: preT1) {
+ for (auto &elt2: preT2) {
+ if (std::get<0>(elt1) == std::get<0>(elt2)) return true;
}
}
- }
-
+ return false;
+ };
+ MDD img = get_successor(S, transition);
+ if (img != lddmc_true && img != lddmc_false) {
+ for (auto i = 0; i < m_transitions.size(); i++) {
+ if (i != transition) {
+ auto &preT1 = m_transitions[i].pre;
+ auto &preT2 = m_transitions[transition].pre;
+ if (!haveCommonPre(preT1, preT2)) ample.insert(i);
+ }
+ }
+ } else {
+ for (auto i = 0; i < m_transitions.size(); i++) {
+ if (i != transition) {
+ auto &preT1 = m_transitions[i].post;
+ auto &preT2 = m_transitions[transition].pre;
+ if (!haveCommonPre(preT1, preT2)) ample.insert(i);
+ }
+ }
+ }
}
-bool CommonSOG::isFirable(const int &transition) {
-
-}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 5118d65c98009d383aa1e64983d24509a0013cd1..39fee9d0e246f834de07a1afce043144c2df88ad 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -60,9 +60,12 @@ class CommonSOG
atomic<uint8_t> m_gc;
volatile bool m_finish=false;
// Functions for POR
+ /*
+ * Determine ample set in S for transition
+ */
void AddConflict(const MDD& S,const int &transition,Set& ample);
private:
- bool isFirable(const int &transition);
+
};
#endif // COMMONSOG_H
diff --git a/src/NewNet.h b/src/NewNet.h
index d394cc8e3754fe2326c6a6f7821ebdc18596404a..9393f8a8d88d938d6ef0c0f46a01dc2c3ebbaae5 100644
--- a/src/NewNet.h
+++ b/src/NewNet.h
@@ -16,7 +16,7 @@ class Node {
public:
Node(){};
~Node(){};
- vector<pair<int, int> > pre, post, inhibitor, preAuto, postAuto;
+ vector<pair<int, int>> pre, post, inhibitor, preAuto, postAuto;
vector<int> reset;
void addPre(int, int);
void addPost(int, int);