diff --git a/src/.HybridKripkeState.h.kate-swp b/src/.HybridKripkeState.h.kate-swp
new file mode 100644
index 0000000000000000000000000000000000000000..779eacdfc4dc852635675663db21ac8d1f87d37e
Binary files /dev/null and b/src/.HybridKripkeState.h.kate-swp differ
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 6b570d2a5446aeb66b4e0378194613e26980bd83..498a6d400c268c974848be3e3eb3c19229292171 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 27c1e4db0c230e9d28ab0c967fa39222febf8023..3770bab909ce8753db8d1906cabc55782d3693b7 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 7a49bf3509096a3974b3e89b62705d81e3c241f2..b7cc6c33086cfb455d3df892d948e3f27498ed4d 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 a4e5d85fb6079254517d898ca4df6fd33f6bd45b..17a81d346e9d536b6d99dc0627d9d18ab54f4e63 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 a286ee994a9f6f3b90081691c9176fb628f30d4a..57dd8bddc8e4d17de14680757f5dd20d2643d227 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 e7e872f4f9540192b6c11441e3966458a8a83bc7..6b07f6d31b25f486ddac6d15abb3f223f478ea37 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;