From cdc55b72c82590dcc7e760364cce1872c39daa38 Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Thu, 2 May 2019 01:26:43 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/SogKripke.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?= =?UTF-8?q?=20=20=20src/SogKripkeIterator.cpp=20=09modifi=C3=A9=C2=A0:=20?= =?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeIterator.h=20=09modifi?= =?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeState.cpp?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/SogKripke.cpp | 8 ++++++-- src/SogKripkeIterator.cpp | 4 ++-- src/SogKripkeIterator.h | 5 +++-- src/SogKripkeState.cpp | 2 +- 4 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp index 69a420d..f86562d 100644 --- a/src/SogKripke.cpp +++ b/src/SogKripke.cpp @@ -49,8 +49,12 @@ std::string SogKripke::format_state(const spot::state* s) const SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const { auto ss = static_cast<const SogKripkeState*>(s); - bdd b=bddfalse; - return new SogKripkeIterator(ss->getLDDState());//,b);//s state_condition(ss)); + ////////////////////////////////////////////// + // Must be changed + // State condition ???? + /////////////////////// + bdd b=bddtrue; + return new SogKripkeIterator(ss->getLDDState(),b);//,b);//s state_condition(ss)); } /* MDD state_condition(const spot::state* s) const override diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp index 949abe1..9b2b679 100644 --- a/src/SogKripkeIterator.cpp +++ b/src/SogKripkeIterator.cpp @@ -1,10 +1,10 @@ -#include <spot/twa/twa.hh> +#include <spot/kripke/kripke.hh> #include "LDDGraph.h" #include "SogKripkeState.h" #include "SogKripkeIterator.h" -SogKripkeIterator::SogKripkeIterator(const LDDState* lddstate):m_lddstate(lddstate) +SogKripkeIterator::SogKripkeIterator(const LDDState* lddstate, bdd cond):kripke_succ_iterator(cond),m_lddstate(lddstate) { //vector<pair<LDDState*, int>> m_lddstate->setDiv(true); diff --git a/src/SogKripkeIterator.h b/src/SogKripkeIterator.h index 33fdf33..435c240 100644 --- a/src/SogKripkeIterator.h +++ b/src/SogKripkeIterator.h @@ -2,14 +2,15 @@ #define SOGKRIPKEITERATOR_H_INCLUDED #include "SogKripkeState.h" #include "LDDGraph.h" +#include <spot/kripke/kripke.hh> // Iterator for a SOG graph -class SogKripkeIterator : public spot::twa_succ_iterator +class SogKripkeIterator : public spot::kripke_succ_iterator { public: static LDDGraph * m_graph; static spot::bdd_dict_ptr* m_dict_ptr; - SogKripkeIterator(const LDDState *lddstate); + SogKripkeIterator(const LDDState *lddstate,bdd cond); virtual ~SogKripkeIterator(); bool first() override; bool next() override; diff --git a/src/SogKripkeState.cpp b/src/SogKripkeState.cpp index d47cc4a..b1da9d3 100644 --- a/src/SogKripkeState.cpp +++ b/src/SogKripkeState.cpp @@ -1,4 +1,4 @@ -#include <spot/twa/twa.hh> +#include <spot/kripke/kripke.hh> #include "LDDState.h" #include "SogKripkeState.h" -- GitLab