modifié : src/HybridKripke.cpp

	modifié :         src/HybridKripkeState.h
	modifié :         src/MCHybridSOG.cpp
	modifié :         src/main.cpp

src/HybridKripke.cpp

@@ -9,7 +9,10 @@
 
 #include "HybridKripke.h"
 #include <map>
+#define TAG_INITIAL 3
+#define TAG_ACK_INITIAL 8
 using namespace spot;
+
 HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr): spot::kripke(dict_ptr)
 {
     
@@ -24,22 +27,33 @@ HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr): spot::kripke(dict_ptr)
 }
 
 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);
     }
+    
     for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
         register_ap(*it);
+    
 
 }
 
 
 state* HybridKripke::get_init_state() const {
-    // LDDState *ss=m_builder->getInitialMetaState();   
-    
-    string id;
-    uint16_t p_container;
-    return new HybridKripkeState(id,p_container);//new SpotSogState();
+    // LDDState *ss=m_builder->getInitialMetaState();
+    int v;
+    MPI_Send( &v, 1, MPI_INT, 0, TAG_INITIAL, MPI_COMM_WORLD); 
+     char message[18];
+    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;
+    string id(message+1);
+    uint16_t p_container=message[0];
+    return new HybridKripkeState(id,p_container);
 
 }
 // Allows to print state label representing its id

src/HybridKripkeState.h

@@ -4,14 +4,14 @@
 #include <mpi.h>
 #include "LDDState.h"
 #include "ModelCheckBaseMT.h"
-#define TAG_ASKSTATE 10
+#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, 0, TAG_ASKSTATE, MPI_COMM_WORLD); 
+        int v=1;        
+        MPI_Send( &v, 1, MPI_INT, m_container, TAG_ASK_SUCC, MPI_COMM_WORLD); 
                 
     };
     // Constructor for cloning

src/MCHybridSOG.cpp

@@ -16,11 +16,10 @@ using namespace sylvan;
 #define TAG_STATE 1
 #define TAG_FINISH 2
 #define TAG_INITIAL 3
-#define TAG_SUCC 4
-#define TAG_AGREGATE 5
-
-
+#define TAG_ASK_SUCC 4
 
+#define TAG_AGREGATE 5
+#define TAG_ACK_INITIAL 8
 
 MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world, int BOUND,bool init)
 {
@@ -157,6 +156,7 @@ void *MCHybridSOG::doCompute()
             m_graph->setInitialState(c);
             m_graph->insert(c);
             m_charge[1]++;
+            strcpySHA(c->m_SHA2,Identif);
         }
         else
         {
@@ -481,8 +481,23 @@ void MCHybridSOG::read_message()
             read_state_message();
             break;
         case TAG_FINISH : break;
-        case TAG_INITIAL : break;
-        case TAG_SUCC : break;
+        case TAG_INITIAL : 
+             int v;
+             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<<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);
+             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);
+            break;
         case TAG_AGREGATE : break;
         default :  //cout<<"unknown received "<<status.MPI_TAG<<" by task "<<task_id<<endl;
             //AbortTerm();
@@ -663,6 +678,7 @@ void MCHybridSOG::strcpySHA(unsigned char *dest,const unsigned char *source)
     for (int i=0; i<LENGTH_ID; i++)
     {
         dest[i]=source[i];
+        //if (source[i]=='\0') exit(0);
     }
     dest[LENGTH_ID]='\0';
 }

src/main.cpp

@@ -103,7 +103,6 @@ int main(int argc, char** argv)
     //if(argc>5)
     nb_th = atoi(argv[2])==0 ? 1 : atoi(argv[2]);
 
-    cout<<"Bonjour..."<<endl;
     cout<<"Fichier net : "<<argv[3]<<endl;
     cout<<"Fichier formule : "<<formula<<endl;
     cout<<"Fichier Interface : "<<Int<<endl;
@@ -327,9 +326,16 @@ int main(int argc, char** argv)
                     }
                     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());
+                       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);
+                     /*   auto k =
+            std::make_shared<HybridKripke>(d,R.getListTransitionAP(),R.getListPlaceAP());*/
+                     /*    fstream file;
+                    string st(argv[3]);
+                    st+=".dot";
+                    file.open(st.c_str(),fstream::out);
+                    spot::print_dot(file, k,"ka");
+                    file.close();*/
                     }
                 }