modifié : src/LDDGraph.cpp

	modifié :         src/LDDState.h
	modifié :         src/ModelCheckLace.cpp
	modifié :         src/ModelCheckLace.h

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);

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;
 
 };
 

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
+
+
+   }
 }
 
 

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;