modifié : src/CMakeLists.txt

	modifié :         src/MCHybridSOG.cpp
	modifié :         src/ModelCheckLace.cpp
	modifié :         src/main.cpp
	modifié :         src/sylvan_sog.c

src/CMakeLists.txt

@@ -9,16 +9,27 @@ include_directories(${MPI_INCLUDE_PATH})
 find_package(OpenSSL)
 include_directories(${OPENSSL_INCLUDE_DIR})
 
-# include spot library
-add_library(spot STATIC IMPORTED)
-set_target_properties(spot PROPERTIES IMPORTED_LOCATION "${SPOT_DIR}/lib/libspot.a")
+include_directories("${CMAKE_SOURCE_DIR}/third-party/sylvan/src")
+
+
+add_library(spot SHARED IMPORTED) # or STATIC instead of SHARED
+set_target_properties(spot PROPERTIES
+  IMPORTED_LOCATION "/usr/lib/x86_64-linux-gnu/libspot.so"
+  INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
+)
+
+add_library(bddx SHARED IMPORTED) # or STATIC instead of SHARED
+set_target_properties(bddx PROPERTIES
+  IMPORTED_LOCATION "/usr/lib/x86_64-linux-gnu/libbddx.so"
+  INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
+)
+
+
+
 
-# include bddx library
-add_library(bddx STATIC IMPORTED)
-set_target_properties(bddx PROPERTIES IMPORTED_LOCATION "${SPOT_DIR}/lib/libbddx.a")
 
 # Hybrid SOG executable
-add_executable(pmc-sog main.cpp
+add_executable(hybrid-sog main.cpp
   NewNet.cpp
   NewNet.h
   CommonSOG.cpp
@@ -69,7 +80,7 @@ add_executable(pmc-sog main.cpp
   HybridKripkeState.h
   )
 
-target_link_libraries(pmc-sog
+target_link_libraries(hybrid-sog
   bddx
   spot
   sylvan
@@ -77,5 +88,3 @@ target_link_libraries(pmc-sog
   ${MPI_LIBRARIES}
   ${OPENSSL_LIBRARIES}
 )
-
-add_dependencies(pmc-sog SpotLibrary)

src/MCHybridSOG.cpp

@@ -567,13 +567,10 @@ void MCHybridSOG::read_message()
              uint16_t id_p=i_agregate->getProcess();             
              memcpy(message+16,&id_p,2);            
              MPI_Send(message,22,MPI_BYTE,m_status.MPI_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD);
-             break;
-       
-        
-        
-        default:  cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
+             break;        
+        /*default:  cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
             //AbortTerm();
-            break;           
+            //break;    */       
         }
         
         MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status);

src/ModelCheckLace.cpp

@@ -33,7 +33,7 @@ void ModelCheckLace::preConfigure() {
     print_h(max);
     printf(" max.\n");
     LACE_ME;
-    sylvan_set_limits(max, 16, 2);
+    sylvan_set_limits(max, 16, 1);
     sylvan_init_package();
     sylvan_init_ldd();
     
@@ -58,7 +58,7 @@ void ModelCheckLace::preConfigure() {
         cout<<(*it2).first<<" : "<<(*it2).second<<endl;
     }*/
     //cout<<"Transitions observables :"<<endl;
-    Set::iterator it=m_observable.begin();
+    //Set::iterator it=m_observable.begin();
     /*for (; it!=m_observable.end(); it++)
     {
         cout<<*it<<"  ";
@@ -133,20 +133,16 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
 {
     MDD M1;
     MDD M2=From;
-    int it=0;
-    /*lddmc_refs_pushptr(&M1);
-    lddmc_refs_pushptr(&M2);*/
-    cout<<"worker "<<lace_get_worker()->worker<<endl;
-    
+      
     do
     {
         M1=M2;
-        for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
+        for(Set::iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
         {
             lddmc_refs_spawn(SPAWN(lddmc_firing_lace,M2,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus()));
         }
       
-        for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
+        for(Set::iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
         {
             lddmc_refs_push(M1);
             lddmc_refs_push(M2);
@@ -155,6 +151,8 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
             M2=lddmc_union(succ,M2);
             lddmc_refs_pop(3);
         }
+        cout<<"M1 :"<<M1<<endl;
+        cout<<"M2 :"<<M2<<endl;
 
     }
     while (M1!=M2);
@@ -237,7 +235,7 @@ LDDState * ModelCheckLace::getInitialMetaState()
     // Compute successors
     unsigned int onb_it=0;
     Set::iterator iter=fire.begin();
-    int j=0;
+    
     while(iter!=fire.end())
     {
         

src/main.cpp

@@ -349,19 +349,8 @@ int main(int argc, char** argv)
 
                     auto d = spot::make_bdd_dict();
                     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,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet),spot::twa::prop_set::all(), true);
-                               cout<<"finished...."<<endl;
-
-
-                               fstream file;
-                               string st(argv[3]);
-                               st+=".dot";
-                               file.open(st.c_str(),fstream::out);
-                               spot::print_dot(file, k,"ka");
-                               file.close(); */
+                
                     double tps;
-
                     auto t1 = std::chrono::high_resolution_clock::now();
                     auto k =
                         std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet);
@@ -372,9 +361,7 @@ int main(int argc, char** argv)
                         std::cout << "temps de verification "
                                   << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
                                   << " milliseconds\n";
-
                         cout<<"=================================="<<endl;
-
                     }
                     else
                     {
@@ -385,27 +372,19 @@ int main(int argc, char** argv)
                                   << " milliseconds\n";
 
                     }
-
                 }
-
             }
-
-
         }
         else
-        {
-            //cout<<" sequential version using Sylvan : 1 with BuDDy : 2 \n" <<endl;
+        {           
             cout<<"*************Distibuted version******************* \n" <<endl;
             {
                 DistributedSOG DR(Rnewnet, bound);
                 LDDGraph g(nullptr);
                 DR.computeDSOG(g);
             }
-
-
         }
     }
-
     MPI_Finalize();
     return (EXIT_SUCCESS);
 }

src/sylvan_sog.c

@@ -66,7 +66,8 @@ TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
         MDD left=lddmc_refs_sync(SYNC(lddmc_firing_lace));
         lddmc_refs_push(left);
         MDD result2 =
-                lddmc_makenode(l_values[count],left, lddmc_false);            
+                lddmc_makenode(l_values[count],left, lddmc_false);      
+        if (l_values[count]>5) printf("%d ",l_values[count]);
         lddmc_refs_push(result2);    
         result = lddmc_union( result, result2);  
         lddmc_refs_pop(3);