From 294f48d900db9bc0316162fb71a52570bc69db2f Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 2 May 2019 21:31:57 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/SogKripke.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/SogKripke.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/SogTwa.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/SogTwa.h=20=09modifi=C3=A9=C2=A0:=20=20?=
=?UTF-8?q?=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/SogKripke.cpp | 30 +++++++++++-------------------
src/SogKripke.h | 3 ++-
src/SogTwa.cpp | 22 ++++++----------------
src/SogTwa.h | 1 +
src/main.cpp | 3 ++-
5 files changed, 22 insertions(+), 37 deletions(-)
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index f86562d..2cc68c6 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -14,24 +14,15 @@ SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(d
{
SogKripkeIterator::m_graph=sog;
SogKripkeIterator::m_dict_ptr=&dict_ptr;
-/*spot::bdd_dict *p=dict_ptr.get();
-cout<<"Taille du dictionnaire :"<<p->var_map.size()<<endl;
+}
-map<spot::formula,int>::iterator i=(p->var_map).begin();
+SogKripke::SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap):SogKripke(dict_ptr,sog) {
+ for (auto it=l_transap.begin();it!=l_transap.end();it++) {
+ register_ap(*it);
+ }
+}
-while (i!=(p->var_map).end()) {
- cout<<" test :"<<(*i).first.ap_name()<<endl;
-std::ostringstream stream;
- stream << (*i).first;
- std::string str = stream.str();
- cout<<" formule 1: "<<str<<endl;
- cout<<" formule 2: "<<str<<endl;
- i++;
-}*/
-//spot::bdd_format_formula(dict_ptr,"test");
-//map<bdd,spot::ltl::formula>.iterator it=p->vf_map.begin();
-}
state* SogKripke::get_init_state() const {
//cout<<"Initial state given...\n";
return new SogKripkeState(m_sog->getInitialState());//new SpotSogState();
@@ -57,17 +48,18 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
return new SogKripkeIterator(ss->getLDDState(),b);//,b);//s state_condition(ss));
}
- /* MDD state_condition(const spot::state* s) const override
+bdd SogKripke::state_condition(const spot::state* s) const
{
- auto ss = static_cast<const SogKripkeState*>(s);
+ /*auto ss = static_cast<const SogKripkeState*>(s);
MDD res = lddmc_true;
std::map<int, int>::const_iterator it;
for (it = place_prop.begin(); it != place_prop.end(); ++it)
if (m_sog->is_marked(it->first, m))
- return res;
- }*/
+ return res;*/
+ return bddtrue;
+ }
SogKripke::~SogKripke()
diff --git a/src/SogKripke.h b/src/SogKripke.h
index a0cf52d..a2bac01 100644
--- a/src/SogKripke.h
+++ b/src/SogKripke.h
@@ -9,11 +9,12 @@ class SogKripke: public spot::kripke {
SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
+ SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap);
virtual ~SogKripke();
spot::state* get_init_state() const;
SogKripkeIterator* succ_iter(const spot::state* s) const override;
std::string format_state(const spot::state* s) const override;
- // MDD state_condition(const spot::state* s) const override;
+ bdd state_condition(const spot::state* s) const override;
protected:
diff --git a/src/SogTwa.cpp b/src/SogTwa.cpp
index f65c22b..42ea5c2 100644
--- a/src/SogTwa.cpp
+++ b/src/SogTwa.cpp
@@ -14,23 +14,13 @@ SogTwa::SogTwa(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): twa(dict_ptr),m_sog(
{
SpotSogIterator::m_graph=sog;
SpotSogIterator::m_dict_ptr=&dict_ptr;
-/*spot::bdd_dict *p=dict_ptr.get();
-cout<<"Taille du dictionnaire :"<<p->var_map.size()<<endl;
-
-map<spot::formula,int>::iterator i=(p->var_map).begin();
-
-while (i!=(p->var_map).end()) {
- cout<<" test :"<<(*i).first.ap_name()<<endl;
-std::ostringstream stream;
- stream << (*i).first;
- std::string str = stream.str();
- cout<<" formule 1: "<<str<<endl;
- cout<<" formule 2: "<<str<<endl;
- i++;
-}*/
-//spot::bdd_format_formula(dict_ptr,"test");
-//map<bdd,spot::ltl::formula>.iterator it=p->vf_map.begin();
+}
+
+SogTwa::SogTwa(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap):SogTwa(dict_ptr,sog) {
+ for (auto it=l_transap.begin();it!=l_transap.end();it++) {
+ register_ap(*it);
+ }
}
state* SogTwa::get_init_state() const {
//cout<<"Initial state given...\n";
diff --git a/src/SogTwa.h b/src/SogTwa.h
index 05a0033..5a39479 100644
--- a/src/SogTwa.h
+++ b/src/SogTwa.h
@@ -7,6 +7,7 @@ class SogTwa : public spot::twa
{
public:
SogTwa(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
+ SogTwa(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap);
virtual ~SogTwa();
spot::state* get_init_state() const;
SpotSogIterator* succ_iter(const spot::state* s) const override;
diff --git a/src/main.cpp b/src/main.cpp
index 4645d56..5ce1d93 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -176,6 +176,7 @@ int main(int argc, char** argv)
{
cout<<"Building automata for not(formula)\n";
auto d = spot::make_bdd_dict();
+ // d->register_ap("jbhkj");
spot::twa_graph_ptr af = spot::translator(d).run(not_f);
cout<<"Formula automata built.\n";
cout<<"Want to save the graph in a dot file ?";
@@ -188,7 +189,7 @@ int main(int argc, char** argv)
spot::print_dot(file, af);
file.close();
}
- auto k = std::make_shared<SogTwa>(d,DR.getGraph());
+ auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP());
cout<<"SOG translated to SPOT succeeded.."<<endl;
cout<<"Want to save the graph in a dot file ?";
cin>>c;
--
GitLab