From e4a70a5247db83c556454ba1c017c52ee7cc99e2 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Fri, 14 Jun 2019 15:13:38 +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=09supprim=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/SogKripkeIteratorOTF.cpp=20=09supprim=C3=A9=C2=A0:?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeIteratorOTF.h=20=09supprim?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20src/SogKripkeOTF.cpp=20=09?=
=?UTF-8?q?supprim=C3=A9=C2=A0:=20=20=20=20=20=20=20=20src/SogKripkeOTF.h?=
=?UTF-8?q?=20=09supprim=C3=A9=C2=A0:=20=20=20=20=20=20=20=20src/SogKripke?=
=?UTF-8?q?StateOTF.cpp=20=09supprim=C3=A9=C2=A0:=20=20=20=20=20=20=20=20s?=
=?UTF-8?q?rc/SogKripkeStateOTF.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=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/SogKripkeIteratorOTF.cpp | 77 ------------------------------
src/SogKripkeIteratorOTF.h | 39 ---------------
src/SogKripkeOTF.cpp | 92 ------------------------------------
src/SogKripkeOTF.h | 34 -------------
src/SogKripkeStateOTF.cpp | 11 -----
src/SogKripkeStateOTF.h | 46 ------------------
src/main.cpp | 2 +-
8 files changed, 1 insertion(+), 306 deletions(-)
delete mode 100644 src/SogKripkeIteratorOTF.cpp
delete mode 100644 src/SogKripkeIteratorOTF.h
delete mode 100644 src/SogKripkeOTF.cpp
delete mode 100644 src/SogKripkeOTF.h
delete mode 100644 src/SogKripkeStateOTF.cpp
delete mode 100644 src/SogKripkeStateOTF.h
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d4c956e..8f392a2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -62,12 +62,6 @@ add_executable(hybrid-sog main.cpp
ModelCheckBaseMT.h
ModelCheckLace.cpp
ModelCheckLace.h
- SogKripkeStateOTF.cpp
- SogKripkeStateOTF.h
- SogKripkeIteratorOTF.cpp
- SogKripkeIteratorOTF.h
- SogKripkeOTF.cpp
- SogKripkeOTF.h
SogKripkeTh.cpp
SogKripkeTh.h
SogKripkeStateTh.cpp
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
deleted file mode 100644
index e2e73dc..0000000
--- a/src/SogKripkeIteratorOTF.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-#include <spot/kripke/kripke.hh>
-#include "LDDGraph.h"
-#include "SogKripkeStateOTF.h"
-#include "SogKripkeIteratorOTF.h"
-
-
-SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
-{
-
- 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 SogKripkeIteratorOTF::first() {
-
- // cout<<"entering "<<__func__<<endl;
- m_current_edge=0;
- //cout<<"exciting "<<__func__<<endl;
- return m_lsucc.size()!=0;
-
-}
-
-bool SogKripkeIteratorOTF::next() {
- //cout<<"entering "<<__func__<<endl;
- m_current_edge++;
- return m_current_edge<m_lsucc.size();
-
-}
-
-bool SogKripkeIteratorOTF::done() const {
- //cout<<"entring /excit"<<__func__<<endl;
- return m_current_edge==m_lsucc.size();
-
-}
-
-SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
- {
- //cout<<"enter/excit "<<__func__<<endl;
- return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
- }
-
-bdd SogKripkeIteratorOTF::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);
-
- //cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n";*/
- //cout<<"exciting "<<__func__<<endl;
- return result & spot::kripke_succ_iterator::cond();
-}
-
-/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
- //cout<<"Iterator acc()\n";
- return 0U;
-}*/
-SogKripkeIteratorOTF::~SogKripkeIteratorOTF()
-{
- //dtor
-}
-
-static ModelCheckLace * SogKripkeIteratorOTF::m_builder;
-static spot::bdd_dict_ptr* SogKripkeIteratorOTF::m_dict_ptr;
-static LDDState SogKripkeIteratorOTF::m_deadlock;
diff --git a/src/SogKripkeIteratorOTF.h b/src/SogKripkeIteratorOTF.h
deleted file mode 100644
index 717afbf..0000000
--- a/src/SogKripkeIteratorOTF.h
+++ /dev/null
@@ -1,39 +0,0 @@
-#ifndef SOGKRIPKEITERATOROTF_H_INCLUDED
-#define SOGKRIPKEITERATOROTF_H_INCLUDED
-#include "SogKripkeStateOTF.h"
-#include "ModelCheckLace.h"
-#include <spot/kripke/kripke.hh>
-// Iterator for a SOG graph
-class SogKripkeIteratorOTF : public spot::kripke_succ_iterator
-{
-public:
- static LDDState m_deadlock;
- 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 LDDState* lddstate, bdd cnd);
- virtual ~SogKripkeIteratorOTF();
- bool first() override;
- bool next() override;
- bool done() const override;
- SogKripkeStateOTF* dst() const override;
- bdd cond() const override final;
-
- SogKripkeStateOTF* current_state() const;
-
- bdd current_condition() const;
-
- int current_transition() const;
-
- bdd current_acceptance_conditions() const;
-
- std::string format_transition() const;
-
-private:
- LDDState * m_lddstate;
- vector<pair<LDDState*, int>> m_lsucc;
- unsigned int m_current_edge=0;
-};
-
-
-#endif // SOGKRIPKEITERATOR_H_INCLUDED
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
deleted file mode 100644
index 215b455..0000000
--- a/src/SogKripkeOTF.cpp
+++ /dev/null
@@ -1,92 +0,0 @@
-#include <spot/twaalgos/dot.hh>
-#include <spot/twaalgos/hoa.hh>
-#include <spot/kripke/kripke.hh>
-#include <spot/twa/bdddict.hh>
-
-
-#include "SogKripkeIteratorOTF.h"
-#include "SogKripkeStateOTF.h"
-
-#include "SogKripkeOTF.h"
-#include <map>
-using namespace spot;
-SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder): spot::kripke(dict_ptr),m_builder(builder)
-{
- SogKripkeIteratorOTF::m_builder=builder;
- SogKripkeStateOTF::m_builder=builder;
- SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
-
- //cout<<__func__<<endl;
-}
-
-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);
- }
- for (auto it=l_placeap.begin(); it!=l_placeap.end(); it++)
- register_ap(*it);
-
-}
-
-
-state* SogKripkeOTF::get_init_state() const
-{
- // cout<<__func__<<endl;
- return new SogKripkeStateOTF(m_builder->buildInitialMetaState());//new SpotSogState();
-
-}
-// Allows to print state label representing its id
-std::string SogKripkeOTF::format_state(const spot::state* s) const
-{
- //cout<<__func__<<endl;
- auto ss = static_cast<const SogKripkeStateOTF*>(s);
- std::ostringstream out;
- out << "( " << ss->getLDDState()->getLDDValue() << ")";
- return out.str();
-}
-
-SogKripkeIteratorOTF* SogKripkeOTF::succ_iter(const spot::state* s) const
-{
-// cout<<__func__<<endl;
-
- auto ss = static_cast<const SogKripkeStateOTF*>(s);
- //////////////////////////////////////////////
-
- return new SogKripkeIteratorOTF(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
-}
-
-bdd SogKripkeOTF::state_condition(const spot::state* s) const
-{
-
- auto ss = static_cast<const SogKripkeStateOTF*>(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;
-}
-
-
-SogKripkeOTF::~SogKripkeOTF()
-{
- //dtor
-}
-
diff --git a/src/SogKripkeOTF.h b/src/SogKripkeOTF.h
deleted file mode 100644
index f43f518..0000000
--- a/src/SogKripkeOTF.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#ifndef SOGKRIPKEOTF_H_INCLUDED
-#define SOGKRIPKEOTF_H_INCLUDED
-#include "LDDGraph.h"
-#include "SogKripkeIteratorOTF.h"
-#include <spot/kripke/kripke.hh>
-#include <LDDGraph.h>
-#include <NewNet.h>
-
-
-class SogKripkeOTF: public spot::kripke {
- public:
-
- SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder);
- 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;
- std::string format_state(const spot::state* s) const override;
- bdd state_condition(const spot::state* s) const override;
-
- /// \brief Get the graph associated to the automaton.
- /* const LDDGraph& get_graph() const {
- return *m_sog;
- }*/
- ModelCheckLace *m_builder;
-
- protected:
-
- private:
- std::map<int, int> place_prop;
- //LDDGraph* m_sog;
-};
-
-#endif // SOGKRIPKE_H_INCLUDED
diff --git a/src/SogKripkeStateOTF.cpp b/src/SogKripkeStateOTF.cpp
deleted file mode 100644
index 8bc377b..0000000
--- a/src/SogKripkeStateOTF.cpp
+++ /dev/null
@@ -1,11 +0,0 @@
-#include <spot/kripke/kripke.hh>
-#include "LDDState.h"
-#include "SogKripkeStateOTF.h"
-
-
-SogKripkeStateOTF::~SogKripkeStateOTF()
-{
- //dtor
-}
-
-static ModelCheckLace * SogKripkeStateOTF::m_builder;
diff --git a/src/SogKripkeStateOTF.h b/src/SogKripkeStateOTF.h
deleted file mode 100644
index 131787c..0000000
--- a/src/SogKripkeStateOTF.h
+++ /dev/null
@@ -1,46 +0,0 @@
-#ifndef SOGKRIPKESTATEOTF_H_INCLUDED
-#define SOGKRIPKESTATEOTF_H_INCLUDED
-
-
-#include "LDDState.h"
-#include "ModelCheckLace.h"
-
-class SogKripkeStateOTF : public spot::state
-{
-public:
- static ModelCheckLace * m_builder;
- SogKripkeStateOTF(LDDState *st):m_state(st) {
- m_builder->buildSucc(st);
- };
- virtual ~SogKripkeStateOTF();
-
- SogKripkeStateOTF* clone() const override
- {
- return new SogKripkeStateOTF(m_state);
- }
- size_t hash() const override
- {
- return m_state->getLDDValue();
- }
-
- int compare(const spot::state* other) const override
- {
- auto o = static_cast<const SogKripkeStateOTF*>(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 34115a9..bc75319 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -25,7 +25,7 @@
#include "NewNet.h"
#include "SogTwa.h"
#include "SogKripke.h"
-#include "SogKripkeOTF.h"
+
#include "SogKripkeTh.h"
--
GitLab