diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 388ee7c906ea7f98fe2da7d036454ffd93a9ae05..4231a5f4049a99848bcad77aa9f95f6f12914afe 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -85,8 +85,6 @@ target_link_libraries(hybrid-sog
spot
sylvan
RdP
-
-
${MPI_LIBRARIES}
${OPENSSL_LIBRARIES}
)
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index e8d4f6d8ca0614e53e9518d3dec6bcc41aa9ef7c..9c86805b9de6341b0ffa6c8ce1fdff45217f1852 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -22,10 +22,10 @@ using namespace sylvan;
-MCHybridSOG::MCHybridSOG(const NewNet &R, int BOUND,bool init)
+MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world, int BOUND,bool init)
{
-
+ m_comm_world=comm_world;
lace_init(1, 0);
lace_startup(0, NULL, NULL);
@@ -204,38 +204,10 @@ void *MCHybridSOG::doCompute()
send_state_message();
read_message();
}
- while (isNotTerminated()); //!m_msg[0].empty());
-
+ while (isNotTerminated());
- if (m_working==0 && m_nbsend>=1)
- {
-
- if(task_id==0)// && !isNotTerminated())
- {
- /*cout<<"Termination started..."<<endl;
- cout<<"Nb send "<<m_nbsend<<" nb recev "<<m_nbrecv<<endl;*/
- startTermDetectionByMaster();
- do
- {
- read_termination();
- }
- while (m_Terminating==true && m_Terminated==false );// && m_tag_state_received==false);
- //cout<<"task id"<<task_id<<"termination is started"<<endl;
- }
- else //if (task_id && !isNotTerminated())
- {
- m_Terminating=true;
- do
- {
- read_termination();
- }
- while (m_Terminating==true && m_Terminated==false); // && !isNotTerminated());// && m_tag_state_received==false);
- m_Terminating=false;
- }
- //pthread_barrier_wait(&m_barrier2);
-
- } //m_working
+
}
/******************************* Construction des aggregats ************************************/
@@ -268,7 +240,7 @@ void *MCHybridSOG::doCompute()
m_charge[id_thread]--;
LDDState *reached_class=NULL;
- // cout << " cccccccccc "<<endl;
+
while(!e.second.empty())
{
@@ -375,7 +347,6 @@ void *MCHybridSOG::doCompute()
strcpySHA(reached_class->m_SHA2,Identif);
pthread_mutex_unlock(&m_graph_mutex);
#ifndef REDUCE
- printf("Hello canonize");
reached=Canonize(ldd_reachedclass,0);
ldd_refs_push(ldd_reachedclass);
#endif
@@ -488,64 +459,33 @@ void MCHybridSOG::ReceiveTermSignal()
{
int term=1;
- MPI_Recv(&term, 1, MPI_INT, task_id==0 ? n_tasks-1 : task_id-1, TAG_TERM, MPI_COMM_WORLD,&m_status);
+ 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, MPI_COMM_WORLD);
+ MPI_Send(&term, 1, MPI_INT, (task_id + 1)%n_tasks, TAG_TERM, m_comm_world);
}
m_Terminated=true;
}
-void MCHybridSOG::TermSendMsg()
-{
-
-
- int term=1;
- int kkk;
- MPI_Recv( &kkk, 1, MPI_INT,task_id==0 ? n_tasks-1 : task_id-1, TAG_SEND, MPI_COMM_WORLD, &m_status);
- // cout<<" Terminaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaate \n"<<task_id<<endl;
-
- if(task_id!=0)
- {
- kkk=kkk+m_nbsend;
- MPI_Send( &kkk, 1, MPI_INT, (task_id + 1) % n_tasks, TAG_SEND, MPI_COMM_WORLD);
-
- }
- else if(kkk==m_total_nb_recv)
- {
- MPI_Send( &term, 1, MPI_INT, (task_id + 1) % n_tasks, TAG_TERM, MPI_COMM_WORLD);
- }
- else
- {
- m_Terminating=false;
- }
-
-}
-
-void MCHybridSOG::startTermDetectionByMaster()
-{
- m_Terminating=true;
- MPI_Send( &m_nbrecv, 1, MPI_INT, (task_id+1)%n_tasks, TAG_REC, MPI_COMM_WORLD);
-}
void MCHybridSOG::TermReceivedMsg()
{
int kkk=0;
- MPI_Recv(&kkk, 1, MPI_INT, task_id==0 ? n_tasks-1 : task_id-1, TAG_REC, MPI_COMM_WORLD, &m_status);
+ 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, MPI_COMM_WORLD);
+ 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, MPI_COMM_WORLD);
+ MPI_Send( &m_nbsend, 1, MPI_INT, 1, TAG_SEND, m_comm_world);
// printf("Process 0 nb send au debut %d\n", m_nbsend);
}
@@ -569,8 +509,8 @@ void MCHybridSOG::AbortTerm()
{
int v=1;
m_Terminating=false;
- MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
- if (task_id) MPI_Send( &v, 1, MPI_INT, 0, TAG_ABORT, MPI_COMM_WORLD);
+ 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()
@@ -578,7 +518,7 @@ 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?
+ MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,m_comm_world,&flag,&m_status); // exist a msg to receiv?
while (flag!=0)
{
switch (m_status.MPI_TAG)
@@ -599,54 +539,12 @@ 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,MPI_COMM_WORLD,&flag,&m_status);
+ MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,m_comm_world,&flag,&m_status);
}
}
-void MCHybridSOG::read_termination()
-{
- 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)
- {
- switch (m_status.MPI_TAG)
- {
- case TAG_ABORT :
- int v;
- MPI_Recv(&v, 1, MPI_INT, MPI_ANY_SOURCE, TAG_ABORT, MPI_COMM_WORLD, &m_status);
- //cout<<"TAG ABORTED received by task"<<task_id<<endl;
- m_Terminating=false;
- return;
- break;
- case TAG_REC :
- //cout<<"TAG REC by task"<<task_id<<endl;
- TermReceivedMsg();
- break;
- case TAG_SEND :
- //cout<<"TAG SEND received by task"<<task_id<<endl;
- TermSendMsg();
- break;
- case TAG_TERM :
- //cout<<"TAG TERM received by task................................."<<task_id<<endl;
- ReceiveTermSignal();
- break;
- case TAG_STATE :
- //cout<<"TAG STATe received by task"<<task_id<<endl;
- m_Terminating=false;
- return;
- break;
- default :
- cout<<"read_termination unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
- break;
-
- }
-
- MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status);
- }
-}
void MCHybridSOG::read_state_message()
{
@@ -655,7 +553,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,MPI_COMM_WORLD, &m_status);
+ 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_";
@@ -685,7 +583,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, MPI_COMM_WORLD);
+ 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");
@@ -706,8 +604,9 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
double tps;
// double t1=(double)clock() / (double)CLOCKS_PER_SEC;
-
- MPI_Barrier(MPI_COMM_WORLD);
+ cout<<"process with id "<<task_id<<" / "<<n_tasks<<endl;
+ MPI_Barrier(m_comm_world);
+ cout<<"After!!!!process with id "<<task_id<<endl;
// int nb_th;
m_nb_thread=nb_th;
cout<<"nb de thread"<<nb_th<<endl;
@@ -770,9 +669,9 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
int nbarcs=g.m_nbArcs;
unsigned long total_size_mess=0;
- MPI_Reduce(&nbstate, &sum_nbStates, 1, MPI_INT, MPI_SUM, 0, MPI_COMM_WORLD);
- MPI_Reduce(&nbarcs, &sum_nbArcs, 1, MPI_INT, MPI_SUM, 0, MPI_COMM_WORLD);
- MPI_Reduce(&m_size_mess, &total_size_mess, 1, MPI_INT, MPI_SUM, 0, MPI_COMM_WORLD);
+ MPI_Reduce(&nbstate, &sum_nbStates, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
+ MPI_Reduce(&nbarcs, &sum_nbArcs, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
+ MPI_Reduce(&m_size_mess, &total_size_mess, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index 72a91176eb5c914131022e78134f14093084e37b..ade83246484f4b594484f89a6a558498eea29fc6 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -47,7 +47,7 @@ typedef stack<MSG> pile_msg;
class MCHybridSOG : public CommonSOG
{
public:
- MCHybridSOG(const NewNet &, int BOUND = 32, bool init = false);
+ MCHybridSOG(const NewNet &,MPI_Comm &, int BOUND = 32, bool init = false);
void buildFromNet(int index);
/// principal functions to construct the SOG
void computeDSOG(LDDGraph &g);
@@ -57,12 +57,13 @@ public:
protected:
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 TermSendMsg();
- inline void startTermDetectionByMaster();
+
+
inline void TermReceivedMsg();
@@ -97,8 +98,8 @@ private:
MDD decodage_message(const char *chaine);
/// there is a message to receive?
void read_message();
- /// receive termination message
- void read_termination();
+
+
void AbortTerm();
/// receive state message
void read_state_message();
diff --git a/src/main.cpp b/src/main.cpp
index eafa3f9e44c1ef8c262dc912affe8173fae1e1fe..9e7f9c9fd79f3aa17cae16a70ee5ede916bb2d45 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -11,6 +11,7 @@
#include "DistributedSOG.h"
#include "threadSOG.h"
#include "HybridSOG.h"
+#include "MCHybridSOG.h"
#include "LDDGraph.h"
#include "ModelCheckLace.h"
#include "ModelCheckerTh.h"
@@ -263,9 +264,7 @@ int main(int argc, char** argv)
//auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
spot::twa_graph_ptr k =
- spot::make_twa_graph(std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()),
- spot::twa::prop_set::all(), true);
-
+ spot::make_twa_graph(std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()),spot::twa::prop_set::all(), true);
cout<<"SOG translated to SPOT succeeded.."<<endl;
cout<<"Want to save the graph in a dot file ?";
@@ -273,7 +272,6 @@ int main(int argc, char** argv)
if (c=='y')
{
fstream file;
-
string st(argv[3]);
st+=".dot";
file.open(st.c_str(),fstream::out);
@@ -311,12 +309,28 @@ int main(int argc, char** argv)
DR.computeDSOG(g);
}
else {
- if (task_id==0) {
+ n_tasks--;
+ if (task_id==n_tasks) {
cout<<"Model checking on the fly..."<<endl;
cout<<" One process will perform Model checking"<<endl;
- cout<<n_tasks-1<<" process will build the Distributed SOG"<<endl;
+ cout<<n_tasks<<" process will build the Distributed SOG"<<endl;
+ }
+ MPI_Comm gprocess;
+ MPI_Comm_split(MPI_COMM_WORLD,task_id==n_tasks?0:1,task_id,&gprocess);
+ cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
+ if (task_id!=n_tasks) {
+ cout<<"N task :"<<n_tasks<<endl;
+ MCHybridSOG DR(R,gprocess, bound,false);
+ LDDGraph g(&DR);
+ DR.computeDSOG(g);
+
+ }
+ else {
+
+ cout<<"On the fly Model checker by process "<<task_id<<endl;
+ }
}
- }
+
}
else