diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp index 410d9d5b38dbd51487b4a3bed73c50c98e09fc69..023a9aed636d4e45b2b225781cec8c1655659a43 100644 --- a/src/CommonSOG.cpp +++ b/src/CommonSOG.cpp @@ -213,3 +213,11 @@ return ((M&cur)!=lddmc_false); //BLOCAGE } +/**************** isMarked **************/ +bool CommonSOG::is_marked(int p, const MDD& m) const { + if(0 <= p && p < m_place_proposition.size()); + return + else + return false; +} + diff --git a/src/CommonSOG.h b/src/CommonSOG.h index 8ff04f23577a3cda6a6689f4da05130090b3a513..b97e0f07a932d97df742b0404f996d23d1c25b88 100644 --- a/src/CommonSOG.h +++ b/src/CommonSOG.h @@ -2,7 +2,7 @@ #define COMMONSOG_H #include "LDDGraph.h" #include "TransSylvan.h" -#include "NewNet.h" +#include "Net.hpp" #include <stack> typedef pair<LDDState *, MDD> couple; @@ -19,7 +19,7 @@ class CommonSOG Set * getNonObservable(); unsigned int getPlacesCount(); protected: - NewNet m_net; + net m_net; int m_nbPlaces = 0; LDDGraph *m_graph; vector<TransSylvan> m_tb_relation; @@ -39,6 +39,9 @@ class CommonSOG MDD Canonize(MDD s, unsigned int level); bool Set_Div(MDD &M) const; bool Set_Bloc(MDD &M) const; + bool is_marked(int p, const MDD & m) const; + + private: }; diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp index 3c5a77cd18cacaaafc41c5963fb336c2a22d4d2f..fa065032ef75d17fe6fee02fc8af36d316c9d32c 100644 --- a/src/DistributedSOG.cpp +++ b/src/DistributedSOG.cpp @@ -25,7 +25,7 @@ using namespace sylvan; /**************************************************/ -DistributedSOG::DistributedSOG(const NewNet &R, int BOUND,bool init) +DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init) { diff --git a/src/DistributedSOG.h b/src/DistributedSOG.h index d608110c62b977eabb3e65b0572268e89cff5b48..f10880f5f36e5d7dfb87a169226d3af33dfd5f0b 100644 --- a/src/DistributedSOG.h +++ b/src/DistributedSOG.h @@ -3,7 +3,7 @@ // #include "RdPBDD.h" #include <stack> #include <vector> -#include "NewNet.h" +#include "Net.hpp" // #include "MDD.h" //#include "MDGraph.h" //#include "bvec.h" @@ -46,7 +46,7 @@ extern int n_tasks, task_id; // typedef vector<Trans> vec_trans; class DistributedSOG : public CommonSOG{ public: - DistributedSOG(const NewNet &, int BOUND = 32, bool init = false); + DistributedSOG(const net &, int BOUND = 32, bool init = false); void buildFromNet(int index); void computeDSOG(LDDGraph &g); void BuildInitialState(LDDState *m_state, MDD mdd); diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp index 8ca3114fbe84ef951d22f668db67ba40b54a6802..b9126a31d3c888cca911dcf46a1df1d81ef4e96f 100644 --- a/src/HybridSOG.cpp +++ b/src/HybridSOG.cpp @@ -50,7 +50,7 @@ using namespace sylvan; } */ -HybridSOG::HybridSOG(const NewNet &R, int BOUND,bool init) +HybridSOG::HybridSOG(const net &R, int BOUND,bool init) { diff --git a/src/HybridSOG.h b/src/HybridSOG.h index f480981e0704aaae9f072d1c5f75b505c63b322b..6511d11790f765010a9352a70bb5943db7bd32a2 100644 --- a/src/HybridSOG.h +++ b/src/HybridSOG.h @@ -3,7 +3,7 @@ #include <stack> #include <vector> -#include "NewNet.h" +#include "Net.hpp" // #include "MDD.h" //#include "MDGraph.h" //#include "bvec.h" @@ -47,7 +47,7 @@ typedef stack<MSG> pile_msg; class HybridSOG : public CommonSOG { public: - HybridSOG(const NewNet &, int BOUND = 32, bool init = false); + HybridSOG(const net &, int BOUND = 32, bool init = false); void buildFromNet(int index); /// principal functions to construct the SOG void computeDSOG(LDDGraph &g); diff --git a/src/LDDState.cpp b/src/LDDState.cpp index a6f372b3af40b1a4f516c2de908a5cbc5aa4659e..afd70ba1dfd33372f411d1c5cae9bd5b9015cf94 100644 --- a/src/LDDState.cpp +++ b/src/LDDState.cpp @@ -28,3 +28,11 @@ void LDDState::setVirtual() { vector<pair<LDDState*, int>>* LDDState::getSuccessors() { return &Successors; } + +void LDDState::setMarked() { + isMarked()=true; +} + +bool LDDState::isMarked() { + return m_marked; +} diff --git a/src/LDDState.h b/src/LDDState.h index 4337d85aa02a692107d5cc4382a10c31d06156fd..4447b7fe97a03499b6e4b7a24d251c49b5318502 100755 --- a/src/LDDState.h +++ b/src/LDDState.h @@ -12,6 +12,7 @@ class LDDState { LDDState() { m_boucle = m_blocage = m_visited = false; m_virtual = false; + m_marked = false; } virtual ~LDDState(); Set firable; @@ -33,6 +34,8 @@ class LDDState { bool isDiv() {return m_boucle;} void setDeadLock(bool de) {m_blocage=de;} bool isDeadLock() {return m_blocage;} + bool isMarked(); + void setMarked(); protected: private: bool m_virtual = false; diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp index 917a54ce5d2229728b79551c008eb11cc57ae5b4..665f8c753691b4be1ab574646d6c802c8e39d8aa 100644 --- a/src/threadSOG.cpp +++ b/src/threadSOG.cpp @@ -26,7 +26,7 @@ void write_to_dot(const char *ch,MDD m) /*************************************************/ -threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool init) +threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool init) { m_nb_thread=nbThread; if (uselace) { diff --git a/src/threadSOG.h b/src/threadSOG.h index f0880740447ef681031bf03b9f575a79bd34e5c2..fc495b298d77c7ae534137bf5b627929ea37f1fb 100644 --- a/src/threadSOG.h +++ b/src/threadSOG.h @@ -3,7 +3,7 @@ // #include "RdPBDD.h" #include <stack> #include <vector> -#include "NewNet.h" +#include "Net.hpp" // #include "MDD.h" //#include "MDGraph.h" //#include "bvec.h" @@ -23,7 +23,7 @@ extern unsigned int nb_th; class threadSOG : public CommonSOG{ public: - threadSOG(const NewNet &, int BOUND = 32, int nbThread=2,bool uselace=false,bool init = false); + threadSOG(const net &, int BOUND = 32, int nbThread=2,bool uselace=false,bool init = false); void buildFromNet(int index); void computeDSOG(LDDGraph &g,bool canonised); void computeSeqSOG(LDDGraph &g);