diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index 72343382aa42f089b121e4155fe9b0aa11878d09..2df164ffa75bc76302161c546d550f53744de108 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -126,12 +126,62 @@ string temp; return temp; } +TASK_3 (MDD, Accessible_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation) +{ + MDD M1; + MDD M2=From; + int it=0; + //cout<<"worker "<<lace_get_worker()->worker<<endl; + do + { + M1=M2; + for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++) + { + SPAWN(lddmc_firing_lace,M2,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus()); + } + for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++) + { + MDD succ=SYNC(lddmc_firing_lace); + M2=lddmc_union(succ,M2); + } + + } + while(M1!=M2); + return M2; +} + +TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, tb_relation) +{ + Set res; + for(Set::const_iterator i=observable->begin(); !(i==observable->end()); i++) + { + MDD succ = lddmc_firing_lace(State,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus()); + if(succ!=lddmc_false) + { + res.insert(*i); + + } + + } + return res; +} + +#define firable_obs_lace(state,obser,tb) CALL(firable_obs_lace, state, obser,tb) + LDDState * ModelCheckLace::buildInitialMetaState() { LDDState *c=new LDDState; LACE_ME; MDD initial_meta_state(CALL(Accessible_epsilon_lace,m_initalMarking,&m_nonObservable,&m_tb_relation)); - fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation); - m_nbmetastate++; - c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this); + Set fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation); + + // c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this); return c; } + +LDDState * ModelCheckLace::buildSucc(LDDState *agregate) { + + LDDState *trmp=nullptr; + return trmp; +} + + diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h index 40e7d4dd921269d085eec815cdf0c087633d8110..4c1e1ff1d3c983b2a59d274d723f240344dfa82c 100644 --- a/src/ModelCheckLace.h +++ b/src/ModelCheckLace.h @@ -7,6 +7,7 @@ public: LDDState * buildInitialMetaState(); string getTransition(int pos); string getPlace(int pos); + LDDState * buildSucc(LDDState *agregate); private: int m_nb_thread; MDD m_initalMarking;