modifié : src/ModelCheckBaseMT.cpp

	modifié :         src/ModelCheckBaseMT.h
	modifié :         src/ModelCheckerTh.cpp
	modifié :         src/main.cpp

src/ModelCheckBaseMT.cpp

@@ -20,6 +20,12 @@ void ModelCheckBaseMT::loadNet()
     m_graph->setPlace(m_placeName);
 }
 
+ModelCheckBaseMT::~ModelCheckBaseMT()
+{
+    cout<<__func__<<endl;
+}
+
+
   
 
 

src/ModelCheckBaseMT.h

@@ -7,6 +7,7 @@ public:
         virtual LDDState * buildInitialMetaState()=0;
         virtual void buildSucc(LDDState *agregate)=0;
         void loadNet();
+        virtual ~ModelCheckBaseMT();
 protected:
     int m_nb_thread;
 private:

src/ModelCheckerTh.cpp

@@ -185,6 +185,7 @@ void * ModelCheckerTh::Compute_successors()
         pthread_barrier_wait(&m_barrier_builder);
     }
     while (!m_finish);
+    cout<<"exit thread i"<<id_thread<<endl;
 }
 
 
@@ -228,10 +229,15 @@ void ModelCheckerTh::ComputeTh_Succ()
 }
 ModelCheckerTh::~ModelCheckerTh() {
     m_finish=true;
+    cout<<"Destructor"<<endl;
     pthread_barrier_wait(&m_barrier_threads);
+    cout<<"Before builder..."<<endl;
     pthread_barrier_wait(&m_barrier_builder);
+    cout<<"After barrier..."<<endl;
     for (int i = 0; i < m_nb_thread; i++)
      {
+         cout<<"thread "<<i<<endl;
          pthread_join(m_list_thread[i], NULL);
      }
+     cout<<"Exit Destructor"<<endl;
 }

src/main.cpp

@@ -127,12 +127,14 @@ int main(int argc, char** argv)
     MPI_Comm_rank(MPI_COMM_WORLD,&task_id);
 
     //
-    if (n_tasks==1 && !strcmp(argv[1],"otfL"))
+    if (n_tasks==1 && (!strcmp(argv[1],"otfL") || !strcmp(argv[1],"otfP")))
     {
-        cout<<"Multi-threaded on the fly Model checking (Lace)..."<<endl;
+        cout<<"Performing on the fly Model checking..."<<endl;
+        if (!strcmp(argv[1],"otfP")) cout<<"Multi-threaded algorithm based on Pthread library!"<<endl;
+        else cout<<"Multi-threaded algorithm based on Lace framework!"<<endl;
         cout<<"Building automata for not(formula)\n";
         auto d = spot::make_bdd_dict();
-        // d->register_ap("jbhkj");
+        
         spot::twa_graph_ptr af = spot::translator(d).run(not_f);
         cout<<"Formula automata built.\n";
         cout<<"Want to save the graph in a dot file ?";
@@ -147,8 +149,11 @@ int main(int argc, char** argv)
             spot::print_dot(file, af);
             file.close();
         }
-        // Initialize SOG builder
-        ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
+        cout<<"Loading net information..."<<endl;
+        ModelCheckBaseMT* mcl;
+        if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(R,bound,nb_th);
+        else 
+            mcl=new ModelCheckerTh(R,bound,nb_th);
         mcl->loadNet();        
         auto k =
             std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
@@ -170,62 +175,7 @@ int main(int argc, char** argv)
         if (auto run = k->intersecting_run(af))
         {
             std::cout << "formula is violated by the following run:\n"<<*run<<endl;
-            /*run->highlight(5); // 5 is a color number.
-            fstream file;
-            file.open("violated.dot",fstream::out);
-            cout<<"Property is violated!"<<endl;
-            cout<<"Check the dot file."<<endl;
-            spot::print_dot(file, k, ".kA");
-            file.close();*/
-        }
-        else
-            std::cout << "formula is verified\n";
-
-    }
-    else if (n_tasks==1 && !strcmp(argv[1],"otfP"))
-    {
-        cout<<"Multi-threaded on the fly Model checking (Pthread)..."<<endl;
-        cout<<"Building automata for not(formula)\n";
-        auto d = spot::make_bdd_dict();
-        
-        spot::twa_graph_ptr af = spot::translator(d).run(not_f);
-        cout<<"Formula automata built.\n";
-        cout<<"Want to save the graph in a dot file ?";
-        char c;
-        cin>>c;
-        if (c=='y')
-        {
-            fstream file;
-            string st(formula);
-            st+=".dot";
-            file.open(st.c_str(),fstream::out);
-            spot::print_dot(file, af);
-            file.close();
-        }
-        // Initialize SOG builder
-        ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th);
-        mcl->loadNet();
-        auto k =
-            std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());                                             ;
-
-        // Performing on the fly Modelchecking
-        cout<<"Want to save the graph in a dot file ?";
-                cin>>c;
-                if (c=='y')
-                {
-                    fstream file;
-
-                    string st(argv[3]);
-                    st+=".dot";
-                    file.open(st.c_str(),fstream::out);
-                    spot::print_dot(file, k,"ka");
-                    file.close();
-                }
-        cout<<"Performing on the fly Modelchecking"<<endl;
-
-        if (auto run = k->intersecting_run(af))
-        {
-            std::cout << "formula is violated by the following run:\n"<<*run<<endl;
+            cout<<"=================================="<<endl;
             /*run->highlight(5); // 5 is a color number.
             fstream file;
             file.open("violated.dot",fstream::out);
@@ -237,9 +187,7 @@ int main(int argc, char** argv)
         else
             std::cout << "formula is verified\n";
         delete mcl;
-
     }
-
     else if (n_tasks==1)
     {
         cout<<"number of task = 1 \n " <<endl;