nouveau fichier : src/HybridKripke.cpp

	nouveau fichier : src/HybridKripke.h
	nouveau fichier : src/HybridKripkeIterator.cpp
	nouveau fichier : src/HybridKripkeIterator.h
	nouveau fichier : src/HybridKripkeState.cpp
	nouveau fichier : src/HybridKripkeState.h

src/HybridKripke.cpp

+#include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/kripke/kripke.hh>
+#include <spot/twa/bdddict.hh>
+
+
+#include "HybridKripkeIterator.h"
+#include "HybridKripkeState.h"
+
+#include "HybridKripke.h"
+#include <map>
+using namespace spot;
+SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder): spot::kripke(dict_ptr),m_builder(builder)
+{
+    SogKripkeIteratorTh::m_builder=builder;
+    SogKripkeStateTh::m_builder=builder;
+    SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
+    SogKripkeIteratorTh::m_deadlock.setLDDValue(1);
+    SogKripkeIteratorTh::m_deadlock.setVisited();
+    SogKripkeIteratorTh::m_deadlock.setCompletedSucc();
+    SogKripkeIteratorTh::m_div.setLDDValue(0);
+    SogKripkeIteratorTh::m_div.setVisited();
+    SogKripkeIteratorTh::m_div.setCompletedSucc();
+    SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));
+}
+
+SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
+
+    for (auto it=l_transap.begin();it!=l_transap.end();it++) {
+        register_ap(*it);
+    }
+    for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
+        register_ap(*it);
+
+}
+
+
+state* SogKripkeTh::get_init_state() const {
+   LDDState *ss=m_builder->getInitialMetaState();   
+    return new SogKripkeStateTh(ss);//new SpotSogState();
+
+}
+// Allows to print state label representing its id
+std::string SogKripkeTh::format_state(const spot::state* s) const
+  {
+    //cout<<__func__<<endl;
+    auto ss = static_cast<const SogKripkeStateTh*>(s);
+    std::ostringstream out;
+    out << "( " << ss->getLDDState()->getLDDValue() <<  ")";
+   // cout << " ( " << ss->getLDDState()->getLDDValue() <<  ")";
+    return out.str();
+  }
+
+SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
+   
+    auto ss = static_cast<const SogKripkeStateTh*>(s);
+    LDDState *aggregate=ss->getLDDState();
+    bdd cond = state_condition(ss);
+    if (iter_cache_)
+    {
+      auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
+      iter_cache_ = nullptr;    // empty the cache
+      it->recycle(aggregate, cond);
+      return it;
+    }
+  return new SogKripkeIteratorTh(aggregate,cond);
+
+    
+    
+    
+/*    auto ss = static_cast<const SogKripkeStateTh*>(s);
+   //////////////////////////////////////////////
+
+    return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));*/
+}
+
+bdd SogKripkeTh::state_condition(const spot::state* s) const
+  {
+
+    auto ss = static_cast<const SogKripkeStateTh*>(s);
+    vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
+
+
+    bdd result=bddtrue;
+    // Marked places
+    for (auto it=marked_place.begin();it!=marked_place.end();it++) {
+    string name=m_builder->getPlace(*it);
+    spot::formula f=spot::formula::ap(name);
+    result&=bdd_ithvar((dict_->var_map.find(f))->second);
+    }
+    vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_builder->getPlaceProposition());
+    for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
+    string name=m_builder->getPlace(*it);
+    spot::formula f=spot::formula::ap(name);
+    result&=!bdd_ithvar((dict_->var_map.find(f))->second);
+    }
+
+  return result;
+  }
+
+
+SogKripkeTh::~SogKripkeTh()
+{
+    //dtor
+}
+

src/HybridKripke.h

+#ifndef HYBRIDKRIPKETH_H_INCLUDED
+#define HYBRIDKRIPKETH_H_INCLUDED
+#include "LDDGraph.h"
+#include "HybridKripkeIterator.h"
+#include <spot/kripke/kripke.hh>
+#include <LDDGraph.h>
+#include <NewNet.h>
+
+
+class SogKripkeTh: public spot::kripke {
+    public:
+
+        SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder);
+        SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap);
+        virtual ~SogKripkeTh();
+        spot::state* get_init_state() const override;
+        SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
+        std::string format_state(const spot::state* s) const override;
+        bdd state_condition(const spot::state* s) const override;
+
+        ModelCheckBaseMT *m_builder;
+
+    protected:
+
+    private:
+    std::map<int, int> place_prop;
+    //LDDGraph* m_sog;
+};
+
+#endif // SOGKRIPKE_H_INCLUDED

src/HybridKripkeIterator.cpp

