diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 338945b375d90f0635535a494259341f58b9402f..7e76293f89fa9c8d089aefbbab482c7821f2bc08 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -140,13 +140,11 @@ LDDState * ModelCheckerTh::buildInitialMetaState()
m_graph->insert(c);
Set fire=firable_obs(initial_meta_state);
int j=0;
- for(auto it=fire.begin();it!=fire.end();it++,j++)
- m_st[j%m_nb_thread].push(couple_th(c,*it));
- cout<<"Before barrier 1 "<<__func__<<endl;
+ for(auto it=fire.begin(); it!=fire.end(); it++,j++)
+ m_st[j%m_nb_thread].push(couple_th(c,*it));
pthread_barrier_wait(&m_barrier_threads);
- cout<<"Before barrier 2 "<<__func__<<endl;
pthread_barrier_wait(&m_barrier_builder);
- cout<<"Leaving "<<__func__<<endl;
+ c->setVisited();
return c;
}
@@ -154,13 +152,11 @@ void ModelCheckerTh::buildSucc(LDDState *agregate)
{
if (!agregate->isVisited())
{
- agregate->setVisited();
-
-
- Set fire=firable_obs(agregate->getLDDValue());
+ agregate->setVisited();
+ Set fire=firable_obs(agregate->getLDDValue());
int j=0;
- for(auto it=fire.begin();it!=fire.end();it++,j++)
- m_st[j%m_nb_thread].push(couple_th(agregate,*it));
+ for(auto it=fire.begin(); it!=fire.end(); it++,j++)
+ m_st[j%m_nb_thread].push(couple_th(agregate,*it));
pthread_barrier_wait(&m_barrier_threads);
pthread_barrier_wait(&m_barrier_builder);
//Wait for all threads to finish their work
@@ -182,100 +178,58 @@ void * ModelCheckerTh::Compute_successors()
cout<<"Thread id : "<<id_thread<<endl;
do
{
- cout<<"Before barrier threads "<<__func__<<" Thread id "<<id_thread<<endl;
pthread_barrier_wait(&m_barrier_threads);
while (!m_st[id_thread].empty())
{
-
- pthread_spin_lock(&m_spin_stack[id_thread]);
couple_th elt=m_st[id_thread].top();
- //pthread_spin_lock(&m_accessible);
m_st[id_thread].pop();
-
- pthread_spin_unlock(&m_spin_stack[id_thread]);
LDDState *aggregate=elt.first;
MDD meta_state=aggregate->getLDDValue();
int transition=elt.second;
-
- //compute successors
-
-
-
-
- MDD complete_state=Accessible_epsilon(get_successor(meta_state,transition));
-
- reached_class=new LDDState;
- reached_class->m_lddstate=complete_state;
- pthread_mutex_lock(&m_graph_mutex);
- LDDState* pos=m_graph->find(reached_class);
-
- if(!pos)
- {
- m_graph->addArc();
- m_graph->insert(reached_class);
- pthread_mutex_unlock(&m_graph_mutex);
- aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(reached_class,transition));
- reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(aggregate,transition));
-
- }
- else
- {
- m_graph->addArc();
- pthread_mutex_unlock(&m_graph_mutex);
- aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(pos,transition));
- pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(aggregate,transition));
- delete reached_class;
- }
+ MDD complete_state=Accessible_epsilon(get_successor(meta_state,transition));
+ reached_class=new LDDState;
+ reached_class->m_lddstate=complete_state;
+ pthread_mutex_lock(&m_graph_mutex);
+ LDDState* pos=m_graph->find(reached_class);
+ if(!pos)
+ {
+ m_graph->addArc();
+ m_graph->insert(reached_class);
+ pthread_mutex_unlock(&m_graph_mutex);
+ aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(reached_class,transition));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(aggregate,transition));
+ }
+ else
+ {
+ m_graph->addArc();
+ pthread_mutex_unlock(&m_graph_mutex);
+ aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(pos,transition));
+ pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(aggregate,transition));
+ delete reached_class;
+ }
}
- cout<<"Before barrier builder "<<__func__<<" Thread id "<<id_thread<<endl;
pthread_barrier_wait(&m_barrier_builder);
-
}
while (1);
}
-bool ModelCheckerTh::isNotTerminated()
-{
- bool res=true;
- int i=0;
- while (i<m_nb_thread && res)
- {
- res=m_terminaison[i];
- i++;
- }
- return !res;
-}
-int ModelCheckerTh::minCharge()
-{
- int pos=0;
- int min_charge=m_charge[0];
- for (int i=1; i<m_nb_thread; i++)
- {
- if (m_charge[i]<min_charge)
- {
- min_charge=m_charge[i];
- pos=i;
- }
- }
- return pos;
-
-}
void * ModelCheckerTh::threadHandler(void *context)
{
return ((ModelCheckerTh*)context)->Compute_successors();
}
-void ModelCheckerTh::ComputeTh_Succ(){
+void ModelCheckerTh::ComputeTh_Succ()
+{
int rc;
- // m_graph=&g;
- // m_graph->setTransition(m_transitionName);
- // m_graph->setPlace(m_placeName);
+// m_graph=&g;
+// m_graph->setTransition(m_transitionName);
+// m_graph->setPlace(m_placeName);
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
@@ -294,11 +248,11 @@ void ModelCheckerTh::ComputeTh_Succ(){
cout<<"error: pthread_create, rc: "<<rc<<endl;
}
}
- /* Compute_successors();
- for (int i = 0; i < m_nb_thread-1; i++)
- {
- pthread_join(m_list_thread[i], NULL);
- }*/
+ /* Compute_successors();
+ for (int i = 0; i < m_nb_thread-1; i++)
+ {
+ pthread_join(m_list_thread[i], NULL);
+ }*/
}
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index 305096658fc736dc898ae801dc2e7e4e0fd43254..e92aea86b4177a50159370bc62e2b80bdb89a976 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -15,20 +15,13 @@ public:
static void *threadHandler(void *context);
void *Compute_successors();
void ComputeTh_Succ();
- int minCharge();
- bool isNotTerminated();
-
-
private:
int m_nb_thread;
MDD m_initalMarking;
int m_min_charge;
pile_t m_st[128];
int m_charge[128];
- bool m_terminaison[128];
- int m_id_thread;
-
-
+ int m_id_thread;
pthread_mutex_t m_mutex;
pthread_mutex_t m_graph_mutex;
pthread_mutex_t m_gc_mutex;
@@ -38,7 +31,6 @@ private:
unsigned int m_gc;
pthread_mutex_t m_mutex_stack[128];
- pthread_spinlock_t m_spin_stack[128];
pthread_t m_list_thread[128];
};
#endif