From f00f99621c0afdcc6cbb432b18671e08c7fbd943 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Fri, 14 Jun 2019 15:59:38 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/SogKripkeIteratorTh.cpp=20=09modifi=C3=A9=C2=A0:=20=20?=
=?UTF-8?q?=20=20=20=20=20=20=20src/SogKripkeIteratorTh.h=20=09modifi?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeTh.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/SogKripkeIteratorTh.cpp | 1 +
src/SogKripkeIteratorTh.h | 1 +
src/SogKripkeTh.cpp | 4 +++-
3 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 3bde48f..b36577a 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -74,3 +74,4 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
static LDDState SogKripkeIteratorTh::m_deadlock;
+static LDDState SogKripkeIteratorTh::m_div;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
index 774cbd5..938803d 100644
--- a/src/SogKripkeIteratorTh.h
+++ b/src/SogKripkeIteratorTh.h
@@ -8,6 +8,7 @@ class SogKripkeIteratorTh : public spot::kripke_succ_iterator
{
public:
static LDDState m_deadlock;
+ static LDDState m_div;
static ModelCheckBaseMT * 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/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index 4f2e563..ab4d48a 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -15,7 +15,9 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder)
SogKripkeIteratorTh::m_builder=builder;
SogKripkeStateTh::m_builder=builder;
SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
-
+ SogKripkeIteratorTh::m_deadlock.setLDDValue(1);
+ SogKripkeIteratorTh::m_div.setLDDValue(0);
+ SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));
}
SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
--
GitLab