diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9f92226db0b2debf6130b80c34b40a366ecffc22..a042d27f9947f696921e586c1d8ade70a4034042 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -60,6 +60,12 @@ add_executable(hybrid-sog main.cpp
SogKripke.h
ModelCheckLace.cpp
ModelCheckLace.h
+ SogKripkeStateOTF.cpp
+ SogKripkeStateOTF.h
+ SogKripkeIteratorOTF.cpp
+ SogKripkeIteratorOTF.h
+ SogKripkeOTF.cpp
+ SogKripkeOTF.h
)
target_link_libraries(hybrid-sog
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index e7d3276ff014a5bce6bd004211f901a93d288843..1e73d55aed98d2a9ea539de5bf4cf786831d29e4 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -114,3 +114,9 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
delete [] prec;
delete [] postc;
}
+
+
+string ModelCheckLace::getTransition(int pos) {
+string temp;
+return temp;
+}
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index 717f1006b009d896fa306434e7641667b51aeb75..6950b92ab1cb1db3411383622b6770532293b6d6 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -4,7 +4,8 @@
class ModelCheckLace : public CommonSOG {
public:
ModelCheckLace(const NewNet &R, int BOUND,int nbThread);
- LDDState & getInitialMetaState();
+ LDDState & buildInitialMetaState();
+ string getTransition(int pos);
private:
int m_nb_thread;
MDD m_initalMarking;
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
index b1fa51415c0ba28d95b4dcda4266a31928df043a..c2f48285c146f1c55a78e9adafb2acb44f4056fb 100644
--- a/src/SogKripkeIteratorOTF.cpp
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -4,7 +4,7 @@
#include "SogKripkeIteratorOTF.h"
-SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDGraph& m_gr, const SogKripkeStateOTF& lddstate, bdd cnd):m_sog(m_gr),m_lddstate(lddstate), kripke_succ_iterator(cnd)
+SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
{
//vector<pair<LDDState*, int>>
m_lddstate->setDiv(true);
@@ -44,7 +44,7 @@ SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
bdd SogKripkeIteratorOTF::cond() const {
if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
- string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
+ 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();
@@ -65,3 +65,5 @@ SogKripkeIteratorOTF::~SogKripkeIteratorOTF()
//dtor
}
+static ModelCheckLace * SogKripkeIteratorOTF::m_builder;
+static spot::bdd_dict_ptr* SogKripkeIteratorOTF::m_dict_ptr;
diff --git a/src/SogKripkeIteratorOTF.h b/src/SogKripkeIteratorOTF.h
index d1f191a97fed2fec0df57565c055e0b2edcd94cc..7a3ac826762e0446ca120669b585933198cee017 100644
--- a/src/SogKripkeIteratorOTF.h
+++ b/src/SogKripkeIteratorOTF.h
@@ -1,17 +1,17 @@
#ifndef SOGKRIPKEITERATOROTF_H_INCLUDED
#define SOGKRIPKEITERATOROTF_H_INCLUDED
#include "SogKripkeStateOTF.h"
-#include "LDDGraph.h"
+#include "ModelCheckLace.h"
#include <spot/kripke/kripke.hh>
// Iterator for a SOG graph
class SogKripkeIteratorOTF : public spot::kripke_succ_iterator
{
public:
- // static LDDGraph * m_graph;
+ 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 LDDGraph& m_gr, const SogKripkeStateOTF& lddstate, bdd cnd);
+ SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd);
virtual ~SogKripkeIteratorOTF();
bool first() override;
bool next() override;
@@ -30,26 +30,9 @@ public:
std::string format_transition() const;
private:
- //const threadSOG& pn_sog; ///< The petri net.
- MDD from; ///< The source state.
- bool dead; ///< The source div attribut.
- bool div; ///< The source div attribut.
- // bdd cond; ///< The condition which must label all successors.
-
- std::set<int>::const_iterator it;
- /// \brief Designate the associated Petri net.
- // const SogKripkeOTF& pn_sog;
-
- /// \brief Point to the marking for which we iterate.
- //MDD mark;
- // Associated SOG graph
-
LDDState * m_lddstate;
- LDDGraph *m_sog;
- vector<pair<SogKripkeStateOTF, int>> m_lsucc;
+ vector<pair<LDDState*, int>> m_lsucc;
unsigned int m_current_edge=0;
- LDDGraph * SogKripkeIteratorOTF::m_graph;
- // spot::bdd_dict_ptr* SogKripkeIteratorOTF::m_dict_ptr;
};
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index dafb02769abdcbfcb1319dc365003efdf7fc92e4..37b7b9367d3fc6a76ee3acca6742461c0be8c2ad 100644
--- a/src/SogKripkeOTF.cpp
+++ b/src/SogKripkeOTF.cpp
@@ -10,13 +10,13 @@
#include "SogKripkeOTF.h"
#include <map>
using namespace spot;
-SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(dict_ptr),m_sog(sog)
+SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder): spot::kripke(dict_ptr),m_builder(builder)
{
- SogKripkeIteratorOTF::m_graph=sog;
+ SogKripkeIteratorOTF::m_builder=builder;
SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
}
-SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap):SogKripkeOTF(dict_ptr,sog) {
+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);
}
diff --git a/src/SogKripkeOTF.h b/src/SogKripkeOTF.h
index 300e783f5fd888940c1dcab08c787c601574f36b..6360cae6148c0bc626d6be10cee0301d46ae218c 100644
--- a/src/SogKripkeOTF.h
+++ b/src/SogKripkeOTF.h
@@ -11,7 +11,7 @@ class SogKripkeOTF: public spot::kripke {
public:
//SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
- SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,const NewNet *n,set<string> &l_transap,set<string> &l_placeap);
+ 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;
@@ -19,10 +19,10 @@ class SogKripkeOTF: public spot::kripke {
bdd state_condition(const spot::state* s) const override;
/// \brief Get the graph associated to the automaton.
- const LDDGraph& get_graph() const {
+ /* const LDDGraph& get_graph() const {
return *m_sog;
- }
- LDDGraph *m_sog;
+ }*/
+ ModelCheckLace *m_builder;
protected:
diff --git a/src/main.cpp b/src/main.cpp
index e48bd281a167cee4bee6d21c432cb78b90595053..434f3e0e6237d9227816ae8dbdabc65d7a4cb1a2 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -24,6 +24,7 @@
#include "NewNet.h"
#include "SogTwa.h"
#include "SogKripke.h"
+#include "SogKripkeOTF.h"
@@ -146,6 +147,9 @@ int main(int argc, char** argv)
}
// Initialize SOG builder
ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
+ spot::twa_graph_ptr k =
+ spot::make_twa_graph(std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
+ spot::twa::prop_set::all(), true);
// Performing on the fly Modelchecking
}
else if (n_tasks==1)