diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d4c956ecdb8c76a308491ad9b6ef439a33e98c89..8f392a2ea10a9717601a9ae56db6cd6983ad2d9a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -62,12 +62,6 @@ add_executable(hybrid-sog main.cpp
ModelCheckBaseMT.h
ModelCheckLace.cpp
ModelCheckLace.h
- SogKripkeStateOTF.cpp
- SogKripkeStateOTF.h
- SogKripkeIteratorOTF.cpp
- SogKripkeIteratorOTF.h
- SogKripkeOTF.cpp
- SogKripkeOTF.h
SogKripkeTh.cpp
SogKripkeTh.h
SogKripkeStateTh.cpp
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
deleted file mode 100644
index e2e73dc50c9ad663841a0764b5dc4d4d5463e54a..0000000000000000000000000000000000000000
--- a/src/SogKripkeIteratorOTF.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-#include <spot/kripke/kripke.hh>
-#include "LDDGraph.h"
-#include "SogKripkeStateOTF.h"
-#include "SogKripkeIteratorOTF.h"
-
-
-SogKripkeIteratorOTF::SogKripkeIteratorOTF(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 SogKripkeIteratorOTF::first() {
-
- // cout<<"entering "<<__func__<<endl;
- m_current_edge=0;
- //cout<<"exciting "<<__func__<<endl;
- return m_lsucc.size()!=0;
-
-}
-
-bool SogKripkeIteratorOTF::next() {
- //cout<<"entering "<<__func__<<endl;
- m_current_edge++;
- return m_current_edge<m_lsucc.size();
-
-}
-
-bool SogKripkeIteratorOTF::done() const {
- //cout<<"entring /excit"<<__func__<<endl;
- return m_current_edge==m_lsucc.size();
-
-}
-
-SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
- {
- //cout<<"enter/excit "<<__func__<<endl;
- return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
- }
-
-bdd SogKripkeIteratorOTF::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;
-}*/
-SogKripkeIteratorOTF::~SogKripkeIteratorOTF()
-{
- //dtor
-}
-
-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
deleted file mode 100644
index 717afbf3d42aaa0800b77e7b90f5f0dd839381eb..0000000000000000000000000000000000000000
--- a/src/SogKripkeIteratorOTF.h
+++ /dev/null
@@ -1,39 +0,0 @@
-#ifndef SOGKRIPKEITERATOROTF_H_INCLUDED
-#define SOGKRIPKEITERATOROTF_H_INCLUDED
-#include "SogKripkeStateOTF.h"
-#include "ModelCheckLace.h"
-#include <spot/kripke/kripke.hh>
-// Iterator for a SOG graph
-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);
- SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd);
- virtual ~SogKripkeIteratorOTF();
- bool first() override;
- bool next() override;
- bool done() const override;
- SogKripkeStateOTF* dst() const override;
- bdd cond() const override final;
-
- SogKripkeStateOTF* 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/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
deleted file mode 100644
index 215b455210cc9c581af731542f9ab5cae76336b9..0000000000000000000000000000000000000000
--- a/src/SogKripkeOTF.cpp
+++ /dev/null
@@ -1,92 +0,0 @@
-#include <spot/twaalgos/dot.hh>
-#include <spot/twaalgos/hoa.hh>
-#include <spot/kripke/kripke.hh>
-#include <spot/twa/bdddict.hh>
-
-
-#include "SogKripkeIteratorOTF.h"
-#include "SogKripkeStateOTF.h"
-
-#include "SogKripkeOTF.h"
-#include <map>
-using namespace spot;
-SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder): spot::kripke(dict_ptr),m_builder(builder)
-{
- SogKripkeIteratorOTF::m_builder=builder;
- SogKripkeStateOTF::m_builder=builder;
- SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
-
- //cout<<__func__<<endl;
-}
-
-SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeOTF(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* SogKripkeOTF::get_init_state() const
-{
- // cout<<__func__<<endl;
- return new SogKripkeStateOTF(m_builder->buildInitialMetaState());//new SpotSogState();
-
-}
-// Allows to print state label representing its id
-std::string SogKripkeOTF::format_state(const spot::state* s) const
-{
- //cout<<__func__<<endl;
- auto ss = static_cast<const SogKripkeStateOTF*>(s);
- std::ostringstream out;
- out << "( " << ss->getLDDState()->getLDDValue() << ")";
- return out.str();
-}
-
-SogKripkeIteratorOTF* SogKripkeOTF::succ_iter(const spot::state* s) const
-{
-// cout<<__func__<<endl;
-
- auto ss = static_cast<const SogKripkeStateOTF*>(s);
- //////////////////////////////////////////////
-
- return new SogKripkeIteratorOTF(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
-}
-
-bdd SogKripkeOTF::state_condition(const spot::state* s) const
-{
-
- auto ss = static_cast<const SogKripkeStateOTF*>(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;
-}
-
-
-SogKripkeOTF::~SogKripkeOTF()
-{
- //dtor
-}
-
diff --git a/src/SogKripkeOTF.h b/src/SogKripkeOTF.h
deleted file mode 100644
index f43f518b11b74821d8e5b42fd868cb3bcbfadba4..0000000000000000000000000000000000000000
--- a/src/SogKripkeOTF.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#ifndef SOGKRIPKEOTF_H_INCLUDED
-#define SOGKRIPKEOTF_H_INCLUDED
-#include "LDDGraph.h"
-#include "SogKripkeIteratorOTF.h"
-#include <spot/kripke/kripke.hh>
-#include <LDDGraph.h>
-#include <NewNet.h>
-
-
-class SogKripkeOTF: public spot::kripke {
- public:
-
- SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder);
- SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder,set<string> &l_transap,set<string> &l_placeap);
- virtual ~SogKripkeOTF();
- spot::state* get_init_state() const;
- SogKripkeIteratorOTF* 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;
- }*/
- ModelCheckLace *m_builder;
-
- protected:
-
- private:
- std::map<int, int> place_prop;
- //LDDGraph* m_sog;
-};
-
-#endif // SOGKRIPKE_H_INCLUDED
diff --git a/src/SogKripkeStateOTF.cpp b/src/SogKripkeStateOTF.cpp
deleted file mode 100644
index 8bc377b94153ff7d57e4a3ccb552c2cc26a3dfe2..0000000000000000000000000000000000000000
--- a/src/SogKripkeStateOTF.cpp
+++ /dev/null
@@ -1,11 +0,0 @@
-#include <spot/kripke/kripke.hh>
-#include "LDDState.h"
-#include "SogKripkeStateOTF.h"
-
-
-SogKripkeStateOTF::~SogKripkeStateOTF()
-{
- //dtor
-}
-
-static ModelCheckLace * SogKripkeStateOTF::m_builder;
diff --git a/src/SogKripkeStateOTF.h b/src/SogKripkeStateOTF.h
deleted file mode 100644
index 131787c88013f838c94dd4b8fca376ea56bff54b..0000000000000000000000000000000000000000
--- a/src/SogKripkeStateOTF.h
+++ /dev/null
@@ -1,46 +0,0 @@
-#ifndef SOGKRIPKESTATEOTF_H_INCLUDED
-#define SOGKRIPKESTATEOTF_H_INCLUDED
-
-
-#include "LDDState.h"
-#include "ModelCheckLace.h"
-
-class SogKripkeStateOTF : public spot::state
-{
-public:
- static ModelCheckLace * m_builder;
- SogKripkeStateOTF(LDDState *st):m_state(st) {
- m_builder->buildSucc(st);
- };
- virtual ~SogKripkeStateOTF();
-
- SogKripkeStateOTF* clone() const override
- {
- return new SogKripkeStateOTF(m_state);
- }
- size_t hash() const override
- {
- return m_state->getLDDValue();
- }
-
- int compare(const spot::state* other) const override
- {
- auto o = static_cast<const SogKripkeStateOTF*>(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/main.cpp b/src/main.cpp
index 34115a97cf6e794b1a2178d4ebcc8cbb85b795a7..bc75319b1d4e963d7dba2986c9b0f96db664b7d2 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -25,7 +25,7 @@
#include "NewNet.h"
#include "SogTwa.h"
#include "SogKripke.h"
-#include "SogKripkeOTF.h"
+
#include "SogKripkeTh.h"