From 3232b6bcea240d7b8a335a0bfbff28223f8be94f Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sat, 11 Apr 2020 23:32:50 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/ModelCheckerThV2.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/ModelCheckerThV2.h?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/ModelCheckerThV2.cpp | 22 ++++++++++++++--------
src/ModelCheckerThV2.h | 6 ++++--
2 files changed, 18 insertions(+), 10 deletions(-)
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
index f1f9c3d..776affd 100644
--- a/src/ModelCheckerThV2.cpp
+++ b/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();
+}
diff --git a/src/ModelCheckerThV2.h b/src/ModelCheckerThV2.h
index 987b7de..84ec05c 100644
--- a/src/ModelCheckerThV2.h
+++ b/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
--
GitLab