diff --git a/mc.cc b/mc.cc
index 0b33196..eda6a2e 100644
--- a/mc.cc
+++ b/mc.cc
@@ -80,6 +80,10 @@ inline BDD ModelChecker::getSucc(const BDD &states)
   }
 
   q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv);
+
+  // we should have one BDD for cleaning up
+  // it should be calculated at the very beginning
+
   q = q.ExistAbstract(*pv_ctx_E);
   q = q.ExistAbstract(*pv_proc_enab_E);
 
diff --git a/symrs.cc b/symrs.cc
index 040d8bd..32889d6 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -681,8 +681,6 @@ void SymRS::encodeTransitions(void)
 
     for (const auto &prod : products) {
       *monoTrans *= encEntityProduction(proc_id, prod);
-      cout << rs->getProcessName(proc_id) << " " << rs->getEntityName(prod) << endl;
-      BDD_PRINT(encEntityProduction(proc_id, prod));
     }
   }
 
@@ -727,6 +725,7 @@ void SymRS::encodeInitStatesForCtxAut(void)
 
 BDD SymRS::encActStrEntity(std::string name) const
 {
+  assert(0); // TODO for rsCTL
   /*
   int id = getMappedStateToActID(rs->getEntityID(name));