modifié : src/CMakeLists.txt

	modifié :         src/ModelCheckLace.cpp
	modifié :         src/ModelCheckLace.h
	modifié :         src/SogKripkeIteratorOTF.cpp
	modifié :         src/SogKripkeIteratorOTF.h
	modifié :         src/SogKripkeOTF.cpp
	modifié :         src/SogKripkeOTF.h
	modifié :         src/main.cpp

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

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;
+}

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;

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;

src/SogKripkeIteratorOTF.h

 #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;
 };
 
 

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);
     }

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:
 

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)