From 95d8123a6ba2752ef8ca4bb813eb950af6954f1f Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Tue, 3 Apr 2018 20:05:50 +0100 Subject: [PATCH] Working DRS with one process --- mc.cc | 20 ++++++++++++++------ mc.hh | 4 +++- symrs.cc | 50 ++++++++++++++++++++++---------------------------- symrs.hh | 17 +++++++---------- 4 files changed, 46 insertions(+), 45 deletions(-) diff --git a/mc.cc b/mc.cc index 00e56c4..b0a148a 100644 --- a/mc.cc +++ b/mc.cc @@ -16,7 +16,15 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts) pv_succ = srs->getEncPVsucc(); pv_E = srs->getEncPV_E(); pv_succ_E = srs->getEncPVsucc_E(); - pv_act_E = srs->getEncPVact_E(); + pv_ctx_E = srs->getEncPVctx_E(); + pv_proc_enab_E = srs->getEncPVproc_enab_E(); + + assert(pv != nullptr); + assert(pv_succ != nullptr); + assert(pv_E != nullptr); + assert(pv_succ_E != nullptr); + assert(pv_ctx_E != nullptr); + assert(pv_proc_enab_E != nullptr); // // Transition relations @@ -69,10 +77,12 @@ inline BDD ModelChecker::getSucc(const BDD &states) } else { q *= states * *trm; + BDD_PRINT(q); } q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv); - q = q.ExistAbstract(*pv_act_E); + q = q.ExistAbstract(*pv_ctx_E); + q = q.ExistAbstract(*pv_proc_enab_E); return q; } @@ -93,7 +103,7 @@ inline BDD ModelChecker::getPreE(const BDD &states) } q = q.ExistAbstract(*pv_succ_E); - q = q.ExistAbstract(*pv_act_E); + q = q.ExistAbstract(*pv_ctx_E); return q; } @@ -113,7 +123,7 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts) } q = q.ExistAbstract(*pv_succ_E); - q = q.ExistAbstract(*pv_act_E); + q = q.ExistAbstract(*pv_ctx_E); return q; } @@ -147,9 +157,7 @@ void ModelChecker::printReach(void) } dropCtxAutStatePart(*reach); - srs->printDecodedRctSysStates(*reach); - cleanup(); if (opts->measure) { diff --git a/mc.hh b/mc.hh index f6d7557..66307c4 100644 --- a/mc.hh +++ b/mc.hh @@ -25,7 +25,7 @@ class ModelChecker vector *pv_succ; BDD *pv_E; BDD *pv_succ_E; - BDD *pv_act_E; + BDD *pv_ctx_E; BDD *reach; vector *trp; BDD *trm; @@ -37,6 +37,8 @@ class ModelChecker BDD *pv_ca_E; BDD *pv_ca_succ_E; + BDD *pv_proc_enab_E; + unsigned int trp_size; unsigned int totalStateVars; diff --git a/symrs.cc b/symrs.cc index d99362e..f2c4cc2 100644 --- a/symrs.cc +++ b/symrs.cc @@ -215,27 +215,18 @@ void SymRS::initBDDvars(void) VERB_LN(2, "Variables for process enabledness/activity"); pv_proc_enab = new BDDvec(numberOfProc); + pv_proc_enab_E = new BDD(BDD_TRUE); for (unsigned int i = 0; i < numberOfProc; ++i) { - (*pv_proc_enab)[i] = cuddMgr->bddVar(bdd_var_idx++); + auto bdd_var = cuddMgr->bddVar(bdd_var_idx++); + (*pv_proc_enab)[i] = bdd_var; + *pv_proc_enab_E *= bdd_var; } // ---------------------------------------------------------- // Context Entities // ---------------------------------------------------------- - // // Actions/Contexts - // pv_act = new BDDvec(totalActions); - // pv_act_E = new BDD(BDD_TRUE); - // - // // TODO - // // Actions need also per-process PV and flattened PV - // - // for (unsigned int i = 0; i < totalActions; ++i) { - // (*pv_act)[i] = cuddMgr->bddVar(bdd_var_idx++); - // *pv_act_E *= (*pv_act)[i]; - // } - VERB_LN(2, "Variables for context entities"); pv_ctx = new BDDvec(totalCtxEntities); @@ -526,26 +517,33 @@ BDD SymRS::compContext(const BDD &context) const std::string SymRS::decodedRctSysStateToStr(const BDD &state) { - assert(0); std::string s = "{ "; - /* - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { - if (!(encEntity(i) * state).IsZero()) { - s += rs->entityToStr(i) + " "; + + for (const auto &proc_entities : usedProducts) { + + auto proc_id = proc_entities.first; + auto entities = proc_entities.second; + s += rs->getProcessName(proc_id) + "={ "; + + for (const auto &entity : entities) { + if (!(encEntity(proc_id, entity) * state).IsZero()) { + s += rs->entityToStr(entity) + " "; + } } + + s += "} "; } - */ + s += "}"; return s; } void SymRS::printDecodedRctSysStates(const BDD &states) { - assert(0); BDD unproc = states; while (!unproc.IsZero()) { - BDD t = unproc.PickOneMinterm(*pv_rs); + BDD t = unproc.PickOneMinterm(*pv_drs_flat); cout << decodedRctSysStateToStr(t) << endl; if (opts->verbose > 9) { @@ -663,7 +661,9 @@ void SymRS::encodeTransitions(void) auto products = proc_products.second; 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)); } } @@ -682,12 +682,6 @@ void SymRS::encodeTransitions(void) } } -BDD SymRS::encNoContext(void) -{ - assert(0); - return BDD_FALSE; -} - void SymRS::encodeInitStates(void) { if (usingContextAutomaton()) { diff --git a/symrs.hh b/symrs.hh index 040d476..71387f4 100644 --- a/symrs.hh +++ b/symrs.hh @@ -51,9 +51,13 @@ class SymRS { return pv_succ_E; } - BDD *getEncPVact_E(void) + BDD *getEncPVctx_E(void) { - return pv_act_E; + return pv_ctx_E; + } + BDD *getEncPVproc_enab_E(void) + { + return pv_proc_enab_E; } BDDvec *getEncPartTrans(void) { @@ -206,12 +210,7 @@ class SymRS BDD *pv_succ_E; BDDvec *pv_proc_enab; /*!< Variables indicating if a process is enabled */ - - BDDvec *pv_rs; // remove - BDDvec *pv_rs_succ; // remove - - BDD *pv_rs_E; // remove - BDD *pv_rs_succ_E; // remove + BDD *pv_proc_enab_E; vector *pv_drs; /*!< PVs for the product part of state (per DRS process) */ @@ -323,8 +322,6 @@ class SymRS std::string decodedRctSysStateToStr(const BDD &state); void printDecodedRctSysStates(const BDD &states); - BDD encNoContext(void); - DecompReactions getProductionConditions(Process proc_id); void initBDDvars(void);