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

modifié : src/CMakeLists.txt 

	modifié :         src/HybridKripke.cpp
	modifié :         src/HybridKripke.h
	modifié :         src/HybridKripkeIterator.cpp
	modifié :         src/HybridKripkeIterator.h
	modifié :         src/HybridKripkeState.cpp
	modifié :         src/HybridKripkeState.h
parent 51ff123e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/CMakeLists.txt
+ 6
− 0
View file @ abb22775
......@@ -72,6 +72,12 @@ add_executable(hybrid-sog main.cpp
ModelCheckerTh.h
MCHybridSOG.cpp
MCHybridSOG.h
HybridKripke.cpp
HybridKripke.h
HybridKripkeIterator.cpp
HybridKripkeIterator.h
HybridKripkeState.cpp
HybridKripkeState.h
)
target_link_libraries(hybrid-sog
......
src/HybridKripke.cpp
+ 23
− 23
View file @ abb22775
......@@ -10,21 +10,21 @@
#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)
HybridKripke::HybridKripke(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));
HybridKripkeIterator::m_builder=builder;
HybridKripkeIterator::m_builder=builder;
HybridKripkeIterator::m_dict_ptr=&dict_ptr;
HybridKripkeIterator::m_deadlock.setLDDValue(1);
HybridKripkeIterator::m_deadlock.setVisited();
HybridKripkeIterator::m_deadlock.setCompletedSucc();
HybridKripkeIterator::m_div.setLDDValue(0);
HybridKripkeIterator::m_div.setVisited();
HybridKripkeIterator::m_div.setCompletedSucc();
HybridKripkeIterator::m_div.Successors.push_back(pair<LDDState*,int>(&HybridKripkeIterator::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) {
HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):HybridKripke(dict_ptr,builder) {
for (auto it=l_transap.begin();it!=l_transap.end();it++) {
register_ap(*it);
......@@ -35,35 +35,35 @@ SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *bu
}
state* SogKripkeTh::get_init_state() const {
state* HybridKripke::get_init_state() const {
LDDState *ss=m_builder->getInitialMetaState();
return new SogKripkeStateTh(ss);//new SpotSogState();
return new HybridKripkeState(ss);//new SpotSogState();
}
// Allows to print state label representing its id
std::string SogKripkeTh::format_state(const spot::state* s) const
std::string HybridKripke::format_state(const spot::state* s) const
{
//cout<<__func__<<endl;
auto ss = static_cast<const SogKripkeStateTh*>(s);
auto ss = static_cast<const HybridKripkeState*>(s);
std::ostringstream out;
out << "( " << ss->getLDDState()->getLDDValue() << ")";
// cout << " ( " << ss->getLDDState()->getLDDValue() << ")";
return out.str();
}
SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
auto ss = static_cast<const SogKripkeStateTh*>(s);
auto ss = static_cast<const HybridKripkeState*>(s);
LDDState *aggregate=ss->getLDDState();
bdd cond = state_condition(ss);
if (iter_cache_)
{
auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
it->recycle(aggregate, cond);
return it;
}
return new SogKripkeIteratorTh(aggregate,cond);
return new HybridKripkeIterator(aggregate,cond);
......@@ -74,10 +74,10 @@ SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));*/
}
bdd SogKripkeTh::state_condition(const spot::state* s) const
bdd HybridKripke::state_condition(const spot::state* s) const
{
auto ss = static_cast<const SogKripkeStateTh*>(s);
auto ss = static_cast<const HybridKripkeState*>(s);
vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
......@@ -99,7 +99,7 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
}
SogKripkeTh::~SogKripkeTh()
HybridKripke::~HybridKripke()
{
//dtor
}
......
src/HybridKripke.h
+ 5
− 5
View file @ abb22775
......@@ -7,14 +7,14 @@
#include <NewNet.h>
class SogKripkeTh: public spot::kripke {
class HybridKripke: 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();
HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder);
HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap);
virtual ~HybridKripke();
spot::state* get_init_state() const override;
SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
HybridKripkeIterator* 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;
......
src/HybridKripkeIterator.cpp
+ 13
− 13
View file @ abb22775
......@@ -4,7 +4,7 @@
#include "HybridKripkeIterator.h"
SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
HybridKripkeIterator::HybridKripkeIterator(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));
......@@ -17,7 +17,7 @@ SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_ld
}
}
bool SogKripkeIteratorTh::first() {
bool HybridKripkeIterator::first() {
// cout<<"entering "<<__func__<<endl;
m_current_edge=0;
......@@ -26,26 +26,26 @@ bool SogKripkeIteratorTh::first() {
}
bool SogKripkeIteratorTh::next() {
bool HybridKripkeIterator::next() {
//cout<<"entering "<<__func__<<" "<<m_current_edge<<endl;
m_current_edge++;
return m_current_edge<m_lsucc.size();
}
bool SogKripkeIteratorTh::done() const {
bool HybridKripkeIterator::done() const {
//cout<<"entring /excit"<<__func__<<endl;
return m_current_edge==m_lsucc.size();
}
SogKripkeStateTh* SogKripkeIteratorTh::dst() const
HybridKripkeState* HybridKripkeIterator::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);
return new HybridKripkeState(m_lsucc.at(m_current_edge).first);
}
bdd SogKripkeIteratorTh::cond() const {
bdd HybridKripkeIterator::cond() const {
//cout<<"entering "<<__func__<<endl;
if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
......@@ -63,18 +63,18 @@ bdd SogKripkeIteratorTh::cond() const {
//cout<<"Iterator acc()\n";
return 0U;
}*/
SogKripkeIteratorTh::~SogKripkeIteratorTh()
HybridKripkeIterator::~HybridKripkeIterator()
{
//dtor
}
void SogKripkeIteratorTh::recycle(LDDState* aggregate, bdd cond)
void HybridKripkeIterator::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;
static ModelCheckBaseMT * HybridKripkeIterator::m_builder;
static spot::bdd_dict_ptr* HybridKripkeIterator::m_dict_ptr;
static LDDState HybridKripkeIterator::m_deadlock;
static LDDState HybridKripkeIterator::m_div;
src/HybridKripkeIterator.h
+ 2
− 2
View file @ abb22775
......@@ -17,10 +17,10 @@ public:
bool first() override;
bool next() override;
bool done() const override;
SogKripkeStateTh* dst() const override;
HybridKripkeState* dst() const override;
bdd cond() const override final;
SogKripkeStateTh* current_state() const;
HybridKripkeState* current_state() const;
void recycle(LDDState *aggregate, bdd cond);
......
src/HybridKripkeState.cpp
+ 3
− 3
View file @ abb22775
#include <spot/kripke/kripke.hh>
#include "LDDState.h"
#include "SogKripkeStateTh.h"
#include "HybridKripkeState.h"
SogKripkeStateTh::~SogKripkeStateTh()
HybridKripkeState::~HybridKripkeState()
{
//dtor
}
static ModelCheckBaseMT * SogKripkeStateTh::m_builder;
static ModelCheckBaseMT * HybridKripkeState::m_builder;
src/HybridKripkeState.h
+ 8
− 8
View file @ abb22775
#ifndef SOGKRIPKESTATETH_H_INCLUDED
#define SOGKRIPKESTATETH_H_INCLUDED
#ifndef HYBRIDKRIPKESTATETH_H_INCLUDED
#define HYBRIDKRIPKESTATETH_H_INCLUDED
#include "LDDState.h"
#include "ModelCheckBaseMT.h"
class SogKripkeStateTh : public spot::state
class HybridKripkeState : public spot::state
{
public:
static ModelCheckBaseMT * m_builder;
SogKripkeStateTh(LDDState *st):m_state(st) {
HybridKripkeState(LDDState *st):m_state(st) {
m_builder->buildSucc(st);
};
virtual ~SogKripkeStateTh();
virtual ~HybridKripkeState();
SogKripkeStateTh* clone() const override
HybridKripkeState* clone() const override
{
return new SogKripkeStateTh(m_state);
return new HybridKripkeState(m_state);
}
size_t hash() const override
{
......@@ -25,7 +25,7 @@ public:
int compare(const spot::state* other) const override
{
auto o = static_cast<const SogKripkeStateTh*>(other);
auto o = static_cast<const HybridKripkeState*>(other);
size_t oh = o->hash();
size_t h = hash();
//return (h!=oh);
......
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