diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp index ddfe47367991fcd209557b80cdf8cd0c1f59a131..1e989b3a66a766f67f43810fdfa1442518310f8d 100644 --- a/src/LDDGraph.cpp +++ b/src/LDDGraph.cpp @@ -49,7 +49,7 @@ LDDState * LDDGraph::findSHA(unsigned char* c) /*----------------------insert() ------------*/ void LDDGraph::insert(LDDState *c) { - c->m_visited=false; + this->m_GONodes.push_back(c); m_nbStates++; } @@ -58,7 +58,7 @@ void LDDGraph::insert(LDDState *c) /*----------------------insert() ------------*/ void LDDGraph::insertSHA(LDDState *c) { - c->m_visited=false; + c->setVirtual(); this->m_GONodes.push_back(c); @@ -129,11 +129,11 @@ void LDDGraph::InitVisit(LDDState * S,size_t nb) { if(nb<=m_nbStates) { - S->m_visited=false; + for(LDDEdges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++) { - if((*i).first->m_visited==true) + if((*i).first->isVisited()==true) { nb++; InitVisit((*i).first,nb); @@ -150,7 +150,7 @@ void LDDGraph::printGraph(LDDState *s,size_t &nb) { cout<<"\nSTATE NUMBER "<<nb<<" sha : "<<s->getSHAValue()<<" LDD v :"<<s->getLDDValue()<<endl; - s->m_visited=true; + s->setVisited(); /*printsuccessors(s); getchar(); printpredecessors(s); @@ -158,7 +158,7 @@ void LDDGraph::printGraph(LDDState *s,size_t &nb) LDDEdges::const_iterator i; for(i=s->Successors.begin();!(i==s->Successors.end());i++) { - if((*i).first->m_visited==false) + if((*i).first->isVisited()==false) { nb++; printGraph((*i).first, nb); diff --git a/src/LDDState.h b/src/LDDState.h index 7f444c69a45f3db24092850f922aa2cd9c9262ee..6d0c3e9c53516f87116fb5d28735eca2eac71bf1 100755 --- a/src/LDDState.h +++ b/src/LDDState.h @@ -29,7 +29,7 @@ class LDDState { unsigned char* getSHAValue(); bool m_boucle; bool m_blocage; - bool m_visited; + bool isVirtual(); void setVirtual(); @@ -37,12 +37,15 @@ class LDDState { bool isDiv() {return m_boucle;} void setDeadLock(bool de) {m_blocage=de;} bool isDeadLock() {return m_blocage;} + void setVisited() {m_visited=true;} + bool isVisited() {return m_visited;} vector<int> getMarkedPlaces(set<int>& lplacesAP); vector<int> getUnmarkedPlaces(set<int>& lplacesAP); protected: private: bool m_virtual = false; + bool m_visited=false; }; diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index cb13980bb75f2d16e71d17b0dc6736a526afce17..2cf50d13e749134ae4756e719fff95f5b0880966 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -210,10 +210,13 @@ LDDState * ModelCheckLace::buildInitialMetaState() return c; } -LDDState * ModelCheckLace::buildSucc(LDDState *agregate) +void ModelCheckLace::buildSucc(LDDState *agregate) { - LDDState *trmp=nullptr; - return trmp; + if (!agregate->isVisited()) { + // It's first time to visit agregate, then we have to build its successors + + + } } diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h index 4c1e1ff1d3c983b2a59d274d723f240344dfa82c..1dfa14c26caf278b9c611d325ee6b7b7c15d0db4 100644 --- a/src/ModelCheckLace.h +++ b/src/ModelCheckLace.h @@ -7,7 +7,7 @@ public: LDDState * buildInitialMetaState(); string getTransition(int pos); string getPlace(int pos); - LDDState * buildSucc(LDDState *agregate); + void buildSucc(LDDState *agregate); private: int m_nb_thread; MDD m_initalMarking;