diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index 62ff0155b9bd882d730611ba019169d543bb1cdb..0836a284b8e43ce03ce0566b15da1b8bbd1d7c1d 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -10,10 +10,9 @@
#include "HybridKripke.h"
#include <map>
using namespace spot;
-HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder): spot::kripke(dict_ptr),m_builder(builder)
+HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr): spot::kripke(dict_ptr)
{
- HybridKripkeIterator::m_builder=builder;
- HybridKripkeIterator::m_builder=builder;
+
HybridKripkeIterator::m_dict_ptr=&dict_ptr;
HybridKripkeIterator::m_deadlock.setLDDValue(1);
HybridKripkeIterator::m_deadlock.setVisited();
@@ -24,7 +23,7 @@ HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builde
HybridKripkeIterator::m_div.Successors.push_back(pair<LDDState*,int>(&HybridKripkeIterator::m_div,-1));
}
-HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):HybridKripke(dict_ptr,builder) {
+HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap):HybridKripke(dict_ptr) {
for (auto it=l_transap.begin();it!=l_transap.end();it++) {
register_ap(*it);
@@ -36,8 +35,11 @@ HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *
state* HybridKripke::get_init_state() const {
- LDDState *ss=m_builder->getInitialMetaState();
- return new HybridKripkeState(ss);//new SpotSogState();
+ // LDDState *ss=m_builder->getInitialMetaState();
+
+ string id;
+ uint16_t p_container;
+ return new HybridKripkeState(id,p_container);//new SpotSogState();
}
// Allows to print state label representing its id
@@ -78,22 +80,22 @@ 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());
+ //vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
bdd result=bddtrue;
// Marked places
- for (auto it=marked_place.begin();it!=marked_place.end();it++) {
- string name=m_builder->getPlace(*it);
+ //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=unmarked_place.begin();it!=unmarked_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=unmarked_place.begin();it!=unmarked_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);
- }
+ result&=!bdd_ithvar((dict_->var_map.find(f))->second);*/
+ //}
return result;
}
diff --git a/src/HybridKripke.h b/src/HybridKripke.h
index b9f718120d032c82d5caac5a78d0a3848657c6b3..273fe216e80d70e3dd70ce4e61b489990e65e31c 100644
--- a/src/HybridKripke.h
+++ b/src/HybridKripke.h
@@ -10,15 +10,15 @@
class HybridKripke: public spot::kripke {
public:
- 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);
+ HybridKripke(const spot::bdd_dict_ptr& dict_ptr);
+ HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_transap,set<string> &l_placeap);
virtual ~HybridKripke();
spot::state* get_init_state() 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;
- ModelCheckBaseMT *m_builder;
+ //ModelCheckBaseMT *m_builder;
protected:
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index 69a4079f5c2783cc64b979145c2c4423d2c5e5b3..7a49bf3509096a3974b3e89b62705d81e3c241f2 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -42,7 +42,11 @@ bool HybridKripkeIterator::done() 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 HybridKripkeState(m_lsucc.at(m_current_edge).first);
+ // return new HybridKripkeState(m_lsucc.at(m_current_edge).first);
+ string id;
+ uint16_t p_container;
+ return new HybridKripkeState(id,p_container);
+ // return new HybridKripkeState(m_lsucc.at(m_current_edge).first);
}
bdd HybridKripkeIterator::cond() const {
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index 212f0561349662cc8722c93e05c0d6a6387d50af..dbf999d169be47cbeb2b7d8a4f3edc7717397cee 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -1,22 +1,27 @@
#ifndef HYBRIDKRIPKESTATETH_H_INCLUDED
#define HYBRIDKRIPKESTATETH_H_INCLUDED
-
+#include <mpi.h>
#include "LDDState.h"
#include "ModelCheckBaseMT.h"
-
+#define TAG_ASKSTATE 10
class HybridKripkeState : public spot::state
{
public:
static ModelCheckBaseMT * m_builder;
- HybridKripkeState(LDDState *st):m_state(st) {
- m_builder->buildSucc(st);
+ HybridKripkeState(string &id,uint16_t pcontainer):m_id(id),m_container(pcontainer) {
+ int v=1;
+ MPI_Send( &v, 1, MPI_INT, 0, TAG_ASKSTATE, MPI_COMM_WORLD);
+
};
+ // 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) {
+ }
virtual ~HybridKripkeState();
HybridKripkeState* clone() const override
{
- return new HybridKripkeState(m_state);
+ return new HybridKripkeState(m_id,m_container,m_div,m_deadlock);
}
size_t hash() const override
{
@@ -41,6 +46,10 @@ protected:
private:
LDDState *m_state;
+ string m_id;
+ bool m_div;
+ bool m_deadlock;
+ uint16_t m_container;
};
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 9c86805b9de6341b0ffa6c8ce1fdff45217f1852..ddb171488f81a5380b74842b0768745f6e6b24b6 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -14,10 +14,10 @@ using namespace sylvan;
#define LENGTH_ID 16
//#define LENGTH_MSG 180
#define TAG_STATE 1
-#define TAG_SEND 2
-#define TAG_REC 4
-#define TAG_TERM 8
-#define TAG_ABORT 16
+#define TAG_FINISH 2
+#define TAG_INITIAL 3
+#define TAG_SUCC 4
+#define TAG_AGREGATE 5
@@ -90,8 +90,7 @@ MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world, int BOUND,bool in
{
adjacentPlace.insert(it->first);
prec[it->first] = prec[it->first] + it->second;
- //printf("It first %d \n",it->first);
- //printf("In prec %d \n",prec[it->first]);
+
}
// arcs post
for(vector< pair<int,int> >::const_iterator it=t->post.begin(); it!=t->post.end(); it++)
@@ -145,9 +144,6 @@ void *MCHybridSOG::doCompute()
// MDD reduced_initialstate=Canonize(Complete_meta_state,0);
convert_wholemdd_stringcpp(Complete_meta_state,*chaine);
- //DisplayMessage(chaine->c_str());
- //write_to_dot("normal.dot",Complete_meta_state);
- //exit(0);
get_md5(*chaine,Identif);
//lddmc_getsha(Complete_meta_state, Identif);
int destination=(int)(Identif[0]%n_tasks);
@@ -455,42 +451,6 @@ void *MCHybridSOG::doCompute()
}
-void MCHybridSOG::ReceiveTermSignal()
-{
-
- int term=1;
- MPI_Recv(&term, 1, MPI_INT, task_id==0 ? n_tasks-1 : task_id-1, TAG_TERM, m_comm_world,&m_status);
- //cout<<"Task id receive terminal message"<<task_id<<endl;
- if(task_id!=0)
- {
- MPI_Send(&term, 1, MPI_INT, (task_id + 1)%n_tasks, TAG_TERM, m_comm_world);
- }
- m_Terminated=true;
-}
-
-
-void MCHybridSOG::TermReceivedMsg()
-{
-
-
- int kkk=0;
- MPI_Recv(&kkk, 1, MPI_INT, task_id==0 ? n_tasks-1 : task_id-1, TAG_REC, m_comm_world, &m_status);
- if(task_id!=0)
- {
- kkk=kkk+m_nbrecv;
- MPI_Send( &kkk, 1, MPI_INT, (task_id+1)%n_tasks, TAG_REC, m_comm_world);
-
- }
- else if (m_Terminating)
- {
- m_total_nb_recv=kkk;
- // printf("Process 0 total receive %d\n", m_total_nb_recv);
- MPI_Send( &m_nbsend, 1, MPI_INT, 1, TAG_SEND, m_comm_world);
- // printf("Process 0 nb send au debut %d\n", m_nbsend);
- }
-
-}
-
bool MCHybridSOG::isNotTerminated()
{
@@ -505,20 +465,13 @@ bool MCHybridSOG::isNotTerminated()
}
-void MCHybridSOG::AbortTerm()
-{
- int v=1;
- m_Terminating=false;
- MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, m_comm_world, &m_status);
- if (task_id) MPI_Send( &v, 1, MPI_INT, 0, TAG_ABORT, m_comm_world);
-}
void MCHybridSOG::read_message()
{
int flag=0;
- MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,m_comm_world,&flag,&m_status); // exist a msg to receiv?
+ MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status); // exist a msg to receiv?
while (flag!=0)
{
switch (m_status.MPI_TAG)
@@ -527,12 +480,12 @@ void MCHybridSOG::read_message()
//cout<<"TAG STATE received by task "<<task_id<<endl;
read_state_message();
break;
- case TAG_REC :
- //cout<<"TAG_REC received by task "<<task_id<<endl;
- AbortTerm();
- break;
+ case TAG_FINISH : break;
+ case TAG_INITIAL : break;
+ case TAG_SUCC : break;
+ case TAG_AGREGATE : break;
default : //cout<<"unknown received "<<status.MPI_TAG<<" by task "<<task_id<<endl;
- AbortTerm();
+ //AbortTerm();
break;
/* int v;
MPI_Recv(&v, 1, MPI_INT, status.MPI_SOURCE, status.MPI_TAG, MPI_COMM_WORLD, &status);
@@ -556,11 +509,6 @@ void MCHybridSOG::read_state_message()
MPI_Recv(inmsg, nbytes, MPI_CHAR,m_status.MPI_SOURCE,TAG_STATE,m_comm_world, &m_status);
m_nbrecv++;
string *msg_receiv =new string(inmsg,nbytes);
- /*string nom_file="recept_";
- nom_file+=to_string(task_id);
- FILE *fp=fopen(nom_file.c_str(),"a");
- fprintf(fp,"%s\n",msg_receiv->c_str());
- fclose(fp);*/
min_charge=minCharge();
m_charge[min_charge]++;
pthread_mutex_lock(&m_spin_msg[min_charge]);
@@ -583,12 +531,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);
- /*string nom_file="send_";
- nom_file+=to_string(task_id);
- FILE *fp=fopen(nom_file.c_str(),"a");
- fprintf(fp,"%s\n",s.first->c_str());
- fclose(fp);*/
+ MPI_Send(s.first->c_str(), message_size, MPI_CHAR, destination, TAG_STATE, m_comm_world);
m_nbsend++;
m_size_mess+=message_size;
delete s.first;
@@ -599,8 +542,6 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
{
m_graph=&g;
-// MPI_Comm_size(MPI_COMM_WORLD,&n_tasks);
-// MPI_Comm_rank(MPI_COMM_WORLD,&task_id);
double tps;
// double t1=(double)clock() / (double)CLOCKS_PER_SEC;
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index ade83246484f4b594484f89a6a558498eea29fc6..6418e3a6d269d5d325d118604a9caaf9fd414097 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -60,14 +60,7 @@ private:
MPI_Comm m_comm_world;
/// \ hash function
void get_md5(const string &chaine, unsigned char *md_chaine);
- /// Termination Detection functions
- inline void ReceiveTermSignal();
-
-
- inline void TermReceivedMsg();
-
-
-
+
/// minimum charge function for the load balancing between thread
inline int minCharge();
inline bool isNotTerminated();
@@ -100,7 +93,7 @@ private:
void read_message();
- void AbortTerm();
+
/// receive state message
void read_state_message();
/// send state message
diff --git a/src/main.cpp b/src/main.cpp
index 9e7f9c9fd79f3aa17cae16a70ee5ede916bb2d45..849673fce29d3e2d075f9f45b9c01207729cfcc6 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -28,6 +28,7 @@
#include "SogKripke.h"
#include "SogKripkeTh.h"
+#include "HybridKripke.h"
@@ -322,12 +323,13 @@ int main(int argc, char** argv)
cout<<"N task :"<<n_tasks<<endl;
MCHybridSOG DR(R,gprocess, bound,false);
LDDGraph g(&DR);
- DR.computeDSOG(g);
-
+ DR.computeDSOG(g);
}
- else {
-
+ else {
cout<<"On the fly Model checker by process "<<task_id<<endl;
+ auto d = spot::make_bdd_dict();
+ auto k =
+ std::make_shared<HybridKripke>(d,R.getListTransitionAP(),R.getListPlaceAP());
}
}