Clean-up
This commit is contained in:
4
mc.cc
4
mc.cc
@@ -80,6 +80,10 @@ inline BDD ModelChecker::getSucc(const BDD &states)
|
|||||||
}
|
}
|
||||||
|
|
||||||
q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv);
|
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_ctx_E);
|
||||||
q = q.ExistAbstract(*pv_proc_enab_E);
|
q = q.ExistAbstract(*pv_proc_enab_E);
|
||||||
|
|
||||||
|
|||||||
3
symrs.cc
3
symrs.cc
@@ -681,8 +681,6 @@ void SymRS::encodeTransitions(void)
|
|||||||
|
|
||||||
for (const auto &prod : products) {
|
for (const auto &prod : products) {
|
||||||
*monoTrans *= encEntityProduction(proc_id, prod);
|
*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
|
BDD SymRS::encActStrEntity(std::string name) const
|
||||||
{
|
{
|
||||||
|
assert(0); // TODO for rsCTL
|
||||||
/*
|
/*
|
||||||
int id = getMappedStateToActID(rs->getEntityID(name));
|
int id = getMappedStateToActID(rs->getEntityID(name));
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user