diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index 2df164ffa75bc76302161c546d550f53744de108..b8eae2a747ab632d102c8d666005ff468966c19b 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -126,7 +126,7 @@ string temp; return temp; } -TASK_3 (MDD, Accessible_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation) +TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation) { MDD M1; MDD M2=From; @@ -150,7 +150,7 @@ TASK_3 (MDD, Accessible_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tra return M2; } -TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, tb_relation) +TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, tb_relation) { Set res; for(Set::const_iterator i=observable->begin(); !(i==observable->end()); i++) @@ -166,15 +166,17 @@ TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>* return res; } -#define firable_obs_lace(state,obser,tb) CALL(firable_obs_lace, state, obser,tb) +#define fire_obs_lace(state,obser,tb) CALL(fire_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)); - Set fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation); + 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); // c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this); + m_graph->setInitialState(c); + m_graph->insert(c); return c; } diff --git a/src/SogKripkeStateOTF.cpp b/src/SogKripkeStateOTF.cpp index c86bc26d9ebfbe2c49862804812a18e7e3356f7c..99b5a5163f2bf19683b4feaad5c7d31ed2bebd86 100644 --- a/src/SogKripkeStateOTF.cpp +++ b/src/SogKripkeStateOTF.cpp @@ -7,10 +7,7 @@ SogKripkeStateOTF::~SogKripkeStateOTF() { //dtor } -SogKripkeStateOTF::SogKripkeStateOTF(const MDD& m) - : spot::state(), ma(m) -{ -} // + SogKripkeStateOTF* SogKripkeStateOTF::clone() const diff --git a/src/SogKripkeStateOTF.h b/src/SogKripkeStateOTF.h index 674ce257d298dd22bf99c0a4d6fa1c75d01865b0..0a50e6e8c1847a67b0f3740bca85f170966b9807 100644 --- a/src/SogKripkeStateOTF.h +++ b/src/SogKripkeStateOTF.h @@ -7,7 +7,7 @@ class SogKripkeStateOTF : public spot::state { public: - SogKripkeStateOTF(const MDD &m); + SogKripkeStateOTF(LDDState *st):m_state(st) {}; virtual ~SogKripkeStateOTF(); SogKripkeStateOTF* clone() const override;