modifié : src/ModelCheckerThV2.cpp

	modifié :         src/ModelCheckerThV2.h

src/ModelCheckerThV2.cpp

@@ -135,24 +135,29 @@ void ModelCheckerThV2::Compute_successors()
         LDDState *c = new LDDState;
         MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
         ldd_refs_push ( Complete_meta_state );
-
         fire = firable_obs ( Complete_meta_state );
         c->m_lddstate = Complete_meta_state;
         c->setDeadLock ( Set_Bloc ( Complete_meta_state ) );
         c->setDiv ( Set_Div ( Complete_meta_state ) );
         m_common_stack.push ( Pair ( couple ( c, Complete_meta_state ), fire ) );
+        m_condStack.notify_one();
         m_started=true;
         m_graph->setInitialState ( c );
         m_graph->insert ( c );
         m_finish_initial = true;
-
     }
 
     LDDState *reached_class;
     //pthread_barrier_wait ( &m_barrier_builder );
+    Pair e;
     do {
-        Pair e;
-        while ( !m_common_stack.empty() && !m_finish ) {
+        
+        
+        std::unique_lock<std::mutex> lk ( m_mutexStack );
+        m_condStack.wait(lk,std::bind(&ModelCheckerThV2::hasToProcess,this));
+        lk.unlock();
+        
+        if (!m_finish ) {
             m_terminaison++;
             bool advance=true;
             try {
@@ -206,15 +211,12 @@ void ModelCheckerThV2::Compute_successors()
                         reached_class->setDeadLock ( Set_Bloc ( reduced_meta ) );
                         reached_class->setDiv ( Set_Div ( reduced_meta ) );
 
-
                         m_common_stack.push ( Pair ( couple ( reached_class, reduced_meta ), fire ) );
+                        m_condStack.notify_one();
 
                         e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( reached_class, t ) );
                         reached_class->Predecessors.insert ( reached_class->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
 
-                        //pthread_mutex_lock(&m_mutex);
-
-
                     } else {
                         m_graph->addArc();
                         m_graph_mutex.unlock();
@@ -272,6 +274,7 @@ void ModelCheckerThV2::ComputeTh_Succ()
 ModelCheckerThV2::~ModelCheckerThV2()
 {
     m_finish = true;
+    m_condStack.notify_all();
     pthread_barrier_wait ( &m_barrier_builder );
     for ( int i = 0; i < m_nb_thread; i++ ) {
         m_list_thread[i]->join();
@@ -279,4 +282,7 @@ ModelCheckerThV2::~ModelCheckerThV2()
     }
 
 }
+bool ModelCheckerThV2::hasToProcess() const {
+    return m_finish || !m_common_stack.empty();
+}
 

src/ModelCheckerThV2.h

@@ -5,6 +5,7 @@
 #include <atomic>
 #include <thread>
 #include <mutex>
+#include <condition_variable>
 typedef pair<LDDState *, int> couple_th;
 typedef stack<pair<LDDState *,int>> pile_t;
 
@@ -20,7 +21,7 @@ public:
     void ComputeTh_Succ();
 private:
     void preConfigure();
-    
+    bool ModelCheckerThV2::hasToProcess() const;
       
     StackSafe<Pair> m_common_stack;
     bool m_started=false;
@@ -31,7 +32,8 @@ private:
     atomic<uint32_t> m_gc,m_terminaison; //
     volatile bool m_finish=false;
     bool m_finish_initial=false;
-    pthread_mutex_t m_mutex_stack[128];
+    std::condition_variable m_condStack;
+    std::mutex m_mutexStack;
     thread* m_list_thread[128];    
 };
 #endif