diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp index b155c67f1c615de8d56d53c80dbf8f516f52b447..7e91dcacda8a4e1d6e1f1bb841ee5df6b2b53f6e 100644 --- a/src/ModelCheckerTh.cpp +++ b/src/ModelCheckerTh.cpp @@ -130,7 +130,7 @@ string ModelCheckerTh::getPlace(int pos) LDDState * ModelCheckerTh::buildInitialMetaState() { - + ComputeTh_Succ(); LDDState *c=new LDDState; cout<<"Initial marking : "<<m_initalMarking<<endl; MDD initial_meta_state=Accessible_epsilon(m_initalMarking); @@ -138,8 +138,11 @@ LDDState * ModelCheckerTh::buildInitialMetaState() c->m_lddstate=initial_meta_state; m_graph->setInitialState(c); m_graph->insert(c); - m_st[0].push(c); - ComputeTh_Succ(); + 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)); + return c; } @@ -148,10 +151,13 @@ void ModelCheckerTh::buildSucc(LDDState *agregate) if (!agregate->isVisited()) { agregate->setVisited(); - m_min_charge=minCharge(); - pthread_spin_lock(&m_spin_stack[m_min_charge]); - m_st[m_min_charge].push(agregate); - pthread_spin_unlock(&m_spin_stack[m_min_charge]); + + + 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)); + //Wait for all threads to finish their work } } @@ -176,23 +182,22 @@ void * ModelCheckerTh::Compute_successors() nb_it++; m_terminaison[id_thread]=false; pthread_spin_lock(&m_spin_stack[id_thread]); - LDDState* agregate=m_st[id_thread].top(); + 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]); - // m_nbmetastate--; - MDD meta_state=agregate->getLDDValue(); - Set fire=firable_obs(meta_state); + LDDState *aggregate=elt.first; + MDD meta_state=aggregate->getLDDValue(); + int transition=elt.second; //compute successors - Set::const_iterator iter=fire.begin(); - while(iter!=fire.end()) - { - int t = *iter; - MDD complete_state=Accessible_epsilon(get_successor(meta_state,t)); - iter++; + + + + 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); @@ -203,19 +208,19 @@ void * ModelCheckerTh::Compute_successors() m_graph->addArc(); m_graph->insert(reached_class); pthread_mutex_unlock(&m_graph_mutex); - agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(reached_class,t)); - reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(agregate,t)); + 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); - agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(pos,t)); - pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(agregate,t)); + aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(pos,transition)); + pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(aggregate,transition)); delete reached_class; } - } + } m_terminaison[id_thread]=true; } diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h index 2d31b0319537583cb9ee2c8752f5132d1191e9d5..e7e58778981a99462060f6196d8b73a73742bcfa 100644 --- a/src/ModelCheckerTh.h +++ b/src/ModelCheckerTh.h @@ -1,7 +1,8 @@ #ifndef MODELCHECKERTH_H #define MODELCHECKERTH_H #include "CommonSOG.h" -typedef stack<LDDState *> pile_t; +typedef pair<LDDState *, int> couple_th; +typedef stack<pair<LDDState *,int>> pile_t; class ModelCheckerTh : public CommonSOG {