diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..d6ae60ab5236533cd2950b48c15820dae38c6000
--- /dev/null
+++ b/src/SogKripkeIteratorTh.cpp
@@ -0,0 +1,76 @@
+#include <spot/kripke/kripke.hh>
+#include "LDDGraph.h"
+#include "SogKripkeStateTh.h"
+#include "SogKripkeIteratorTh.h"
+
+
+SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
+{
+
+ m_lddstate->setDiv(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->isDiv()) {
+ m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
+ }
+
+}
+bool SogKripkeIteratorTh::first() {
+
+ // cout<<"entering "<<__func__<<endl;
+ m_current_edge=0;
+ //cout<<"exciting "<<__func__<<endl;
+ return m_lsucc.size()!=0;
+
+}
+
+bool SogKripkeIteratorTh::next() {
+ //cout<<"entering "<<__func__<<endl;
+ m_current_edge++;
+ return m_current_edge<m_lsucc.size();
+
+}
+
+bool SogKripkeIteratorTh::done() const {
+ //cout<<"entring /excit"<<__func__<<endl;
+ return m_current_edge==m_lsucc.size();
+
+}
+
+SogKripkeStateTh* SogKripkeIteratorTh::dst() const
+ {
+ //cout<<"enter/excit "<<__func__<<endl;
+ return new SogKripkeStateTh(m_lsucc.at(m_current_edge).first);
+ }
+
+bdd SogKripkeIteratorTh::cond() const {
+ //cout<<"entering "<<__func__<<endl;
+ if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+
+ string name=m_builder->getTransition(m_lsucc.at(m_current_edge).second);
+ //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
+
+ spot::bdd_dict *p=m_dict_ptr->get();
+ 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();
+}
+
+/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
+ //cout<<"Iterator acc()\n";
+ return 0U;
+}*/
+SogKripkeIteratorTh::~SogKripkeIteratorTh()
+{
+ //dtor
+}
+
+static ModelCheckerTh * SogKripkeIteratorTh::m_builder;
+static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..b3624d6be8d978eb81bb81169c8012e230bbafde
--- /dev/null
+++ b/src/SogKripkeIteratorTh.h
@@ -0,0 +1,39 @@
+#ifndef SOGKRIPKEITERATORTH_H_INCLUDED
+#define SOGKRIPKEITERATORTH_H_INCLUDED
+#include "SogKripkeStateTh.h"
+#include "ModelCheckerTh.h"
+#include <spot/kripke/kripke.hh>
+// Iterator for a SOG graph
+class SogKripkeIteratorTh : public spot::kripke_succ_iterator
+{
+public:
+
+ static ModelCheckerTh * m_builder;
+ static spot::bdd_dict_ptr* m_dict_ptr;
+ // sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
+ SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd);
+ virtual ~SogKripkeIteratorTh();
+ bool first() override;
+ bool next() override;
+ bool done() const override;
+ SogKripkeStateTh* dst() const override;
+ bdd cond() const override final;
+
+ SogKripkeStateTh* current_state() const;
+
+ bdd current_condition() const;
+
+ int current_transition() const;
+
+ bdd current_acceptance_conditions() const;
+
+ std::string format_transition() const;
+
+private:
+ LDDState * m_lddstate;
+ vector<pair<LDDState*, int>> m_lsucc;
+ unsigned int m_current_edge=0;
+};
+
+
+#endif // SOGKRIPKEITERATOR_H_INCLUDED
diff --git a/src/SogKripkeStateTh.cpp b/src/SogKripkeStateTh.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..76c38845a939bbf61a9c9ba4c2aca9f92add023a
--- /dev/null
+++ b/src/SogKripkeStateTh.cpp
@@ -0,0 +1,11 @@
+#include <spot/kripke/kripke.hh>
+#include "LDDState.h"
+#include "SogKripkeStateTh.h"
+
+
+SogKripkeStateTh::~SogKripkeStateTh()
+{
+ //dtor
+}
+
+static ModelCheckerTh * SogKripkeStateTh::m_builder;
diff --git a/src/SogKripkeStateTh.h b/src/SogKripkeStateTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..48d64ff99e8eab4d4981030c3548ca76976c81ef
--- /dev/null
+++ b/src/SogKripkeStateTh.h
@@ -0,0 +1,46 @@
+#ifndef SOGKRIPKESTATETH_H_INCLUDED
+#define SOGKRIPKESTATETH_H_INCLUDED
+
+
+#include "LDDState.h"
+#include "ModelCheckerTh.h"
+
+class SogKripkeStateTh : public spot::state
+{
+public:
+ static ModelCheckerTh * m_builder;
+ SogKripkeStateTh(LDDState *st):m_state(st) {
+ m_builder->buildSucc(st);
+ };
+ virtual ~SogKripkeStateTh();
+
+ SogKripkeStateTh* clone() const override
+ {
+ return new SogKripkeStateTh(m_state);
+ }
+ size_t hash() const override
+ {
+ return m_state->getLDDValue();
+ }
+
+ int compare(const spot::state* other) const override
+ {
+ auto o = static_cast<const SogKripkeStateTh*>(other);
+ size_t oh = o->hash();
+ size_t h = hash();
+ if (h < oh)
+ return -1;
+ else
+ return h > oh;
+ }
+ LDDState* getLDDState() {
+ return m_state;
+ }
+protected:
+
+private:
+ LDDState *m_state;
+};
+
+
+#endif // SOGKRIPKESTATE_H_INCLUDED
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..0e5f86d8b685cb91688e6bc79166b462147b22f3
--- /dev/null
+++ b/src/SogKripkeTh.cpp
@@ -0,0 +1,86 @@
+#include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/kripke/kripke.hh>
+#include <spot/twa/bdddict.hh>
+
+
+#include "SogKripkeIteratorTh.h"
+#include "SogKripkeStateTh.h"
+
+#include "SogKripkeTh.h"
+#include <map>
+using namespace spot;
+SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckerTh *builder): spot::kripke(dict_ptr),m_builder(builder)
+{
+ SogKripkeIteratorTh::m_builder=builder;
+ SogKripkeStateTh::m_builder=builder;
+ SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
+ //cout<<__func__<<endl;
+}
+
+SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
+
+ for (auto it=l_transap.begin();it!=l_transap.end();it++) {
+ register_ap(*it);
+ }
+ for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
+ register_ap(*it);
+
+}
+
+
+state* SogKripkeTh::get_init_state() const {
+ // cout<<__func__<<endl;
+ return new SogKripkeStateTh(m_builder->buildInitialMetaState());//new SpotSogState();
+
+}
+// Allows to print state label representing its id
+std::string SogKripkeTh::format_state(const spot::state* s) const
+ {
+ //cout<<__func__<<endl;
+ auto ss = static_cast<const SogKripkeStateTh*>(s);
+ std::ostringstream out;
+ out << "( " << ss->getLDDState()->getLDDValue() << ")";
+ // cout << " ( " << ss->getLDDState()->getLDDValue() << ")";
+ return out.str();
+ }
+
+SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
+ // cout<<__func__<<endl;
+
+ auto ss = static_cast<const SogKripkeStateTh*>(s);
+ //////////////////////////////////////////////
+
+ return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
+}
+
+bdd SogKripkeTh::state_condition(const spot::state* s) const
+ {
+
+ auto ss = static_cast<const SogKripkeStateTh*>(s);
+ vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
+
+
+ bdd result=bddtrue;
+ // Marked places
+ for (auto it=marked_place.begin();it!=marked_place.end();it++) {
+ string name=m_builder->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+ vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_builder->getPlaceProposition());
+ for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
+ string name=m_builder->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=!bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+
+ return result;
+ }
+
+
+SogKripkeTh::~SogKripkeTh()
+{
+ //dtor
+}
+
diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..4f4a114286a9b024fefcb7f5b697f9344b7e6b06
--- /dev/null
+++ b/src/SogKripkeTh.h
@@ -0,0 +1,34 @@
+#ifndef SOGKRIPKETH_H_INCLUDED
+#define SOGKRIPKETH_H_INCLUDED
+#include "LDDGraph.h"
+#include "SogKripkeIteratorTh.h"
+#include <spot/kripke/kripke.hh>
+#include <LDDGraph.h>
+#include <NewNet.h>
+
+
+class SogKripkeTh: public spot::kripke {
+ public:
+
+ SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder);
+ SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap);
+ virtual ~SogKripkeTh();
+ spot::state* get_init_state() const;
+ SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
+ std::string format_state(const spot::state* s) const override;
+ bdd state_condition(const spot::state* s) const override;
+
+ /// \brief Get the graph associated to the automaton.
+ /* const LDDGraph& get_graph() const {
+ return *m_sog;
+ }*/
+ ModelCheckerTh *m_builder;
+
+ protected:
+
+ private:
+ std::map<int, int> place_prop;
+ //LDDGraph* m_sog;
+};
+
+#endif // SOGKRIPKE_H_INCLUDED