From ab593e5b4550750e651505f8a748723c0376e7a5 Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Thu, 18 Jul 2019 01:11:14 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/CommonSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?= =?UTF-8?q?=20=20=20src/HybridKripke.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20?= =?UTF-8?q?=20=20=20=20=20=20src/HybridKripkeIterator.cpp=20=09modifi?= =?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/HybridKripkeIterato?= =?UTF-8?q?r.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/Hybr?= =?UTF-8?q?idKripkeState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?= =?UTF-8?q?=20=20src/MCHybridSOG.cpp?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/.HybridKripkeState.h.kate-swp | Bin 0 -> 290 bytes src/CommonSOG.cpp | 1 - src/HybridKripke.cpp | 13 +++++++------ src/HybridKripkeIterator.cpp | 12 +++++++++--- src/HybridKripkeIterator.h | 3 ++- src/HybridKripkeState.h | 20 +++++++++++--------- src/MCHybridSOG.cpp | 8 +++++--- 7 files changed, 34 insertions(+), 23 deletions(-) create mode 100644 src/.HybridKripkeState.h.kate-swp diff --git a/src/.HybridKripkeState.h.kate-swp b/src/.HybridKripkeState.h.kate-swp new file mode 100644 index 0000000000000000000000000000000000000000..779eacdfc4dc852635675663db21ac8d1f87d37e GIT binary patch literal 290 zcmZQzU=Z?7EJ;-eE>A2_aLdd|RWQ;sU|?Vn3BTKY_r#NnwGZ7IO6y}U@v1prQV$Mi zU|=v}U|^7O4fbSUU@&HY02T!W1qFl<3j+fKV=02q3gTxX_-r749)iyf;+MDv2SJSl z>F0o%59X9+=9L&5#g`!T@PPCn*~tsy=OX0!K>T<FpC808K=1`X{Coso5X3J=@P$Bp IYu8{`0HfL|I{*Lx literal 0 HcmV?d00001 diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp index 6b570d2..498a6d4 100644 --- a/src/CommonSOG.cpp +++ b/src/CommonSOG.cpp @@ -20,7 +20,6 @@ MDD CommonSOG::Accessible_epsilon(MDD From) { MDD M1; MDD M2=From; - do { M1=M2; diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp index 27c1e4d..3770bab 100644 --- a/src/HybridKripke.cpp +++ b/src/HybridKripke.cpp @@ -49,11 +49,12 @@ state* HybridKripke::get_init_state() const { MPI_Get_count(&status, MPI_UNSIGNED_CHAR, &v); cout<<" Message size : "<<v<<endl; MPI_Recv(message, 17, MPI_UNSIGNED_CHAR,MPI_ANY_SOURCE,TAG_ACK_INITIAL,MPI_COMM_WORLD, &status); - message[17]='\0'; + message[17]='\0'; cout<<"Message received : "<<message<<endl; - string id(message+1); + + uint16_t p_container=message[0]; - return new HybridKripkeState(id,p_container); + return new HybridKripkeState(message+1,p_container); } // Allows to print state label representing its id @@ -62,7 +63,7 @@ std::string HybridKripke::format_state(const spot::state* s) const //cout<<__func__<<endl; auto ss = static_cast<const HybridKripkeState*>(s); std::ostringstream out; - out << "( " << ss->getLDDState()->getLDDValue() << ")"; + out << "( " << ss->getId() << ")"; // cout << " ( " << ss->getLDDState()->getLDDValue() << ")"; return out.str(); } @@ -70,7 +71,7 @@ std::string HybridKripke::format_state(const spot::state* s) const HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const { auto ss = static_cast<const HybridKripkeState*>(s); - LDDState *aggregate=ss->getLDDState(); + LDDState *aggregate;//=ss->getLDDState(); bdd cond = state_condition(ss); if (iter_cache_) { @@ -79,7 +80,7 @@ HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const { it->recycle(aggregate, cond); return it; } - return new HybridKripkeIterator(aggregate,cond); + return new HybridKripkeIterator(*ss,cond); diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp index 7a49bf3..b7cc6c3 100644 --- a/src/HybridKripkeIterator.cpp +++ b/src/HybridKripkeIterator.cpp @@ -2,10 +2,13 @@ #include "LDDGraph.h" #include "HybridKripkeState.h" #include "HybridKripkeIterator.h" +#define TAG_ASK_SUCC 4 - -HybridKripkeIterator::HybridKripkeIterator(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd) +HybridKripkeIterator::HybridKripkeIterator(const HybridKripkeState &kstate, bdd cnd):m_current_state(&kstate), kripke_succ_iterator(cnd) { + LDDState* lddstate; + cout<<"Send ask container"<<endl; + MPI_Send(m_current_state->getId(),16,MPI_UNSIGNED_CHAR,m_current_state->getContainerProcess(), TAG_ASK_SUCC, MPI_COMM_WORLD); for (int i=0;i<m_lddstate->getSuccessors()->size();i++) { m_lsucc.push_back(m_lddstate->getSuccessors()->at(i)); } @@ -43,7 +46,7 @@ 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 HybridKripkeState(m_lsucc.at(m_current_edge).first); - string id; + char* id; uint16_t p_container; return new HybridKripkeState(id,p_container); // return new HybridKripkeState(m_lsucc.at(m_current_edge).first); @@ -78,6 +81,9 @@ void HybridKripkeIterator::recycle(LDDState* aggregate, bdd cond) spot::kripke_succ_iterator::recycle(cond); } +HybridKripkeState* HybridKripkeIterator::current_state() const { + return m_current_state; +} static ModelCheckBaseMT * HybridKripkeIterator::m_builder; static spot::bdd_dict_ptr* HybridKripkeIterator::m_dict_ptr; static LDDState HybridKripkeIterator::m_deadlock; diff --git a/src/HybridKripkeIterator.h b/src/HybridKripkeIterator.h index a4e5d85..17a81d3 100644 --- a/src/HybridKripkeIterator.h +++ b/src/HybridKripkeIterator.h @@ -12,7 +12,7 @@ public: 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); + HybridKripkeIterator(const HybridKripkeState &kstate, bdd cnd); virtual ~HybridKripkeIterator(); bool first() override; bool next() override; @@ -28,6 +28,7 @@ public: std::string format_transition() const; private: + HybridKripkeState *m_current_state; LDDState * m_lddstate; vector<pair<LDDState*, int>> m_lsucc; unsigned int m_current_edge=0; diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h index a286ee9..57dd8bd 100644 --- a/src/HybridKripkeState.h +++ b/src/HybridKripkeState.h @@ -4,18 +4,17 @@ #include <mpi.h> #include "LDDState.h" #include "ModelCheckBaseMT.h" -#define TAG_ASK_SUCC 4 + class HybridKripkeState : public spot::state { public: static ModelCheckBaseMT * m_builder; - HybridKripkeState(string &id,uint16_t pcontainer):m_id(id),m_container(pcontainer) { - int v=1; - MPI_Send( &v, 1, MPI_INT, m_container, TAG_ASK_SUCC, MPI_COMM_WORLD); - + HybridKripkeState(unsigned char * id,uint16_t pcontainer):m_container(pcontainer) { + memcpy(m_id,id,16); }; // Constructor for cloning - HybridKripkeState(const string &id,uint16_t pcontainer,bool ddiv, bool deadlock):m_id(id),m_container(pcontainer),m_div(ddiv),m_deadlock(deadlock) { + HybridKripkeState(unsigned char *id,uint16_t pcontainer,bool ddiv, bool deadlock):m_container(pcontainer),m_div(ddiv),m_deadlock(deadlock) { + memcpy(m_id,id,16); } virtual ~HybridKripkeState(); @@ -39,14 +38,17 @@ public: else return h > oh; } - LDDState* getLDDState() { - return m_state; + unsigned char * getId() { + return m_id; + } + uint16_t getContainerProcess() { + return m_container; } protected: private: LDDState *m_state; - string m_id; + unsigned char m_id[16]; bool m_div; bool m_deadlock; uint16_t m_container; diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp index e7e872f..6b07f6d 100644 --- a/src/MCHybridSOG.cpp +++ b/src/MCHybridSOG.cpp @@ -487,16 +487,18 @@ void MCHybridSOG::read_message() LDDState *i_agregate=m_graph->getInitialState(); stringstream ss; - ss<<(task_id); + ss<<(task_id);ss<<'\0'; ss<<i_agregate->getSHAValue(); cout<<"Ldd Value :"<<i_agregate->getLDDValue()<<endl; - cout<<"string :"<<ss.str()<<endl; + cout<<"string :"<<ss.str()<<endl; + MPI_Send(ss.str().c_str(),17,MPI_UNSIGNED_CHAR,m_status.MPI_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD); break; case TAG_ASK_SUCC : int id; MPI_Recv(&id, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status); - LDDState *aggregate=m_graph->getLDDStateById(id); + // LDDState *aggregate=m_graph->findSHA() + // Send successors break; case TAG_AGREGATE : break; default : //cout<<"unknown received "<<status.MPI_TAG<<" by task "<<task_id<<endl; -- GitLab