diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp index 69a420d77f22e5cad90a886a9f68bf135a1dbdf5..f86562dd1b76d8b8e22742d72c6f293fec09749c 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 949abe1b4de92194290ff4dd24eed20af615cb5b..9b2b6797b9a1288d8ab95ce66ab7a937191eb7d9 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 33fdf33a5b260b6446a74d3e55ee3c78cd26e615..435c240e64f51eb771de13221b2d94a05ce3795f 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 d47cc4a4161ca353b3e086e064aad531e8b07542..b1da9d314fb18111d6892d8a8fff1478c8cbdf56 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"