From cf40a63af0d9089f832d06d54dd5554b99e8d243 Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Thu, 9 Apr 2020 20:33:45 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/ModelCheckerTh.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?= =?UTF-8?q?=20=20=20=20=20third-party/sylvan=20(contenu=20modifi=C3=A9)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/ModelCheckerTh.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp index 85ae0a3..340c0d9 100644 --- a/src/ModelCheckerTh.cpp +++ b/src/ModelCheckerTh.cpp @@ -151,8 +151,6 @@ void* ModelCheckerTh::Compute_successors() { while (!e.second.empty() && !m_finish) { int t = *e.second.begin(); e.second.erase(t); - - if (id_thread) { pthread_mutex_lock(&m_supervise_gc_mutex); m_gc++; @@ -161,17 +159,13 @@ void* ModelCheckerTh::Compute_successors() { } pthread_mutex_unlock(&m_supervise_gc_mutex); } - - //MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0); /*ldd_refs_push(reduced_meta);*/ - if (id_thread == 0) { pthread_mutex_lock(&m_gc_mutex); // #ifdef DEBUG_GC //displayMDDTableInfo(); // #endif // DEBUG_GC - sylvan_gc_seq(); // #ifdef DEBUG_GC //displayMDDTableInfo(); @@ -182,18 +176,13 @@ void* ModelCheckerTh::Compute_successors() { ldd_refs_push(reduced_meta); reached_class = new LDDState(); reached_class->m_lddstate = reduced_meta; - - //pthread_spin_lock(&m_accessible); pthread_mutex_lock(&m_graph_mutex); - LDDState *pos = m_graph->find(reached_class); - if (!pos) { // cout<<"not found"<<endl; //reached_class->blocage=Set_Bloc(Complete_meta_state); //reached_class->boucle=Set_Div(Complete_meta_state); - m_graph->addArc(); m_graph->insert(reached_class); -- GitLab