Skip to content
Snippets Groups Projects
Commit e4a70a52 authored by Chiheb Amer Abid's avatar Chiheb Amer Abid
Browse files

modifié : src/CMakeLists.txt 

	supprimé :        src/SogKripkeIteratorOTF.cpp
	supprimé :        src/SogKripkeIteratorOTF.h
	supprimé :        src/SogKripkeOTF.cpp
	supprimé :        src/SogKripkeOTF.h
	supprimé :        src/SogKripkeStateOTF.cpp
	supprimé :        src/SogKripkeStateOTF.h
	modifié :         src/main.cpp
parent 7744f597
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/CMakeLists.txt
+ 0
− 6
View file @ e4a70a52
......@@ -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
......
src/SogKripkeIteratorOTF.cpp deleted 100644 → 0
+ 0
− 77
View file @ 7744f597
#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;
src/SogKripkeIteratorOTF.h deleted 100644 → 0
+ 0
− 39
View file @ 7744f597
#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
src/SogKripkeOTF.cpp deleted 100644 → 0
+ 0
− 92
View file @ 7744f597
#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
}
src/SogKripkeOTF.h deleted 100644 → 0
+ 0
− 34
View file @ 7744f597
#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
src/SogKripkeStateOTF.cpp deleted 100644 → 0
+ 0
− 11
View file @ 7744f597
#include <spot/kripke/kripke.hh>
#include "LDDState.h"
#include "SogKripkeStateOTF.h"
SogKripkeStateOTF::~SogKripkeStateOTF()
{
//dtor
}
static ModelCheckLace * SogKripkeStateOTF::m_builder;
src/SogKripkeStateOTF.h deleted 100644 → 0
+ 0
− 46
View file @ 7744f597
#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
src/main.cpp
+ 1
− 1
View file @ e4a70a52
......@@ -25,7 +25,7 @@
#include "NewNet.h"
#include "SogTwa.h"
#include "SogKripke.h"
#include "SogKripkeOTF.h"
#include "SogKripkeTh.h"
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment