From ae740fa88547973570b2f10ba0e3a4c94f8b4b24 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Tue, 27 Mar 2018 18:19:06 +0100 Subject: [PATCH] PV vectors for global state with CA, states printing (resolved an issue with duplicates) --- mc.cc | 32 +++++++++--- mc.hh | 11 ++-- symrs.cc | 150 ++++++++++++++++++++++++------------------------------- symrs.hh | 42 ++++++++++++---- 4 files changed, 130 insertions(+), 105 deletions(-) diff --git a/mc.cc b/mc.cc index c113a96..2ec8873 100644 --- a/mc.cc +++ b/mc.cc @@ -1,6 +1,7 @@ #include "mc.hh" ModelChecker::ModelChecker(SymRS *srs, Options *opts) + : using_ctx_aut(false) { this->srs = srs; this->opts = opts; @@ -34,10 +35,19 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts) if (srs->usingContextAutomaton()) { - // ca_init_state = srs->getEncCtxAutInitState(); + using_ctx_aut = true; pv_ca = srs->getEncCtxAutPV(); pv_ca_succ = srs->getEncCtxAutPVsucc(); - // ca_tr = srs->getEncCtxAutTrans(); + pv_ca_E = srs->getEncCtxAutPV_E(); + pv_ca_succ_E = srs->getEncCtxAutPVsucc_E(); + } + else + { + using_ctx_aut = false; + pv_ca = nullptr; + pv_ca_succ = nullptr; + pv_ca_E = nullptr; + pv_ca_succ_E = nullptr; } // Initialise the set of reachable states @@ -62,7 +72,7 @@ inline BDD ModelChecker::getSucc(const BDD &states) } q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv); q = q.ExistAbstract(*pv_act_E); - + return q; } @@ -104,6 +114,11 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts) return q; } +void ModelChecker::dropCtxAutStatePart(BDD &states) +{ + states = states.ExistAbstract(*pv_ca_E); +} + void ModelChecker::printReach(void) { VERB_LN(2, "Printing/generating reachable states"); @@ -127,8 +142,10 @@ void ModelChecker::printReach(void) reach_p = *reach; *reach += getSucc(*reach); } + + dropCtxAutStatePart(*reach); - srs->printDecodedStates(*reach); + srs->printDecodedRctSysStates(*reach); cleanup(); @@ -159,11 +176,12 @@ void ModelChecker::printReachWithSucc(void) { BDD t; t = unproc.PickOneMinterm(*pv); - cout << "Successors of " << srs->decodedStateToStr(t) << ":" << endl; - srs->printDecodedStates(getSucc(t)); + cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl; + srs->printDecodedRctSysStates(getSucc(t)); unproc -= t; } - cleanup(); + + cleanup(); } bool ModelChecker::checkReach(const Entities testState) diff --git a/mc.hh b/mc.hh index 04868a0..20d22fb 100644 --- a/mc.hh +++ b/mc.hh @@ -31,15 +31,20 @@ class ModelChecker BDD *trm; // Context Automaton + bool using_ctx_aut; vector *pv_ca; vector *pv_ca_succ; - // BDD *ca_tr; - // BDD *ca_init_state; + BDD *pv_ca_E; + BDD *pv_ca_succ_E; unsigned int trp_size; unsigned int totalStateVars; + + /** + * @brief Abstracts away (in-place!) the context automaton states + */ + void dropCtxAutStatePart(BDD &states); - BDD zeroFill(const BDD &state); BDD getSucc(const BDD &states); BDD getPreE(const BDD &states); BDD getPreEctx(const BDD &states, const BDD *contexts); diff --git a/symrs.cc b/symrs.cc index 680135c..6440e93 100644 --- a/symrs.cc +++ b/symrs.cc @@ -10,12 +10,14 @@ SymRS::SymRS(RctSys *rs, Options *opts) { this->rs = rs; this->opts = opts; - totalStateVars = rs->getEntitiesSize(); + totalRctSysStateVars = rs->getEntitiesSize(); totalReactions = rs->getReactionsSize(); totalActions = rs->getActionsSize(); totalCtxAutStateVars = getCtxAutStateEncodingSize(); + totalStateVars = totalRctSysStateVars + totalCtxAutStateVars; + partTrans = nullptr; monoTrans = nullptr; @@ -119,7 +121,7 @@ BDD SymRS::compState(const BDD &state) const { BDD s = state; - for (unsigned int i = 0; i < totalStateVars; ++i) + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { if (!(*pv)[i] * state != cuddMgr->bddZero()) s *= !(*pv)[i]; @@ -141,10 +143,10 @@ BDD SymRS::compContext(const BDD &context) const return c; } -std::string SymRS::decodedStateToStr(const BDD &state) +std::string SymRS::decodedRctSysStateToStr(const BDD &state) { std::string s = "{ "; - for (unsigned int i = 0; i < totalStateVars; ++i) + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { if (!(encEntity(i) * state).IsZero()) { @@ -155,13 +157,13 @@ std::string SymRS::decodedStateToStr(const BDD &state) return s; } -void SymRS::printDecodedStates(const BDD &states) +void SymRS::printDecodedRctSysStates(const BDD &states) { BDD unproc = states; while (!unproc.IsZero()) { - BDD t = unproc.PickOneMinterm(*pv); - cout << decodedStateToStr(t) << endl; + BDD t = unproc.PickOneMinterm(*pv_rs); + cout << decodedRctSysStateToStr(t) << endl; if (opts->verbose > 9) { t.PrintMinterm(); cout << endl; @@ -178,17 +180,37 @@ void SymRS::initBDDvars(void) VERB("Preparing BDD variables"); - unsigned int needed_state_vars = totalStateVars; - if (usingContextAutomaton()) - needed_state_vars += totalCtxAutStateVars; + // used for bddVar + unsigned int bdd_var_idx = 0; - pv = new vector(needed_state_vars); - pv_succ = new vector(needed_state_vars); - pv_act = new vector(totalActions); + // used for pv, pv_succ + unsigned int global_state_idx = 0; + + // Variables for reaction system with CA (if used) + pv = new vector(totalStateVars); + pv_succ = new vector(totalStateVars); pv_E = new BDD(BDD_TRUE); pv_succ_E = new BDD(BDD_TRUE); - pv_act_E = new BDD(BDD_TRUE); + + // Reaction system (no actions, no CA) + pv_rs = new vector(totalRctSysStateVars); + pv_rs_succ = new vector(totalRctSysStateVars); + pv_rs_E = new BDD(BDD_TRUE); + pv_rs_succ_E = new BDD(BDD_TRUE); + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) + { + (*pv_rs)[i] = cuddMgr->bddVar(bdd_var_idx++); + (*pv_rs_succ)[i] = cuddMgr->bddVar(bdd_var_idx++); + *pv_rs_E *= (*pv_rs)[i]; + *pv_rs_succ_E *= (*pv_rs_succ)[i]; + + (*pv)[global_state_idx] = (*pv_rs)[i]; + (*pv_succ)[global_state_idx] = (*pv_rs_succ)[i]; + ++global_state_idx; + } + + // CA if (usingContextAutomaton()) { VERB("Context automaton variables"); @@ -197,73 +219,40 @@ void SymRS::initBDDvars(void) pv_ca_succ = new vector(totalCtxAutStateVars); pv_ca_E = new BDD(BDD_TRUE); pv_ca_succ_E = new BDD(BDD_TRUE); - } - VERB_LN(3, "Preparing individual variables"); - - for (unsigned int i = 0; i < needed_state_vars; ++i) - { - (*pv)[i] = cuddMgr->bddVar(i*2); - (*pv_succ)[i] = cuddMgr->bddVar((i*2)+1); - - *pv_E *= (*pv)[i]; - *pv_succ_E *= (*pv_succ)[i]; - - if (i >= totalStateVars) + for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) { - VERB_LN(3, "Preparing CA variables"); - unsigned int ca_i = i - totalStateVars; - - (*pv_ca)[ca_i] = (*pv)[i]; - (*pv_ca_succ)[ca_i] = (*pv_succ)[i]; + (*pv_ca)[i] = cuddMgr->bddVar(bdd_var_idx++); + (*pv_ca_succ)[i] = cuddMgr->bddVar(bdd_var_idx++); + *pv_ca_E *= (*pv_ca)[i]; + *pv_ca_succ_E *= (*pv_ca_succ)[i]; - *pv_ca_E *= (*pv)[i]; - *pv_ca_succ_E *= (*pv_succ)[i]; + (*pv)[global_state_idx] = (*pv_ca)[i]; + (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i]; + ++global_state_idx; } - } - - // first index after state vars - unsigned int offset = needed_state_vars * 2; - - // if (usingContextAutomaton()) - // { - // VERB("Context automaton variables"); - // - // pv_ca = new vector(totalCtxAutStateVars); - // pv_ca_succ = new vector(totalCtxAutStateVars); - // pv_ca_E = new BDD(BDD_TRUE); - // pv_ca_succ_E = new BDD(BDD_TRUE); - // - // // - // // BDD variables for encoding local states of context automaton - // // - // unsigned int base_index = offset; - // for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) - // { - // (*pv_ca)[i] = cuddMgr->bddVar(base_index); - // (*pv_ca_succ)[i] = cuddMgr->bddVar(base_index+1); - // - // *pv_ca_E *= (*pv_ca)[i]; - // *pv_ca_succ_E *= (*pv_ca_succ)[i]; - // - // base_index += 2; - // } - // - // // - // // We need to extend the quantification to the states of the - // // context automaton, because they constitute the control part - // // of the system. - // // - // // *pv_E *= *pv_ca_E; - // // *pv_succ_E *= *pv_ca_succ_E; - // } + } - for (unsigned int i = 0; i < totalActions; ++i) + // Actions/Contexts + pv_act = new vector(totalActions); + pv_act_E = new BDD(BDD_TRUE); + + for (unsigned int i = 0; i < totalActions; ++i) { - (*pv_act)[i] = cuddMgr->bddVar(offset+i); + (*pv_act)[i] = cuddMgr->bddVar(bdd_var_idx++); *pv_act_E *= (*pv_act)[i]; } - + + // Quantification BDDs + + *pv_E = *pv_rs_E; + *pv_succ_E = *pv_rs_succ_E; + + if (usingContextAutomaton()) + { + *pv_E *= *pv_ca_E; + *pv_succ_E *= *pv_ca_succ_E; + } VERB("All BDD variables ready"); } @@ -291,7 +280,7 @@ void SymRS::encodeTransitions(void) if (opts->part_tr_rel) { VERB("Using partitioned transition relation encoding"); - partTrans = new vector(totalStateVars); + partTrans = new vector(totalRctSysStateVars); } else { @@ -299,7 +288,7 @@ void SymRS::encodeTransitions(void) monoTrans = new BDD(BDD_TRUE); } - for (unsigned int p = 0; p < totalStateVars; ++p) + for (unsigned int p = 0; p < totalRctSysStateVars; ++p) { VERB_L3("Encoding for successor " << p); @@ -407,7 +396,7 @@ void SymRS::encodeInitStatesForCtxAut(void) { initStates = new BDD(BDD_TRUE); - for (unsigned int i = 0; i < totalStateVars; ++i) + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { *initStates *= !(*pv)[i]; } @@ -454,7 +443,7 @@ void SymRS::mapStateToAct(void) { VERB("Mapping state variables to action variables"); unsigned int j = 0; - for (unsigned int i = 0; i < totalStateVars; ++i) + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { if (rs->isActionEntity(i)) { stateToAct.push_back(j++); @@ -572,8 +561,6 @@ BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const r *= !(*enc_vec)[i]; } - cout << "STATE:" << endl; - BDD_PRINT(r); return r; } @@ -607,12 +594,7 @@ void SymRS::encodeCtxAutTrans(void) BDD enc_ctx = compContext(encActEntitiesConj(t.ctx)); *tr_ca += enc_src * enc_ctx * enc_dst; - // cout << "tr_ca:" << endl; - // BDD_PRINT(*tr_ca); } - - // cout << "tr_ca:" << endl; - // BDD_PRINT(*tr_ca); } /** EOF **/ diff --git a/symrs.hh b/symrs.hh index 9bdc8ef..376c559 100644 --- a/symrs.hh +++ b/symrs.hh @@ -42,14 +42,15 @@ class SymRS BDD *initStates; vector *pv; - vector *pv_act; vector *pv_succ; - - // BDDs for quantification BDD *pv_E; - BDD *pv_act_E; BDD *pv_succ_E; + vector *pv_rs; + vector *pv_rs_succ; + BDD *pv_rs_E; + BDD *pv_rs_succ_E; + vector *partTrans; BDD *monoTrans; @@ -61,8 +62,12 @@ class SymRS BDD *pv_ca_succ_E; BDD *tr_ca; - unsigned int totalReactions; + vector *pv_act; + BDD *pv_act_E; + unsigned int totalStateVars; + unsigned int totalReactions; + unsigned int totalRctSysStateVars; unsigned int totalActions; unsigned int totalCtxAutStateVars; @@ -105,8 +110,8 @@ class SymRS BDD compContext(const BDD &context) const; - std::string decodedStateToStr(const BDD &state); - void printDecodedStates(const BDD &states); + std::string decodedRctSysStateToStr(const BDD &state); + void printDecodedRctSysStates(const BDD &states); BDD encNoContext(void); @@ -121,7 +126,7 @@ class SymRS int getMappedStateToActID(int stateID) const { - assert(stateID < static_cast(totalStateVars)); + assert(stateID < static_cast(totalRctSysStateVars)); return stateToAct[stateID]; } @@ -141,6 +146,7 @@ public: BDD *getEncInitStates(void) { return initStates; } Cudd *getCuddMgr(void) { return cuddMgr; } unsigned int getTotalStateVars(void) { return totalStateVars; } + unsigned int getTotalRctSysStateVars(void) { return totalRctSysStateVars; } BDD encEntity(std::string name) const { return encEntity(rs->getEntityID(name)); } @@ -198,9 +204,23 @@ public: */ vector *getEncCtxAutPVsucc(void) { return pv_ca_succ; } - /** - * @brief Encodes the monolithic transition relation - */ + /** + * @brief Getter for context automaton's quantification BDD (for non-primed vars) + * + * @return Returns a BDD for quantification + */ + BDD *getEncCtxAutPV_E(void) { return pv_ca_E; } + + /** + * @brief Getter for context automaton's quantification BDD (for primed vars) + * + * @return Returns a BDD for quantification + */ + BDD *getEncCtxAutPVsucc_E(void) { return pv_ca_succ_E; } + + /** + * @brief Encodes the monolithic transition relation + */ void encodeCtxAutTrans(void); /**