From 47a3c36c8e1287af6a0d03bed092871bcf2ac5a6 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 2 May 2019 01:08:11 +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/SogKripke.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/SogKripke.h=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeIterator.cpp=20=09modifi?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeState.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/CMakeLists.txt | 7 ++++++-
src/SogKripke.cpp | 28 ++++++++++++++--------------
src/SogKripke.h | 6 +++---
src/SogKripkeIterator.cpp | 4 ++--
src/SogKripkeState.cpp | 1 +
5 files changed, 26 insertions(+), 20 deletions(-)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f4953cc..3c737d7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -52,7 +52,12 @@ add_executable(hybrid-sog main.cpp
SpotSogIterator.h
SogTwa.cpp
SogTwa.h
-
+ SogKripkeState.cpp
+ SogKripkeState.h
+ SogKripkeIterator.cpp
+ SogKripkeIterator.h
+ SogKripke.cpp
+ SogKripke.h
)
target_link_libraries(hybrid-sog
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index f46fa15..69a420d 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -1,19 +1,19 @@
#include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/hoa.hh>
-#include <spot/twa/twa.hh>
+#include <spot/kripke/kripke.hh>
#include <spot/twa/bdddict.hh>
-#include "SpotSogIterator.h"
-#include "SpotSogState.h"
+#include "SogKripkeIterator.h"
+#include "SogKripkeState.h"
#include "SogKripke.h"
#include <map>
using namespace spot;
-SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): twa(dict_ptr),m_sog(sog)
+SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(dict_ptr),m_sog(sog)
{
- SpotSogIterator::m_graph=sog;
- SpotSogIterator::m_dict_ptr=&dict_ptr;
+ 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;
@@ -34,28 +34,28 @@ std::ostringstream stream;
}
state* SogKripke::get_init_state() const {
//cout<<"Initial state given...\n";
- return new SpotSogState(m_sog->getInitialState());//new SpotSogState();
+ return new SogKripkeState(m_sog->getInitialState());//new SpotSogState();
}
// Allows to print state label representing its id
std::string SogKripke::format_state(const spot::state* s) const
{
- auto ss = static_cast<const SpotSogState*>(s);
+ auto ss = static_cast<const SogKripkeState*>(s);
std::ostringstream out;
out << "( " << ss->getLDDState()->getLDDValue() << ")";
return out.str();
}
-SpotSogIterator* SogKripke::succ_iter(const spot::state* s) const {
+SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
- auto ss = static_cast<const SpotSogState*>(s);
+ auto ss = static_cast<const SogKripkeState*>(s);
bdd b=bddfalse;
- return new SpotSogIterator(ss->getLDDState());//,b);//s state_condition(ss));
+ return new SogKripkeIterator(ss->getLDDState());//,b);//s state_condition(ss));
}
- MDD state_condition(const spot::state* s) const override
+ /* MDD state_condition(const spot::state* s) const override
{
- auto ss = static_cast<const SpotSogState*>(s);
+ auto ss = static_cast<const SogKripkeState*>(s);
MDD res = lddmc_true;
std::map<int, int>::const_iterator it;
@@ -63,7 +63,7 @@ SpotSogIterator* SogKripke::succ_iter(const spot::state* s) const {
if (m_sog->is_marked(it->first, m))
return res;
- }
+ }*/
SogKripke::~SogKripke()
diff --git a/src/SogKripke.h b/src/SogKripke.h
index b6fc776..a0cf52d 100644
--- a/src/SogKripke.h
+++ b/src/SogKripke.h
@@ -2,8 +2,8 @@
#define SOGKRIPKE_H_INCLUDED
#include "LDDGraph.h"
#include "SogKripkeIterator.h"
-class SogKripke : public spot::kripke
-{
+#include <spot/kripke/kripke.hh>
+class SogKripke: public spot::kripke {
public:
@@ -13,7 +13,7 @@ class SogKripke : public spot::kripke
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;
+ // MDD state_condition(const spot::state* s) const override;
protected:
diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp
index 20565dc..949abe1 100644
--- a/src/SogKripkeIterator.cpp
+++ b/src/SogKripkeIterator.cpp
@@ -37,9 +37,9 @@ bool SogKripkeIterator::done() const {
return m_current_edge==m_lsucc.size();
}
-SpotSogState* SogKripkeIterator::dst() const
+SogKripkeState* SogKripkeIterator::dst() const
{
- return new SpotSogState(m_lsucc.at(m_current_edge).first);
+ return new SogKripkeState(m_lsucc.at(m_current_edge).first);
}
bdd SogKripkeIterator::cond() const {
diff --git a/src/SogKripkeState.cpp b/src/SogKripkeState.cpp
index 8d471cc..d47cc4a 100644
--- a/src/SogKripkeState.cpp
+++ b/src/SogKripkeState.cpp
@@ -1,3 +1,4 @@
+#include <spot/twa/twa.hh>
#include "LDDState.h"
#include "SogKripkeState.h"
--
GitLab