diff --git a/src/.HybridKripkeState.h.kate-swp b/src/.HybridKripkeState.h.kate-swp
deleted file mode 100644
index 779eacdfc4dc852635675663db21ac8d1f87d37e..0000000000000000000000000000000000000000
Binary files a/src/.HybridKripkeState.h.kate-swp and /dev/null differ
diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index 3770bab909ce8753db8d1906cabc55782d3693b7..ee4946682b092bac07f00e920d42b994dccfa087 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -9,25 +9,27 @@
#include "HybridKripke.h"
#include <map>
+#define TAG_FINISH 2
#define TAG_INITIAL 3
#define TAG_ACK_INITIAL 8
using namespace spot;
HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr): spot::kripke(dict_ptr)
{
-
+ cout<<__func__<<endl;
HybridKripkeIterator::m_dict_ptr=&dict_ptr;
- HybridKripkeIterator::m_deadlock.setLDDValue(1);
+ /*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));
+ HybridKripkeIterator::m_div.Successors.push_back(pair<LDDState*,int>(&HybridKripkeIterator::m_div,-1));*/
}
-HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap):HybridKripke(dict_ptr) {
-
+HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap,NewNet &net_):HybridKripke(dict_ptr) {
+ m_net=&net_;
+ HybridKripkeIterator::m_net=&net_;
for (auto it=l_transap.begin();it!=l_transap.end();it++) {
register_ap(*it);
}
@@ -40,47 +42,47 @@ HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_tra
state* HybridKripke::get_init_state() const {
- // LDDState *ss=m_builder->getInitialMetaState();
+
+
int v;
MPI_Send( &v, 1, MPI_INT, 0, TAG_INITIAL, MPI_COMM_WORLD);
- char message[18];
+ char message[23];
MPI_Status status; int nbytes;
MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD, &status);
- 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';
- cout<<"Message received : "<<message<<endl;
+ MPI_Get_count(&status, MPI_BYTE, &v);
+ MPI_Recv(message, 22, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_INITIAL,MPI_COMM_WORLD, &status);
+ char id[16];
+ memcpy(id,message,16);
-
- uint16_t p_container=message[0];
- return new HybridKripkeState(message+1,p_container);
+ uint16_t p_container;
+ memcpy(&p_container,message+16,2);
+ return new HybridKripkeState(id,p_container);
}
// Allows to print state label representing its id
std::string HybridKripke::format_state(const spot::state* s) const
{
- //cout<<__func__<<endl;
+ cout<<__func__<<endl;
auto ss = static_cast<const HybridKripkeState*>(s);
std::ostringstream out;
- out << "( " << ss->getId() << ")";
- // cout << " ( " << ss->getLDDState()->getLDDValue() << ")";
+ out << "( " << ss->hash() << ")";
+
return out.str();
}
HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
-
+ cout<<__func__<<endl;
auto ss = static_cast<const HybridKripkeState*>(s);
- LDDState *aggregate;//=ss->getLDDState();
+ HybridKripkeState *aggregate=ss;
bdd cond = state_condition(ss);
if (iter_cache_)
{
auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
- it->recycle(aggregate, cond);
+ it->recycle(ss, cond);
return it;
}
- return new HybridKripkeIterator(*ss,cond);
+ return new HybridKripkeIterator(*aggregate,cond);
@@ -93,19 +95,19 @@ HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
bdd HybridKripke::state_condition(const spot::state* s) const
{
-
+
auto ss = static_cast<const HybridKripkeState*>(s);
- //vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
+ set<uint16_t> marked_place=ss->getMarkedPlaces();
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=marked_place.begin();it!=marked_place.end();it++) {
+ string name=m_net->getPlaceName(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+ set<uint16_t> unmarked_place=ss->getUnmarkedPlaces();
//for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
/*string name=m_builder->getPlace(*it);
spot::formula f=spot::formula::ap(name);
@@ -118,6 +120,12 @@ bdd HybridKripke::state_condition(const spot::state* s) const
HybridKripke::~HybridKripke()
{
- //dtor
+ int world_size;
+ MPI_Comm_size(MPI_COMM_WORLD, &world_size);
+ int i,v;
+ for (i = 0; i < world_size-1; i++) {
+ MPI_Send( &v, 1, MPI_INT, i, TAG_FINISH, MPI_COMM_WORLD);
+ }
+
}
diff --git a/src/HybridKripke.h b/src/HybridKripke.h
index 273fe216e80d70e3dd70ce4e61b489990e65e31c..d8caeb85d1c1f577816fd1038b50ac3b73239cea 100644
--- a/src/HybridKripke.h
+++ b/src/HybridKripke.h
@@ -11,7 +11,7 @@ class HybridKripke: public spot::kripke {
public:
HybridKripke(const spot::bdd_dict_ptr& dict_ptr);
- HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap);
+ HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap,NewNet &net_);
virtual ~HybridKripke();
spot::state* get_init_state() const override;
HybridKripkeIterator* succ_iter(const spot::state* s) const override;
@@ -24,7 +24,7 @@ class HybridKripke: public spot::kripke {
private:
std::map<int, int> place_prop;
- //LDDGraph* m_sog;
+ NewNet *m_net;
};
#endif // SOGKRIPKE_H_INCLUDED
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index b7cc6c33086cfb455d3df892d948e3f27498ed4d..0c7f4bf226a7e33b9c5e22dc1b579565c695348d 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -3,61 +3,85 @@
#include "HybridKripkeState.h"
#include "HybridKripkeIterator.h"
#define TAG_ASK_SUCC 4
+#define TAG_ACK_SUCC 11
+#define TAG_NOTCOMPLETED 20
-HybridKripkeIterator::HybridKripkeIterator(const HybridKripkeState &kstate, bdd cnd):m_current_state(&kstate), kripke_succ_iterator(cnd)
+HybridKripkeIterator::HybridKripkeIterator(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));
+ cout<<__func__<<endl;
+ // Ask list of successors
+ MPI_Send(m_current_state->getId(),16,MPI_BYTE,m_current_state->getContainerProcess(), TAG_ASK_SUCC, MPI_COMM_WORLD);
+ cout<<"Container process to ask :"<<m_current_state->getContainerProcess()<<endl;
+ // Receive list of successors
+
+ MPI_Status status;
+ MPI_Probe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&status);
+ uint32_t nbytes;
+ MPI_Get_count(&status, MPI_BYTE, &nbytes);
+ char inmsg[nbytes+1];
+ cout<<"Received bytes : "<<nbytes<<endl;
+ MPI_Recv(inmsg, nbytes, MPI_BYTE,status.MPI_SOURCE,TAG_ACK_SUCC,MPI_COMM_WORLD, &status);
+ uint32_t nb_succ;
+ memcpy(&nb_succ,inmsg,4);
+ cout<<"Number of successors : "<<nb_succ<<endl;
+ uint32_t indice=4;
+ for (uint32_t i=0;i<nb_succ;i++) {
+ succ_t succ_elt;
+
+ memcpy(succ_elt.id,inmsg+indice,16);
+ indice+=16;
+
+ memcpy(&(succ_elt.pcontainer),inmsg+indice,2);
+ indice+=2;
+ memcpy(&(succ_elt.transition),inmsg+indice,2);
+ indice+=2;
+
+ m_succ.push_back(succ_elt);
}
- if (lddstate->isDeadLock()) {
+
+ /*if (lddstate->isDeadLock()) {
m_lsucc.push_back(pair<LDDState*,int>(&m_deadlock,-1));
}
if (lddstate->isDiv()) {
m_lsucc.push_back(pair<LDDState*,int>(&m_div,-1));
- }
+ }*/
}
bool HybridKripkeIterator::first() {
- // cout<<"entering "<<__func__<<endl;
+ cout<<"entering "<<__func__<<endl;
m_current_edge=0;
- //cout<<"exciting "<<__func__<<endl;
- return m_lsucc.size()!=0;
+
+ return m_succ.size()!=0;
}
bool HybridKripkeIterator::next() {
- //cout<<"entering "<<__func__<<" "<<m_current_edge<<endl;
+
m_current_edge++;
- return m_current_edge<m_lsucc.size();
+ return m_current_edge<m_succ.size();
}
bool HybridKripkeIterator::done() const {
- //cout<<"entring /excit"<<__func__<<endl;
- return m_current_edge==m_lsucc.size();
-
+ cout<<"entring /excit"<<__func__<<endl;
+ return m_current_edge==m_succ.size();
}
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);
- char* id;
- uint16_t p_container;
- return new HybridKripkeState(id,p_container);
- // return new HybridKripkeState(m_lsucc.at(m_current_edge).first);
+ succ_t succ_elt= m_succ.at(m_current_edge);
+ return new HybridKripkeState(succ_elt.id,succ_elt.pcontainer);
+
}
bdd HybridKripkeIterator::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;
+ cout<<"entering "<<__func__<<endl;
+ succ_t succ_elt=m_succ.at(m_current_edge);
+
+ if (succ_elt.transition==-1) return bddtrue;
+
+ string name=m_net->getTransitionName(succ_elt.transition);
spot::bdd_dict *p=m_dict_ptr->get();
spot::formula f=spot::formula::ap(name);
@@ -72,19 +96,21 @@ bdd HybridKripkeIterator::cond() const {
}*/
HybridKripkeIterator::~HybridKripkeIterator()
{
- //dtor
+
}
-void HybridKripkeIterator::recycle(LDDState* aggregate, bdd cond)
+void HybridKripkeIterator::recycle(HybridKripkeState* aggregate, bdd cond)
{
- m_lddstate=aggregate;
+ cout<<__func__<<endl;
+ m_current_state=aggregate;
spot::kripke_succ_iterator::recycle(cond);
}
-HybridKripkeState* HybridKripkeIterator::current_state() const {
+/*HybridKripkeState* HybridKripkeIterator::current_state() const {
+ cout<<__func__<<endl;
return m_current_state;
-}
-static ModelCheckBaseMT * HybridKripkeIterator::m_builder;
+}*/
+static NewNet * HybridKripkeIterator::m_net;
static spot::bdd_dict_ptr* HybridKripkeIterator::m_dict_ptr;
static LDDState HybridKripkeIterator::m_deadlock;
static LDDState HybridKripkeIterator::m_div;
diff --git a/src/HybridKripkeIterator.h b/src/HybridKripkeIterator.h
index 17a81d346e9d536b6d99dc0627d9d18ab54f4e63..720b4ea122f43b27d5c60ca7797c24a6d7eafd9e 100644
--- a/src/HybridKripkeIterator.h
+++ b/src/HybridKripkeIterator.h
@@ -4,15 +4,20 @@
#include "ModelCheckBaseMT.h"
#include <spot/kripke/kripke.hh>
// Iterator for a SOG graph
+typedef struct {
+ char id[17];
+ int16_t transition;
+ uint16_t pcontainer;
+} succ_t;
class HybridKripkeIterator : public spot::kripke_succ_iterator
{
public:
static LDDState m_deadlock;
static LDDState m_div;
- static ModelCheckBaseMT * m_builder;
+ static NewNet * m_net;
static spot::bdd_dict_ptr* m_dict_ptr;
// sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
- HybridKripkeIterator(const HybridKripkeState &kstate, bdd cnd);
+ HybridKripkeIterator(HybridKripkeState &kstate, bdd cnd);
virtual ~HybridKripkeIterator();
bool first() override;
bool next() override;
@@ -20,18 +25,20 @@ public:
HybridKripkeState* dst() const override;
bdd cond() const override final;
- HybridKripkeState* current_state() const;
+ // HybridKripkeState* current_state() const;
- void recycle(LDDState *aggregate, bdd cond);
+ void recycle(HybridKripkeState *aggregate, bdd cond);
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;
+ vector<succ_t> m_succ;
};
diff --git a/src/HybridKripkeState.cpp b/src/HybridKripkeState.cpp
index 31dd140aa3b194166fc6cac92b71ba4d525a6081..9c2e02ffd800cb2dd52e1b4b5e5be30d20e97393 100644
--- a/src/HybridKripkeState.cpp
+++ b/src/HybridKripkeState.cpp
@@ -6,6 +6,7 @@
HybridKripkeState::~HybridKripkeState()
{
//dtor
+ cout<<__func__<<endl;
}
-static ModelCheckBaseMT * HybridKripkeState::m_builder;
+//static ModelCheckBaseMT * HybridKripkeState::m_builder;
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index 57dd8bddc8e4d17de14680757f5dd20d2643d227..0ed7af28cfcb9f65aa7d5cddd9b66e0bb4bb6a48 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -4,31 +4,52 @@
#include <mpi.h>
#include "LDDState.h"
#include "ModelCheckBaseMT.h"
-
+#define TAG_ASK_STATE 9
+#define TAG_ACK_STATE 10
class HybridKripkeState : public spot::state
{
public:
- static ModelCheckBaseMT * m_builder;
+ //static ModelCheckBaseMT * m_builder;
HybridKripkeState(unsigned char * id,uint16_t pcontainer):m_container(pcontainer) {
- memcpy(m_id,id,16);
- };
- // Constructor for cloning
- HybridKripkeState(unsigned char *id,uint16_t pcontainer,bool ddiv, bool deadlock):m_container(pcontainer),m_div(ddiv),m_deadlock(deadlock) {
+ cout<<__func__<<"pcontainer :"<<pcontainer<<endl;
memcpy(m_id,id,16);
+
+ MPI_Send(m_id,16,MPI_BYTE,pcontainer, TAG_ASK_STATE, MPI_COMM_WORLD);
+
+
+ char message[9];
+ MPI_Status status; //int nbytes;
+ MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_STATE, MPI_COMM_WORLD, &status);
+ cout<<"ACK state received..."<<endl;
+ MPI_Recv(message, 8, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_STATE,MPI_COMM_WORLD, &status);
+ memcpy(&m_hashid,message,8);
+ m_hashid=m_hashid | (size_t(m_container)<<56);
+
+
+ }
+ // Constructor for cloning
+ HybridKripkeState(unsigned char *id,uint16_t pcontainer,size_t hsh,bool ddiv, bool deadlock):m_container(pcontainer),m_div(ddiv),m_deadlock(deadlock),m_hashid(hsh) {
+ memcpy(m_id,id,16);
+
+ cout<<__func__<<endl;
+
}
virtual ~HybridKripkeState();
HybridKripkeState* clone() const override
{
- return new HybridKripkeState(m_id,m_container,m_div,m_deadlock);
+ cout<<__func__<<endl;
+ return new HybridKripkeState(m_id,m_container,m_hashid,m_div,m_deadlock);
}
size_t hash() const override
{
- return m_state->getLDDValue();
+ cout<<__func__<<m_hashid<<endl;
+ return m_hashid;
}
int compare(const spot::state* other) const override
{
+ cout<<__func__<<endl;
auto o = static_cast<const HybridKripkeState*>(other);
size_t oh = o->hash();
size_t h = hash();
@@ -39,19 +60,27 @@ public:
return h > oh;
}
unsigned char * getId() {
+ cout<<__func__<<endl;
return m_id;
}
uint16_t getContainerProcess() {
+ cout<<__func__<<endl;
return m_container;
}
+ set<uint16_t> & getMarkedPlaces() { return m_marked_places;}
+ set<uint16_t> & getUnmarkedPlaces() { return m_unmarked_places;}
protected:
private:
- LDDState *m_state;
- unsigned char m_id[16];
+ //LDDState *m_state;
+ char m_id[17];
+ uint32_t m_pos;
+ size_t m_hashid;
bool m_div;
bool m_deadlock;
uint16_t m_container;
+ set<uint16_t> m_marked_places;
+ set<uint16_t> m_unmarked_places;
};
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index 4cb6537fda0836dc6be9a964dfb3e365f7eed725..cf0829b14303e1e64cb49b48d07770c59a2bccac 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -44,7 +44,19 @@ LDDState * LDDGraph::findSHA(unsigned char* c)
return *i;
return NULL;
}
-
+/*--------------------------------------------*/
+size_t LDDGraph::findSHAPos(unsigned char* c,bool &res)
+{
+ size_t i=0;
+ res=false;
+ for(i=0;i<m_GONodes.size();i++)
+ if((cmpSHA(c,m_GONodes.at(i)->m_SHA2)==0)) {
+ res=true;
+ return i;
+ }
+ // cout<<__func__<<" : Aggregate not found!!!"<<endl;
+ return i;
+}
/*----------------------insert() ------------*/
void LDDGraph::insert(LDDState *c)
@@ -110,7 +122,7 @@ void LDDGraph::printCompleteInformation()
//InitVisit(initialstate,n);
size_t n=1;
- //cout<<"NB BDD NODE : "<<NbBddNode(initialstate,n)<<endl;
+ //cout<<"NB BDD NODE : "<<NbBdm_current_state->getContainerProcess()dNode(initialstate,n)<<endl;
NbBddNode(m_initialstate,n);
// cout<<"NB BDD NODE : "<<bdd_anodecount(m_Tab,(int)m_nbStates)<<endl;
//cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index 9c027cece4d3916bc6f2efa970029fd2ed5a7795..891eaf6fc23d4f67efe4928a93610167f1c73083 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -34,6 +34,7 @@ class LDDGraph
long m_nbArcs;
LDDState* find(LDDState*);
LDDState* findSHA(unsigned char*);
+ size_t findSHAPos(unsigned char*,bool &res);
bool cmpSHA(const unsigned char *s1, const unsigned char *s2);
void insertSHA(LDDState *c);
LDDEdges& get_successor(LDDState*);
diff --git a/src/LDDState.h b/src/LDDState.h
index 59ba7ef0242a7b7c669ec95127f0c042ef854516..e59e7195b46c5ffd15e3ca407376e4ef1d3276fc 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -43,13 +43,14 @@ class LDDState {
bool isCompletedSucc() {return m_completed;}
vector<int> getMarkedPlaces(set<int>& lplacesAP);
vector<int> getUnmarkedPlaces(set<int>& lplacesAP);
-
+ void setProcess(uint16_t v) {m_process=v;}
+ uint16_t getProcess() {return m_process;}
protected:
private:
bool m_virtual = false;
bool m_visited=false;
bool m_completed=false;
-
+ uint16_t m_process=0;
};
typedef pair<LDDState*, int> LDDEdge;
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 6b07f6d31b25f486ddac6d15abb3f223f478ea37..9ca13560fece90bb9653c9338b5c9f81f7366774 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -20,6 +20,10 @@ using namespace sylvan;
#define TAG_AGREGATE 5
#define TAG_ACK_INITIAL 8
+#define TAG_ASK_STATE 9
+#define TAG_ACK_STATE 10
+#define TAG_ACK_SUCC 11
+#define TAG_NOTCOMPLETED 20
MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world, int BOUND,bool init)
{
@@ -129,7 +133,7 @@ void *MCHybridSOG::doCompute()
unsigned char Identif[20];
m_Terminated=false;
- m_Terminating=false;
+
/****************************************** initial state ********************************************/
if (task_id==0 && id_thread==0)
{
@@ -146,7 +150,7 @@ void *MCHybridSOG::doCompute()
get_md5(*chaine,Identif);
//lddmc_getsha(Complete_meta_state, Identif);
int destination=(int)(Identif[0]%n_tasks);
-
+ c->setProcess(destination);
if(destination==0)
{
@@ -156,7 +160,7 @@ void *MCHybridSOG::doCompute()
m_graph->setInitialState(c);
m_graph->insert(c);
m_charge[1]++;
- strcpySHA(c->m_SHA2,Identif);
+ memcpy(c->m_SHA2,Identif,16);
}
else
{
@@ -199,8 +203,39 @@ void *MCHybridSOG::doCompute()
{
send_state_message();
read_message();
+ if (m_waitingBuild) {
+ bool res;
+ size_t pos=m_graph->findSHAPos(m_id_md5,res);
+ if (res) {
+ m_waitingBuild=false;
+ m_aggWaiting=m_graph->getLDDStateById(pos);
+ m_waitingSucc=true;
+ cout<<"Get build..."<<endl;
+ }
+
+ }
+ if (m_waitingSucc) {
+
+ if (m_aggWaiting->isCompletedSucc()) {
+ cout<<"Get succ..."<<endl;
+ m_waitingSucc=false;
+ sendSuccToMC();
+ }
+ }
+ if (m_waitingAgregate) {
+ bool res;
+ size_t pos=m_graph->findSHAPos(m_id_md5,res);
+ //cout<<"Not found..."<<endl;
+ if (res) {
+ m_waitingAgregate=false;
+ char mess[9];
+ memcpy(mess,&pos,8);
+ MPI_Send(mess,8,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD);
+
+ }
+ }
}
- while (isNotTerminated());
+ while (!m_Terminated);
@@ -291,7 +326,7 @@ void *MCHybridSOG::doCompute()
/**************** construction local ******/
// cout<<"debut boucle pile process "<<task_id<< " thread "<< id_thread<<endl;
-
+ reached_class->setProcess(destination);
if(destination==task_id)
{
// cout << " construction local de l'aggregat " <<endl;
@@ -300,6 +335,7 @@ void *MCHybridSOG::doCompute()
if(!pos)
{
m_graph->insert(reached_class);
+
pthread_mutex_unlock(&m_graph_mutex);
m_graph->addArc();
@@ -340,7 +376,7 @@ void *MCHybridSOG::doCompute()
MDD reached=ldd_reachedclass;
m_graph->insertSHA(reached_class);
- strcpySHA(reached_class->m_SHA2,Identif);
+ memcpy(reached_class->m_SHA2,Identif,16);
pthread_mutex_unlock(&m_graph_mutex);
#ifndef REDUCE
reached=Canonize(ldd_reachedclass,0);
@@ -380,6 +416,8 @@ void *MCHybridSOG::doCompute()
}
+ e.first.first->setCompletedSucc();
+
@@ -411,6 +449,12 @@ void *MCHybridSOG::doCompute()
if (!m_graph->find(Agregate))
{
m_graph->insert(Agregate);
+ Agregate->setProcess(task_id);
+ string* chaine=new string();
+ convert_wholemdd_stringcpp(MState,*chaine);
+ get_md5(*chaine,Identif);
+ delete chaine;
+ memcpy(Agregate->m_SHA2,Identif,16);
pthread_mutex_unlock(&m_graph_mutex);
Set fire=firable_obs(MState);
min_charge=minCharge();
@@ -446,62 +490,99 @@ void *MCHybridSOG::doCompute()
} /// End else
//cout<<"Working process "<<task_id<<" leaved...thread "<<id_thread<<endl;
+
}
}
-bool MCHybridSOG::isNotTerminated()
-{
- bool res=true;
- int i=0;
- while (i<m_nb_thread && res)
- {
- res=m_st[i].empty() && m_msg[i].empty();
- i++;
- }
- return !res;
-}
-
void MCHybridSOG::read_message()
{
int flag=0;
-
-
MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status); // exist a msg to receiv?
while (flag!=0)
{
+ //cout<<"message tag :"<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
+ if (m_status.MPI_TAG==TAG_ASK_STATE) {
+ cout<<"TAG ASKSTATE received by task "<<task_id<<" from "<<m_status.MPI_SOURCE<<endl;
+ char mess[17];
+ MPI_Recv(mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status);
+ bool res;m_waitingAgregate=false;
+ size_t pos=m_graph->findSHAPos(mess,res);
+ if (!res) {
+ cout<<"Not found"<<endl;
+ m_waitingAgregate=true;
+ memcpy(m_id_md5,mess,16);
+ }
+ else {
+ cout<<"pos found :"<<pos<<endl;
+ memcpy(mess,&pos,8);
+ MPI_Send(mess,8,MPI_BYTE,m_status.MPI_SOURCE, TAG_ACK_STATE, MPI_COMM_WORLD);
+ }
+
+ }
+ else if (m_status.MPI_TAG==TAG_ASK_SUCC) {
+
+ char mess[17];
+
+ MPI_Recv(mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status);
+ m_waitingBuild=false;m_waitingSucc=false;
+ bool res;
+ cout<<"Before "<<res<<endl;
+ size_t pos=m_graph->findSHAPos(mess,res);
+ cout<<"After "<<res<<endl;
+ if (res) {
+ LDDState *aggregate=m_graph->getLDDStateById(pos);
+ m_aggWaiting=aggregate;
+ if (aggregate->isCompletedSucc()) sendSuccToMC();
+ else {
+ m_waitingSucc=true;
+ cout<<"Waiting for succ..."<<endl;
+ }
+ }
+ else {
+ m_waitingBuild=true;
+ cout<<"Waiting for build..."<<endl;
+ memcpy(m_id_md5,mess,16);
+ }
+
+ }
+ int v;
switch (m_status.MPI_TAG)
{
- case TAG_STATE :
- //cout<<"TAG STATE received by task "<<task_id<<endl;
+ case TAG_STATE:
+ cout<<"=============================TAG STATE received by task "<<task_id<<endl;
read_state_message();
break;
- case TAG_FINISH : break;
- case TAG_INITIAL :
- int v;
+ case TAG_FINISH:
+ cout<<"TAG FINISH received by task "<<task_id<<endl;
+
+ MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
+ m_Terminated=true;
+ break;
+ case TAG_INITIAL:
+ cout<<"TAG INITIAL received by task "<<task_id<<endl;
+
MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
LDDState *i_agregate=m_graph->getInitialState();
- stringstream ss;
- ss<<(task_id);ss<<'\0';
- ss<<i_agregate->getSHAValue();
- cout<<"Ldd Value :"<<i_agregate->getLDDValue()<<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);
+
+ char message[23];
+ memcpy(message,i_agregate->getSHAValue(),16);
+ uint16_t id_p=i_agregate->getProcess();
+ uint32_t jouk=65535;
+ memcpy(message+16,&id_p,2);
+ memcpy(message+18,&jouk,4);
+
+ MPI_Send(message,22,MPI_BYTE,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->findSHA()
- // Send successors
- break;
- case TAG_AGREGATE : break;
- default : //cout<<"unknown received "<<status.MPI_TAG<<" by task "<<task_id<<endl;
+
+
+
+ default: cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
//AbortTerm();
break;
/* int v;
@@ -509,7 +590,8 @@ void MCHybridSOG::read_message()
if (task_id!=0)
MPI_Send( &v, 1, MPI_INT, 0, TAG_ABORT, MPI_COMM_WORLD);*/
}
- MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,m_comm_world,&flag,&m_status);
+
+ MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status);
}
}
@@ -523,7 +605,7 @@ void MCHybridSOG::read_state_message()
int nbytes;
MPI_Get_count(&m_status, MPI_CHAR, &nbytes);
char inmsg[nbytes+1];
- MPI_Recv(inmsg, nbytes, MPI_CHAR,m_status.MPI_SOURCE,TAG_STATE,m_comm_world, &m_status);
+ MPI_Recv(inmsg, nbytes, MPI_CHAR,m_status.MPI_SOURCE,TAG_STATE,MPI_COMM_WORLD, &m_status);
m_nbrecv++;
string *msg_receiv =new string(inmsg,nbytes);
min_charge=minCharge();
@@ -548,7 +630,7 @@ void MCHybridSOG::send_state_message()
message_size=s.first->size()+1;
int destination=s.second;
read_message();
- MPI_Send(s.first->c_str(), message_size, MPI_CHAR, destination, TAG_STATE, m_comm_world);
+ MPI_Send(s.first->c_str(), message_size, MPI_CHAR, destination, TAG_STATE, MPI_COMM_WORLD);
m_nbsend++;
m_size_mess+=message_size;
delete s.first;
@@ -740,10 +822,6 @@ MDD MCHybridSOG::decodage_message(const char *chaine)
} */
-
-
-
-
void * MCHybridSOG::threadHandler(void *context)
{
@@ -801,3 +879,29 @@ void MCHybridSOG::get_md5(const string& chaine,unsigned char *md_chaine)
pthread_spin_unlock(&m_spin_md5);
md_chaine[16]='\0';
}
+
+void MCHybridSOG::sendSuccToMC() {
+ uint32_t nb_succ=m_aggWaiting->getSuccessors()->size();
+ uint32_t message_size=nb_succ*20+4;
+
+ char mess_tosend[message_size];
+ memcpy(mess_tosend,&nb_succ,4);
+ uint32_t i_message=4;
+
+ for (uint32_t i=0;i<nb_succ;i++) {
+
+ pair<LDDState*,int> elt;
+ elt=m_aggWaiting->getSuccessors()->at(i);
+ memcpy(mess_tosend+i_message,elt.first->getSHAValue(),16);
+ i_message+=16;
+ uint16_t pcontainer=elt.first->getProcess();
+ cout<<" pcontainer "<<pcontainer<<endl;
+ memcpy(mess_tosend+i_message,&pcontainer,2);
+ i_message+=2;
+ memcpy(mess_tosend+i_message,&(elt.second),2);
+ i_message+=2;
+ }
+
+ MPI_Send(mess_tosend,message_size,MPI_BYTE,n_tasks, TAG_ACK_SUCC,MPI_COMM_WORLD);
+
+}
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index 6418e3a6d269d5d325d118604a9caaf9fd414097..9c250deae146d7543a4fc2fd5b2d95c916695ee8 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -58,12 +58,19 @@ public:
protected:
private:
MPI_Comm m_comm_world;
+ void sendSuccToMC();
+ bool m_waitingAgregate=false;
+ bool m_waitingBuild=false;
+ char m_id_md5[16];
+ LDDState * m_aggWaiting=nullptr;
+ bool m_waitingSucc=false;
+
/// \ hash function
void get_md5(const string &chaine, unsigned char *md_chaine);
/// minimum charge function for the load balancing between thread
inline int minCharge();
- inline bool isNotTerminated();
+
/// Copie string of caracter
void strcpySHA(unsigned char *dest, const unsigned char *source);
@@ -126,7 +133,7 @@ private:
int m_total_nb_send = 0, m_total_nb_recv = 0;
MPI_Status m_status;
- bool m_Terminating = false;
+
};
diff --git a/src/NewNet.h b/src/NewNet.h
index 10107a044d95ba59d98744209c254420af8b0a50..9709a016016507dec081c17a3d9ee6ac867e63fc 100644
--- a/src/NewNet.h
+++ b/src/NewNet.h
@@ -106,8 +106,11 @@ class NewNet : public RdPMonteur {
int nbTransition() const { return transitions.size(); };
set<string>& getListTransitionAP() {return m_ltransitionAP;}
set<string>& getListPlaceAP() {return m_lplaceAP;}
+ string& getPlaceName(size_t pos) { return m_placePosName.find(pos)->second;}
+ string& getTransitionName(size_t pos) { return m_transitionPosName.find(pos)->second;}
map<int,string> m_placePosName;
private:
+
map<int,string> m_transitionPosName;
diff --git a/src/main.cpp b/src/main.cpp
index 369c6d849d044d5b924bc8bb44dd8bc971bfadaf..d358602a16673541c7422350e903f85377b52b99 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -327,15 +327,19 @@ int main(int argc, char** argv)
else {
cout<<"On the fly Model checker by process "<<task_id<<endl;
auto d = spot::make_bdd_dict();
- spot::twa_graph_ptr k =spot::make_twa_graph(std::make_shared<HybridKripke>(d,R.getListTransitionAP(),R.getListPlaceAP()),spot::twa::prop_set::all(), true);
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ spot::twa_graph_ptr k =spot::make_twa_graph(std::make_shared<HybridKripke>(d,R.getListTransitionAP(),R.getListPlaceAP(),R),spot::twa::prop_set::all(), true);
+ cout<<"finished...."<<endl;
+ //while(1);
/* auto k =
std::make_shared<HybridKripke>(d,R.getListTransitionAP(),R.getListPlaceAP());*/
- /* fstream file;
+ fstream file;
string st(argv[3]);
st+=".dot";
file.open(st.c_str(),fstream::out);
spot::print_dot(file, k,"ka");
- file.close();*/
+ file.close();
+
}
}