+#include <spot/kripke/kripke.hh>
+#include "LDDGraph.h"
+#include "HybridKripkeState.h"
+#include "HybridKripkeIterator.h"
+
+
+SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
+{
+    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<LDDState*,int>(&m_deadlock,-1));
+    }
+    if (lddstate->isDiv()) {
+        m_lsucc.push_back(pair<LDDState*,int>(&m_div,-1));
+    }
+
+}
+bool SogKripkeIteratorTh::first() {
+
+   // cout<<"entering "<<__func__<<endl;
+    m_current_edge=0;
+    //cout<<"exciting "<<__func__<<endl;
+    return m_lsucc.size()!=0;
+
+}
+
+bool SogKripkeIteratorTh::next() {
+    //cout<<"entering "<<__func__<<"   "<<m_current_edge<<endl;
+    m_current_edge++;
+    return m_current_edge<m_lsucc.size();
+
+}
+
+bool SogKripkeIteratorTh::done() const {
+    //cout<<"entring /excit"<<__func__<<endl;
+    return m_current_edge==m_lsucc.size();
+
+}
+
+SogKripkeStateTh* SogKripkeIteratorTh::dst() const
+  {
+    /*cout<<"Source "<<m_lddstate->getLDDValue()<<"Destination :"<<m_lsucc.at(m_current_edge).first->getLDDValue()<<" in "<<m_lsucc.size()<<" / "<<m_current_edge<<endl;*/
+    return new SogKripkeStateTh(m_lsucc.at(m_current_edge).first);
+  }
+
+bdd SogKripkeIteratorTh::cond()  const {
+    //cout<<"entering "<<__func__<<endl;
+    if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+
+    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();
+    spot::formula f=spot::formula::ap(name);
+    bdd   result=bdd_ithvar((p->var_map.find(f))->second);
+
+    return result & spot::kripke_succ_iterator::cond();
+}
+
+/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
+  //cout<<"Iterator acc()\n";
+  return 0U;
+}*/
+SogKripkeIteratorTh::~SogKripkeIteratorTh()
+{
+    //dtor
+}
+
+void SogKripkeIteratorTh::recycle(LDDState* aggregate, bdd cond)
+{
+        m_lddstate=aggregate;
+        spot::kripke_succ_iterator::recycle(cond);
+}
+
+static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
+static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
+static LDDState SogKripkeIteratorTh::m_deadlock;
+static LDDState SogKripkeIteratorTh::m_div;

src/HybridKripkeIterator.h

+#ifndef HybridKRIPKEITERATORTH_H_INCLUDED
+#define HybridKRIPKEITERATORTH_H_INCLUDED
+#include "HybridKripkeState.h"
+#include "ModelCheckBaseMT.h"
+#include <spot/kripke/kripke.hh>
+// Iterator for a SOG graph
+class HybridKripkeIterator : public spot::kripke_succ_iterator
+{
+public:
+    static LDDState m_deadlock;
+    static LDDState m_div;
+    static ModelCheckBaseMT * m_builder;
+    static spot::bdd_dict_ptr* m_dict_ptr;
+  //  sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
+    HybridKripkeIterator(const LDDState* lddstate, bdd cnd);
+    virtual ~HybridKripkeIterator();
+    bool first() override;
+    bool next() override;
+    bool done() const override;
+    SogKripkeStateTh* dst() const override;
+    bdd cond() const override final;
+
+    SogKripkeStateTh* current_state() const;
+
+    void recycle(LDDState *aggregate, bdd cond);
+
+   
+    std::string format_transition() const;
+
+private:
+    LDDState * m_lddstate;
+    vector<pair<LDDState*, int>> m_lsucc;
+    unsigned int m_current_edge=0;
+};
+
+
+#endif // HybridKRIPKEITERATOR_H_INCLUDED

src/HybridKripkeState.cpp

+#include <spot/kripke/kripke.hh>
+#include "LDDState.h"
+#include "SogKripkeStateTh.h"
+
+
+SogKripkeStateTh::~SogKripkeStateTh()
+{
+    //dtor
+}
+
+static ModelCheckBaseMT * SogKripkeStateTh::m_builder;

src/HybridKripkeState.h

+#ifndef SOGKRIPKESTATETH_H_INCLUDED
+#define SOGKRIPKESTATETH_H_INCLUDED
+
+
+#include "LDDState.h"
+#include "ModelCheckBaseMT.h"
+
+class SogKripkeStateTh : public spot::state
+{
+public:
+    static ModelCheckBaseMT * m_builder;
+    SogKripkeStateTh(LDDState *st):m_state(st) {
+            m_builder->buildSucc(st);
+    };
+    virtual ~SogKripkeStateTh();
+
+    SogKripkeStateTh* clone() const override
+    {
+        return new SogKripkeStateTh(m_state);
+    }
+    size_t hash() const override
+    {
+        return m_state->getLDDValue();
+    }
+
+    int compare(const spot::state* other) const override
+    {
+        auto o = static_cast<const SogKripkeStateTh*>(other);
+        size_t oh = o->hash();
+        size_t h = hash();
+        //return (h!=oh);
+        if (h < oh)
+            return -1;
+        else
+            return h > oh;
+    }
+    LDDState* getLDDState() {
+        return m_state;
+    }
+protected:
+
+private:
+    LDDState *m_state;
+};
+
+
+#endif // SOGKRIPKESTATE_H_INCLUDED