diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index 000280670863a399d44054b2caa7e8dcefb776b9..e9d174b9d8ad33ca4472d0b90de3f0826dffbfdf 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -173,7 +173,7 @@ TASK_3 (bool, SetDivL, MDD, M, Set*, nonObservable, vector<TransSylvan>*, tb_rel if (nonObservable->empty()) return false; Set::iterator i; MDD Reached,From; - //cout<<"Ici detect divergence \n"; + Reached=lddmc_false; From=M; do @@ -256,15 +256,15 @@ LDDState * ModelCheckLace::getInitialMetaState() void ModelCheckLace::buildSucc(LDDState *agregate) { - cout<<__func__<<endl; + //cout<<__func__<<endl; if (!agregate->isVisited()) { // It's first time to visit agregate, then we have to build its successors agregate->setVisited(); LDDState *reached_class=nullptr; LACE_ME; - displayMDDTableInfo(); + //displayMDDTableInfo(); sylvan_gc(); - displayMDDTableInfo(); + //displayMDDTableInfo(); MDD meta_state=agregate->getLDDValue();//(CALL(Aggregate_epsilon_lace,agregate->getLDDValue(),&m_nonObservable,&m_tb_relation)); Set fire=fire_obs_lace(meta_state,&m_observable,&m_tb_relation);