From 27a4efa88a38538ad7ff9f40b05e4a96504b1b89 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Mon, 27 May 2019 23:31:18 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/LDDGraph.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/LDDState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20=20src/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/ModelCheckLace.h?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/LDDGraph.cpp | 12 ++++++------
src/LDDState.h | 5 ++++-
src/ModelCheckLace.cpp | 9 ++++++---
src/ModelCheckLace.h | 2 +-
4 files changed, 17 insertions(+), 11 deletions(-)
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index ddfe473..1e989b3 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 7f444c6..6d0c3e9 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 cb13980..2cf50d1 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 4c1e1ff..1dfa14c 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;
--
GitLab