From 3aa5ddaa4375d05ca442888bdf6a5b501bcc0017 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 6 Jun 2019 02:17:48 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/LDDState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
=?UTF-8?q?=20=20src/ModelCheckerTh.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/SogKripkeIteratorOTF.cpp=20=09modifi?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeIteratorOT?=
=?UTF-8?q?F.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogK?=
=?UTF-8?q?ripkeIteratorTh.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/SogKripkeIteratorTh.h=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeOTF.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/LDDState.h | 4 ++--
src/ModelCheckerTh.cpp | 1 -
src/SogKripkeIteratorOTF.cpp | 1 +
src/SogKripkeIteratorOTF.h | 2 +-
src/SogKripkeIteratorTh.cpp | 12 ++++++------
src/SogKripkeIteratorTh.h | 2 +-
src/SogKripkeOTF.cpp | 1 +
7 files changed, 12 insertions(+), 11 deletions(-)
diff --git a/src/LDDState.h b/src/LDDState.h
index 6d0c3e9..074a253 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -24,10 +24,10 @@ class LDDState {
pair<LDDState*, int> LastEdge;
void setLDDValue(MDD m);
MDD getLDDValue();
- MDD m_lddstate;
+ MDD m_lddstate=0;
unsigned char m_SHA2[81];
unsigned char* getSHAValue();
- bool m_boucle;
+ bool m_boucle=false;
bool m_blocage;
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index bcffda8..159855c 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -245,5 +245,4 @@ ModelCheckerTh::~ModelCheckerTh() {
{
pthread_join(m_list_thread[i], NULL);
}
- cout<<"Destructor "<<endl;
}
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
index 2790ac5..e2e73dc 100644
--- a/src/SogKripkeIteratorOTF.cpp
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -74,3 +74,4 @@ SogKripkeIteratorOTF::~SogKripkeIteratorOTF()
static ModelCheckLace * SogKripkeIteratorOTF::m_builder;
static spot::bdd_dict_ptr* SogKripkeIteratorOTF::m_dict_ptr;
+static LDDState SogKripkeIteratorOTF::m_deadlock;
diff --git a/src/SogKripkeIteratorOTF.h b/src/SogKripkeIteratorOTF.h
index 7a3ac82..717afbf 100644
--- a/src/SogKripkeIteratorOTF.h
+++ b/src/SogKripkeIteratorOTF.h
@@ -7,7 +7,7 @@
class SogKripkeIteratorOTF : public spot::kripke_succ_iterator
{
public:
-
+ static LDDState m_deadlock;
static ModelCheckLace * m_builder;
static spot::bdd_dict_ptr* m_dict_ptr;
// sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index d6ae60a..f28f324 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -7,13 +7,14 @@
SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
{
- m_lddstate->setDiv(true);
+ //m_lddstate->setDiv(true);
+ //if (m_lddstate->getLDDValue()) m_lddstate->setDeadLock(true);
for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
}
- /* if (lddstate->isDeadLock()) {
- m_lsucc.push_back(pair(,-1));
- }*/
+ if (lddstate->isDeadLock()) {
+ m_lsucc.push_back(pair<LDDState*,int>(&m_deadlock,-1));
+ }
if (lddstate->isDiv()) {
m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
}
@@ -58,8 +59,6 @@ bdd SogKripkeIteratorTh::cond() const {
spot::formula f=spot::formula::ap(name);
bdd result=bdd_ithvar((p->var_map.find(f))->second);
- //cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n";*/
- //cout<<"exciting "<<__func__<<endl;
return result & spot::kripke_succ_iterator::cond();
}
@@ -74,3 +73,4 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
static ModelCheckerTh * SogKripkeIteratorTh::m_builder;
static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
+static LDDState SogKripkeIteratorTh::m_deadlock;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
index b3624d6..1a8adc8 100644
--- a/src/SogKripkeIteratorTh.h
+++ b/src/SogKripkeIteratorTh.h
@@ -7,7 +7,7 @@
class SogKripkeIteratorTh : public spot::kripke_succ_iterator
{
public:
-
+ static LDDState m_deadlock;
static ModelCheckerTh * m_builder;
static spot::bdd_dict_ptr* m_dict_ptr;
// sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index 13037d5..215b455 100644
--- a/src/SogKripkeOTF.cpp
+++ b/src/SogKripkeOTF.cpp
@@ -15,6 +15,7 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder)
SogKripkeIteratorOTF::m_builder=builder;
SogKripkeStateOTF::m_builder=builder;
SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
+
//cout<<__func__<<endl;
}
--
GitLab