diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index 2cf50d13e749134ae4756e719fff95f5b0880966..69d802d88744927a396730d84ce13e7724d582fd 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -214,6 +214,47 @@ void ModelCheckLace::buildSucc(LDDState *agregate) { if (!agregate->isVisited()) { // It's first time to visit agregate, then we have to build its successors + LDDState *reached_class=nullptr; + LACE_ME; + MDD meta_state(CALL(Aggregate_epsilon_lace,agregate->getLDDValue(),&m_nonObservable,&m_tb_relation)); + + Set fire=fire_obs_lace(meta_state,&m_observable,&m_tb_relation); + unsigned int onb_it=0; + Set::const_iterator iter=fire.begin(); + while(iter!=fire.end()) + { + int t = *iter; + SPAWN(Aggregate_epsilon_lace,get_successor(meta_state,t),&m_nonObservable,&m_tb_relation); + onb_it++;iter++; + } + + for (unsigned int i=0; i<onb_it; i++) + { + Set::iterator it = fire.end(); + it--; + int t=*it; + fire.erase(it); + MDD Complete_meta_state=SYNC(Aggregate_epsilon_lace); + reached_class=new LDDState; + reached_class->m_lddstate=Complete_meta_state; + LDDState* pos=m_graph->find(reached_class); + + if(!pos) + { + m_graph->addArc(); + m_graph->insert(reached_class); + agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(reached_class,t)); + reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(agregate,t)); + + } + else + { + m_graph->addArc(); + agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(pos,t)); + pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(agregate,t)); + delete reached_class; + } + } }