From f101c28f039d33679d5756f5c26779990f3827ae Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Sat, 22 Jun 2019 00:04:04 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?= =?UTF-8?q?=20=20=20=20=20src/ModelCheckLace.h=20=09modifi=C3=A9=C2=A0:=20?= =?UTF-8?q?=20=20=20=20=20=20=20=20src/ModelCheckerTh.cpp=20=09modifi?= =?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeIteratorTh?= =?UTF-8?q?.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/Sog?= =?UTF-8?q?KripkeIteratorTh.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?= =?UTF-8?q?=20=20=20src/SogKripkeStateTh.cpp=20=09modifi=C3=A9=C2=A0:=20?= =?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeStateTh.h=20=09modifi?= =?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeTh.cpp=20?= =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeT?= =?UTF-8?q?h.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/main?= =?UTF-8?q?.cpp?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/ModelCheckLace.cpp | 24 +++++++++++++----------- src/ModelCheckLace.h | 4 ++-- src/ModelCheckerTh.cpp | 11 ++--------- src/SogKripkeIteratorTh.cpp | 13 ++++++++----- src/SogKripkeIteratorTh.h | 6 +++--- src/SogKripkeStateTh.cpp | 2 +- src/SogKripkeStateTh.h | 5 +++-- src/SogKripkeTh.cpp | 24 +++++++++++++++++++----- src/SogKripkeTh.h | 8 ++------ src/main.cpp | 15 +++++++++++---- 10 files changed, 64 insertions(+), 48 deletions(-) diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index 41d1095..9c8cbab 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -190,8 +190,8 @@ TASK_3 (bool, SetDivL, MDD, M, Set*, nonObservable, vector<TransSylvan>*, tb_rel LDDState * ModelCheckLace::getInitialMetaState() { - - LDDState *initalAggregate=new LDDState; + + LDDState *initalAggregate=new LDDState(); LDDState *reached_class; LACE_ME; MDD initial_meta_state(CALL(Aggregate_epsilon_lace,m_initialMarking,&m_nonObservable,&m_tb_relation)); @@ -202,27 +202,28 @@ LDDState * ModelCheckLace::getInitialMetaState() initalAggregate->setVisited(); m_graph->setInitialState(initalAggregate); m_graph->insert(initalAggregate); + initalAggregate->setDiv(SetDivL(initial_meta_state,&m_nonObservable,&m_tb_relation)); + initalAggregate->setDeadLock(Set_Bloc(initial_meta_state)); // Compute successors unsigned int onb_it=0; - Set::const_iterator iter=fire.begin(); + Set::iterator iter=fire.begin(); while(iter!=fire.end()) { int t = *iter; - SPAWN(Aggregate_epsilon_lace,get_successor(initial_meta_state,t),&m_nonObservable,&m_tb_relation); onb_it++; iter++; } - + MDD Complete_meta_state; for (unsigned int i=0; i<onb_it; i++) { Set::iterator it = fire.end(); it--; int t=*it; fire.erase(it); - MDD Complete_meta_state=SYNC(Aggregate_epsilon_lace); - reached_class=new LDDState; + Complete_meta_state=SYNC(Aggregate_epsilon_lace); + reached_class=new LDDState(); reached_class->m_lddstate=Complete_meta_state; reached_class->setDiv(SetDivL(Complete_meta_state,&m_nonObservable,&m_tb_relation)); m_graph->addArc(); @@ -231,18 +232,18 @@ LDDState * ModelCheckLace::getInitialMetaState() reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(initalAggregate,t)); } - return initalAggregate; + return m_graph->getInitialState(); } void ModelCheckLace::buildSucc(LDDState *agregate) { - + if (!agregate->isVisited()) { // It's first time to visit agregate, then we have to build its successors agregate->setVisited(); LDDState *reached_class=nullptr; LACE_ME; - MDD meta_state(CALL(Aggregate_epsilon_lace,agregate->getLDDValue(),&m_nonObservable,&m_tb_relation)); + MDD meta_state=agregate->getLDDValue();//(CALL(Aggregate_epsilon_lace,agregate->getLDDValue(),&m_nonObservable,&m_tb_relation)); Set fire=fire_obs_lace(meta_state,&m_observable,&m_tb_relation); unsigned int onb_it=0; @@ -261,13 +262,14 @@ void ModelCheckLace::buildSucc(LDDState *agregate) int t=*it; fire.erase(it); MDD Complete_meta_state=SYNC(Aggregate_epsilon_lace); - reached_class=new LDDState; + reached_class=new LDDState(); reached_class->m_lddstate=Complete_meta_state; LDDState* pos=m_graph->find(reached_class); if(!pos) { reached_class->setDiv(SetDivL(Complete_meta_state,&m_nonObservable,&m_tb_relation)); + reached_class->setDeadLock(Set_Bloc(Complete_meta_state)); m_graph->addArc(); m_graph->insert(reached_class); agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(reached_class,t)); diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h index e77ee39..00437d3 100644 --- a/src/ModelCheckLace.h +++ b/src/ModelCheckLace.h @@ -4,8 +4,8 @@ class ModelCheckLace : public ModelCheckBaseMT { public: ModelCheckLace(const NewNet &R, int BOUND,int nbThread); - LDDState * getInitialMetaState(); - void buildSucc(LDDState *agregate); + LDDState * getInitialMetaState() override; + void buildSucc(LDDState *agregate) override; private: void preConfigure(); diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp index 55a4d37..698815d 100644 --- a/src/ModelCheckerTh.cpp +++ b/src/ModelCheckerTh.cpp @@ -108,8 +108,6 @@ void ModelCheckerTh::preConfigure() LDDState * ModelCheckerTh::getInitialMetaState() { - cout<<"**********************************"<<endl; - while (!m_finish_initial); LDDState *initial_metastate=m_graph->getInitialState(); if (!initial_metastate->isVisited()) { @@ -264,18 +262,13 @@ void * ModelCheckerTh::Compute_successors() e.first.first->setCompletedSucc(); } m_terminaison[id_thread]=true; - - - } while (isNotTerminated() && !m_finish); - cout<<"Thread id :"<<id_thread<<endl; + //cout<<"Thread id :"<<id_thread<<endl; pthread_barrier_wait(&m_barrier_builder); } - - void * ModelCheckerTh::threadHandler(void *context) { return ((ModelCheckerTh*)context)->Compute_successors(); @@ -319,7 +312,7 @@ void ModelCheckerTh::ComputeTh_Succ() ModelCheckerTh::~ModelCheckerTh() { m_finish=true; - cout<<__func__<<endl; + pthread_barrier_wait(&m_barrier_builder); for (int i = 0; i < m_nb_thread; i++) { diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp index 7385566..4862d60 100644 --- a/src/SogKripkeIteratorTh.cpp +++ b/src/SogKripkeIteratorTh.cpp @@ -6,9 +6,6 @@ SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd) { - - //m_lddstate->setDiv(true); - //if (m_lddstate->getLDDValue()) m_lddstate->setDeadLock(true); for (int i=0;i<m_lddstate->getSuccessors()->size();i++) { m_lsucc.push_back(m_lddstate->getSuccessors()->at(i)); } @@ -30,7 +27,7 @@ bool SogKripkeIteratorTh::first() { } bool SogKripkeIteratorTh::next() { - //cout<<"entering "<<__func__<<endl; + //cout<<"entering "<<__func__<<" "<<m_current_edge<<endl; m_current_edge++; return m_current_edge<m_lsucc.size(); @@ -44,7 +41,7 @@ bool SogKripkeIteratorTh::done() const { SogKripkeStateTh* SogKripkeIteratorTh::dst() const { - //cout<<"enter/excit "<<__func__<<endl; + /*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); } @@ -71,6 +68,12 @@ 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; diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h index 938803d..c5307b4 100644 --- a/src/SogKripkeIteratorTh.h +++ b/src/SogKripkeIteratorTh.h @@ -22,11 +22,11 @@ public: SogKripkeStateTh* current_state() const; - bdd current_condition() const; + void recycle(LDDState *aggregate, bdd cond); - int current_transition() const; + //int current_transition() const; - bdd current_acceptance_conditions() const; + //bdd current_acceptance_conditions() const; std::string format_transition() const; diff --git a/src/SogKripkeStateTh.cpp b/src/SogKripkeStateTh.cpp index 76c3884..70712c9 100644 --- a/src/SogKripkeStateTh.cpp +++ b/src/SogKripkeStateTh.cpp @@ -8,4 +8,4 @@ SogKripkeStateTh::~SogKripkeStateTh() //dtor } -static ModelCheckerTh * SogKripkeStateTh::m_builder; +static ModelCheckBaseMT * SogKripkeStateTh::m_builder; diff --git a/src/SogKripkeStateTh.h b/src/SogKripkeStateTh.h index 48d64ff..f07ab07 100644 --- a/src/SogKripkeStateTh.h +++ b/src/SogKripkeStateTh.h @@ -3,12 +3,12 @@ #include "LDDState.h" -#include "ModelCheckerTh.h" +#include "ModelCheckBaseMT.h" class SogKripkeStateTh : public spot::state { public: - static ModelCheckerTh * m_builder; + static ModelCheckBaseMT * m_builder; SogKripkeStateTh(LDDState *st):m_state(st) { m_builder->buildSucc(st); }; @@ -28,6 +28,7 @@ public: 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 diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp index abb3693..d2884fa 100644 --- a/src/SogKripkeTh.cpp +++ b/src/SogKripkeTh.cpp @@ -36,8 +36,8 @@ SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *bu state* SogKripkeTh::get_init_state() const { - // cout<<__func__<<endl; - return new SogKripkeStateTh(m_builder->getInitialMetaState());//new SpotSogState(); + LDDState *ss=m_builder->getInitialMetaState(); + return new SogKripkeStateTh(ss);//new SpotSogState(); } // Allows to print state label representing its id @@ -52,12 +52,26 @@ std::string SogKripkeTh::format_state(const spot::state* s) const } SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const { - // cout<<__func__<<endl; - + 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)); + return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));*/ } bdd SogKripkeTh::state_condition(const spot::state* s) const diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h index 81d27eb..46c06ce 100644 --- a/src/SogKripkeTh.h +++ b/src/SogKripkeTh.h @@ -13,16 +13,12 @@ class SogKripkeTh: public spot::kripke { 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; + 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; - /// \brief Get the graph associated to the automaton. - /* const LDDGraph& get_graph() const { - return *m_sog; - }*/ - ModelCheckerTh *m_builder; + ModelCheckBaseMT *m_builder; protected: diff --git a/src/main.cpp b/src/main.cpp index ae3018b..adb7c2f 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -154,10 +154,14 @@ int main(int argc, char** argv) if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(R,bound,nb_th); else mcl=new ModelCheckerTh(R,bound,nb_th); - mcl->loadNet(); + mcl->loadNet(); + auto k = std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); - /* cout<<"Want to save the graph in a dot file ?"; + /* spot::twa_graph_ptr k = + spot::make_twa_graph(std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()), + spot::twa::prop_set::all(), true);*/ + /* cout<<"Want to save the graph in a dot file ?"; cin>>c; if (c=='y') { @@ -167,8 +171,9 @@ int main(int argc, char** argv) file.open(st.c_str(),fstream::out); spot::print_dot(file, k,"ka"); file.close(); - } */ ; - // Performing on the fly Modelchecking + } + mcl->getGraph()->printCompleteInformation(); + // Performing on the fly Modelchecking*/ cout<<"Performing on the fly Modelchecking"<<endl; if (auto run = k->intersecting_run(af)) @@ -185,6 +190,8 @@ int main(int argc, char** argv) } else std::cout << "formula is verified\n"; + //cin>>c; + //mcl->getGraph()->printCompleteInformation(); delete mcl; } else if (n_tasks==1) -- GitLab