From 29dee60598bcf6fbdd32bee0548a525cdb458144 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sun, 26 May 2019 23:14:35 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/CMakeLists.txt=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20=20src/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/ModelCheckLace.h=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeIteratorOTF.cpp?=
=?UTF-8?q?=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKrip?=
=?UTF-8?q?keIteratorOTF.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
=?UTF-8?q?=20=20src/SogKripkeOTF.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/SogKripkeOTF.h=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/CMakeLists.txt | 6 ++++++
src/ModelCheckLace.cpp | 6 ++++++
src/ModelCheckLace.h | 3 ++-
src/SogKripkeIteratorOTF.cpp | 6 ++++--
src/SogKripkeIteratorOTF.h | 25 ++++---------------------
src/SogKripkeOTF.cpp | 6 +++---
src/SogKripkeOTF.h | 8 ++++----
src/main.cpp | 4 ++++
8 files changed, 33 insertions(+), 31 deletions(-)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9f92226..a042d27 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 e7d3276..1e73d55 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 717f100..6950b92 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 b1fa514..c2f4828 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 d1f191a..7a3ac82 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 dafb027..37b7b93 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 300e783..6360cae 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 e48bd28..434f3e0 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)
--
GitLab