From 1684c89bbcb4b00c5f50a564a0caba7ce7633d4b Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 2 May 2019 00:13:37 +0100
Subject: [PATCH] =?UTF-8?q?=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
 =?UTF-8?q?=20=20src/SogKripke.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
 =?UTF-8?q?=20=20=20=20src/SogKripkeIterator.cpp=20=09modifi=C3=A9=C2=A0:?=
 =?UTF-8?q?=20=20=20=20=20=20=20=20=20src/SogKripkeIterator.h=20=09modifi?=
 =?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeState.cpp?=
 =?UTF-8?q?=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKrip?=
 =?UTF-8?q?keState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20sr?=
 =?UTF-8?q?c/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/SogKripke.h           |  5 +--
 src/SogKripkeIterator.cpp | 68 +++++++++++++++++++++++++++++++++++++++
 src/SogKripkeIterator.h   | 27 ++++++++++++++++
 src/SogKripkeState.cpp    |  8 +++++
 src/SogKripkeState.h      | 35 ++++++++++++++++++++
 src/main.cpp              |  1 +
 6 files changed, 142 insertions(+), 2 deletions(-)

diff --git a/src/SogKripke.h b/src/SogKripke.h
index 6dae6cf..b6fc776 100644
--- a/src/SogKripke.h
+++ b/src/SogKripke.h
@@ -1,6 +1,7 @@
 #ifndef SOGKRIPKE_H_INCLUDED
 #define SOGKRIPKE_H_INCLUDED
-
+#include "LDDGraph.h"
+#include "SogKripkeIterator.h"
 class SogKripke : public spot::kripke
 {
     public:
@@ -10,7 +11,7 @@ class SogKripke : public spot::kripke
         SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
         virtual ~SogKripke();
         spot::state* get_init_state() const;
-        SpotSogIterator* succ_iter(const spot::state* s) const override;
+        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;
 
diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp
index e69de29..20565dc 100644
--- a/src/SogKripkeIterator.cpp
+++ b/src/SogKripkeIterator.cpp
@@ -0,0 +1,68 @@
+#include <spot/twa/twa.hh>
+#include "LDDGraph.h"
+#include "SogKripkeState.h"
+#include "SogKripkeIterator.h"
+
+
+SogKripkeIterator::SogKripkeIterator(const LDDState* lddstate):m_lddstate(lddstate)
+{
+    //vector<pair<LDDState*, int>>
+    m_lddstate->setDiv(true);
+    for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
+        m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
+    }
+   /* if (lddstate->isDeadLock()) {
+        m_lsucc.push_back(pair(,-1));
+    }*/
+    if (lddstate->isDiv()) {
+        m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
+    }
+}
+bool SogKripkeIterator::first() {
+  //  m_sog->getLDDStateById(m_id)->Successors().
+    //return m_sog->get_successor()
+
+    m_current_edge=0;
+    return m_lsucc.size()!=0;
+}
+
+bool SogKripkeIterator::next() {
+
+    m_current_edge++;
+    return m_current_edge<m_lsucc.size();
+}
+
+bool SogKripkeIterator::done() const {
+
+    return m_current_edge==m_lsucc.size();
+}
+
+SpotSogState* SogKripkeIterator::dst() const
+  {
+    return new SpotSogState(m_lsucc.at(m_current_edge).first);
+  }
+
+bdd SogKripkeIterator::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);
+    //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
+
+    spot::bdd_dict *p=m_dict_ptr->get();
+    spot::formula f=spot::formula::ap(name);
+    bdd   result=bdd_ithvar((p->var_map.find(f))->second);
+
+    //cout<<"Iterator "<<__func__<<"  "<<m_current_edge<<"\n";
+    return result;
+}
+
+spot::acc_cond::mark_t SogKripkeIterator::acc() const {
+  //cout<<"Iterator acc()\n";
+  return 1U;
+}
+SogKripkeIterator::~SogKripkeIterator()
+{
+    //dtor
+}
+
+static LDDGraph * SogKripkeIterator::m_graph;
+static spot::bdd_dict_ptr* SogKripkeIterator::m_dict_ptr;
diff --git a/src/SogKripkeIterator.h b/src/SogKripkeIterator.h
index eed3549..33fdf33 100644
--- a/src/SogKripkeIterator.h
+++ b/src/SogKripkeIterator.h
@@ -1,6 +1,33 @@
 #ifndef SOGKRIPKEITERATOR_H_INCLUDED
 #define SOGKRIPKEITERATOR_H_INCLUDED
+#include "SogKripkeState.h"
+#include "LDDGraph.h"
+// Iterator for a SOG graph
+class SogKripkeIterator : public spot::twa_succ_iterator
+{
+    public:
 
+        static LDDGraph * m_graph;
+        static spot::bdd_dict_ptr* m_dict_ptr;
+        SogKripkeIterator(const LDDState *lddstate);
+        virtual ~SogKripkeIterator();
+        bool first() override;
+        bool next() override;
+        bool done() const override;
+        SogKripkeState* dst() const override;
+
+        bdd cond() const override final;
+        spot::acc_cond::mark_t acc() const override final;
+
+    protected:
+
+    private:
+        // Associated SOG graph
+
+        LDDState * m_lddstate;
+        vector<pair<LDDState*, int>> m_lsucc;
+        unsigned int m_current_edge=0;
+};
 
 
 #endif // SOGKRIPKEITERATOR_H_INCLUDED
diff --git a/src/SogKripkeState.cpp b/src/SogKripkeState.cpp
index e69de29..8d471cc 100644
--- a/src/SogKripkeState.cpp
+++ b/src/SogKripkeState.cpp
@@ -0,0 +1,8 @@
+#include "LDDState.h"
+#include "SogKripkeState.h"
+
+
+SogKripkeState::~SogKripkeState()
+{
+    //dtor
+}
diff --git a/src/SogKripkeState.h b/src/SogKripkeState.h
index 57c6dbe..089692b 100644
--- a/src/SogKripkeState.h
+++ b/src/SogKripkeState.h
@@ -2,5 +2,40 @@
 #define SOGKRIPKESTATE_H_INCLUDED
 
 
+#include "LDDState.h"
+class SogKripkeState : public spot::state
+{
+public:
+    SogKripkeState(LDDState *st):m_state(st) {};
+    virtual ~SogKripkeState();
+
+    SogKripkeState* clone() const override
+    {
+        return new SogKripkeState(m_state);
+    }
+    size_t hash() const override
+    {
+        return m_state->getLDDValue();
+    }
+
+    int compare(const spot::state* other) const override
+    {
+        auto o = static_cast<const SogKripkeState*>(other);
+        size_t oh = o->hash();
+        size_t h = hash();
+        if (h < oh)
+            return -1;
+        else
+            return h > oh;
+    }
+    LDDState* getLDDState() {
+        return m_state;
+    }
+protected:
+
+private:
+    LDDState *m_state;
+};
+
 
 #endif // SOGKRIPKESTATE_H_INCLUDED
diff --git a/src/main.cpp b/src/main.cpp
index bcba3af..4645d56 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -23,6 +23,7 @@
 #include <spot/tl/apcollect.hh>
 #include "NewNet.h"
 #include "SogTwa.h"
+#include "SogKripke.h"
 
 
 
-- 
GitLab