diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index b8eae2a747ab632d102c8d666005ff468966c19b..cb13980bb75f2d16e71d17b0dc6736a526afce17 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -116,14 +116,16 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread) } -string ModelCheckLace::getTransition(int pos) { -string temp; -return temp; +string ModelCheckLace::getTransition(int pos) +{ + string temp; + return temp; } -string ModelCheckLace::getPlace(int pos) { -string temp; -return temp; +string ModelCheckLace::getPlace(int pos) +{ + string temp; + return temp; } TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation) @@ -168,8 +170,10 @@ TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, t #define fire_obs_lace(state,obser,tb) CALL(fire_obs_lace, state, obser,tb) -LDDState * ModelCheckLace::buildInitialMetaState() { +LDDState * ModelCheckLace::buildInitialMetaState() +{ LDDState *c=new LDDState; + LDDState *reached_class; LACE_ME; MDD initial_meta_state(CALL(Aggregate_epsilon_lace,m_initalMarking,&m_nonObservable,&m_tb_relation)); Set fire=fire_obs_lace(initial_meta_state,&m_observable,&m_tb_relation); @@ -177,11 +181,37 @@ LDDState * ModelCheckLace::buildInitialMetaState() { // c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this); m_graph->setInitialState(c); m_graph->insert(c); + // Compute successors + unsigned int onb_it=0; + Set::const_iterator iter=fire.begin(); + while(iter!=fire.end()) + { + int t = *iter; + + SPAWN(Aggregate_epsilon_lace,get_successor(initial_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; + m_graph->addArc(); + m_graph->insert(reached_class); + c->Successors.insert(c->Successors.begin(),LDDEdge(reached_class,t)); + reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(c,t)); + } return c; } -LDDState * ModelCheckLace::buildSucc(LDDState *agregate) { - +LDDState * ModelCheckLace::buildSucc(LDDState *agregate) +{ LDDState *trmp=nullptr; return trmp; } diff --git a/src/SogKripkeStateOTF.cpp b/src/SogKripkeStateOTF.cpp index 99b5a5163f2bf19683b4feaad5c7d31ed2bebd86..5c34da89dd6aec8282bf6c50270c14fdbfb92ee7 100644 --- a/src/SogKripkeStateOTF.cpp +++ b/src/SogKripkeStateOTF.cpp @@ -8,8 +8,6 @@ SogKripkeStateOTF::~SogKripkeStateOTF() //dtor } - - SogKripkeStateOTF* SogKripkeStateOTF::clone() const { return new SogKripkeStateOTF(*this); @@ -30,8 +28,3 @@ int SogKripkeStateOTF::compare(const spot::state* other) const else return h > oh; } - -const MDD& SogKripkeStateOTF::get_marking() const -{ - return ma; -} // diff --git a/src/SogKripkeStateOTF.h b/src/SogKripkeStateOTF.h index 0a50e6e8c1847a67b0f3740bca85f170966b9807..0e4135907296eb65794e9937c840c22aac920895 100644 --- a/src/SogKripkeStateOTF.h +++ b/src/SogKripkeStateOTF.h @@ -19,13 +19,8 @@ public: { return m_state; } - const MDD& get_marking() const; - double limit_marking(const bdd& m); - - private: LDDState *m_state; - MDD ma; }; diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp index a281b20c05b64112fca0e054787d4a192f9a6596..0481ca45f49e6d0244deac6e1bbcf1371d244d58 100644 --- a/src/threadSOG.cpp +++ b/src/threadSOG.cpp @@ -816,7 +816,7 @@ void threadSOG::computeSOGLace(LDDGraph &g) while(iter!=e.second.end()) { int t = *iter; - cout<<"Transition order1: "<<*iter<<endl; + //cout<<"Transition order1: "<<*iter<<endl; //e.second.erase(t); SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&m_nonObservable,&m_tb_relation); onb_it++;iter++;