From e3119099ea3815698cad37e7160d0815305faffa Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Mon, 26 Mar 2018 19:18:41 +0100 Subject: [PATCH] Context automaton state encoding --- ctx_aut.cc | 6 +++ ctx_aut.hh | 1 + mc.cc | 13 +++-- rs.cc | 17 ++++++- rs.hh | 1 + symrs.cc | 143 ++++++++++++++++++++++++++++++++--------------------- symrs.hh | 28 ++++++++--- 7 files changed, 142 insertions(+), 67 deletions(-) diff --git a/ctx_aut.cc b/ctx_aut.cc index 38030dd..8a3c5bb 100644 --- a/ctx_aut.cc +++ b/ctx_aut.cc @@ -57,6 +57,12 @@ void CtxAut::setInitState(std::string name) init_state_defined = true; } +State CtxAut::getInitState(void) +{ + assert(init_state_defined); + return init_state_id; +} + void CtxAut::printAutomaton(void) { showStates(); diff --git a/ctx_aut.hh b/ctx_aut.hh index 8bf03ba..766873d 100644 --- a/ctx_aut.hh +++ b/ctx_aut.hh @@ -32,6 +32,7 @@ class CtxAut bool hasState(std::string name); void addState(std::string stateName); void setInitState(std::string stateName); + State getInitState(void); State getStateID(std::string name); std::string getStateName(State state_id); void printAutomaton(void); diff --git a/mc.cc b/mc.cc index 6fd8342..51d5817 100644 --- a/mc.cc +++ b/mc.cc @@ -21,7 +21,10 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts) // // Transition relations // - // If we use trp, then trm is going to be nullptr (same for trm) + // trp -- partitioned TR + // trm -- monolithic TR + // + // If we use trp, then trm is nullptr (same for trm) // trp = srs->getEncPartTrans(); if (trp == nullptr) @@ -32,10 +35,10 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts) if (srs->usingContextAutomaton()) { - ca_init_state = srs->getEncCA_InitState(); - pv_ca = srs->getEncCA_PV(); - pv_ca_succ = srs->getEncCA_PVsucc(); - ca_tr = srs->getEncCA_Trans(); + ca_init_state = srs->getEncCtxAutInitState(); + pv_ca = srs->getEncCtxAutPV(); + pv_ca_succ = srs->getEncCtxAutPVsucc(); + ca_tr = srs->getEncCtxAutTrans(); } // Initialise the set of reachable states diff --git a/rs.cc b/rs.cc index acb04ff..9ed9d26 100644 --- a/rs.cc +++ b/rs.cc @@ -130,7 +130,6 @@ void RctSys::commitInitState(void) tmpState.clear(); } - void RctSys::addActionEntity(std::string entityName) { if (!hasEntity(entityName)) @@ -138,6 +137,12 @@ void RctSys::addActionEntity(std::string entityName) actionEntities.insert(getEntityID(entityName)); } +void RctSys::addActionEntity(Entity entity) +{ + if (!isActionEntity(entity)) + actionEntities.insert(entity); +} + bool RctSys::isActionEntity(Entity entity) { if (actionEntities.count(entity) > 0) @@ -211,7 +216,17 @@ void RctSys::ctxAutAddTransition(std::string srcStateName, std::string dstStateN void RctSys::ctxAutPushNamedContextEntity(std::string entityName) { assert(ctx_aut != nullptr); + Entity entity_id = getEntityID(entityName); + + // + // We mark the entity as an action entity + // + // This step is required to ensure the minimal number of + // BDD variables used in the encoding of the context sets + // + addActionEntity(entity_id); + ctx_aut->pushContextEntity(entity_id); } diff --git a/rs.hh b/rs.hh index 21df20d..00bf7fa 100644 --- a/rs.hh +++ b/rs.hh @@ -52,6 +52,7 @@ class RctSys void pushStateEntity(std::string entityName); void commitInitState(void); void addActionEntity(std::string entityName); + void addActionEntity(Entity entity); bool isActionEntity(Entity entity); void resetInitStates(void) { initStates.clear(); diff --git a/symrs.cc b/symrs.cc index a8f6d98..9ce38da 100644 --- a/symrs.cc +++ b/symrs.cc @@ -51,9 +51,12 @@ BDD SymRS::encStateActEntitiesConj(const Entities &entities) { BDD state_act = encEntity(*entity); int actEntity; + + // if entity is also an aciton entity, we include it in the encoding if ((actEntity = getMappedStateToActID(*entity)) >= 0) state_act += encActEntity(actEntity); - r *= state_act; + + r *= state_act; } return r; @@ -67,8 +70,11 @@ BDD SymRS::encStateActEntitiesDisj(const Entities &entities) { BDD state_act = encEntity(*entity); int actEntity; + + // if entity is also an aciton entity, we include it in the encoding if ((actEntity = getMappedStateToActID(*entity)) >= 0) state_act += encActEntity(actEntity); + r += state_act; } @@ -132,40 +138,61 @@ void SymRS::printDecodedStates(const BDD &states) void SymRS::initBDDvars(void) { + VERB("Initialising CUDD"); + cuddMgr = new Cudd(0,0); - //RctSys::Entities aa = rs->actionEntities; - VERB("Preparing BDD variables"); + pv = new vector(totalStateVars); pv_succ = new vector(totalStateVars); pv_act = new vector(totalActions); - pv_E = new BDD(cuddMgr->bddOne()); - pv_succ_E = new BDD(cuddMgr->bddOne()); - pv_act_E = new BDD(cuddMgr->bddOne()); + pv_E = new BDD(BDD_TRUE); + pv_succ_E = new BDD(BDD_TRUE); + pv_act_E = new BDD(BDD_TRUE); - //unsigned int j = 0; for (unsigned int i = 0; i < totalStateVars; ++i) { (*pv)[i] = cuddMgr->bddVar(i*2); (*pv_succ)[i] = cuddMgr->bddVar((i*2)+1); - //(*pv_act)[i] = cuddMgr->bddVar(totalStateVars*2+i); *pv_E *= (*pv)[i]; *pv_succ_E *= (*pv_succ)[i]; - - //if (rs->actionEntities.find(i) == rs->actionEntities.end()) - // (*pv_noact)[j++] = cuddMgr->bddVar(i*2); } unsigned int offset = totalStateVars * 2; + for (unsigned int i = 0; i < totalActions; ++i) { (*pv_act)[i] = cuddMgr->bddVar(offset+i); *pv_act_E *= (*pv_act)[i]; } - VERB("Variables ready"); + offset += totalActions; + + 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; + } + + VERB("All BDD variables ready"); } void SymRS::encodeTransitions(void) @@ -246,43 +273,6 @@ void SymRS::encodeTransitions(void) } - /* - for (unsigned int p = 0; p < totalStateVars; ++p) // we iterate through products - { - RctSys::Entities::iterator ai = rs->actionEntities.find(p); - DecompReactions::iterator di; - - if ((di = dr.find(p)) == dr.end()) - { - (*partTrans)[p] = cuddMgr->bddOne(); - if (ai == rs->actionEntities.end()) - (*partTrans)[p] *= !encEntitySucc(p); - } - else - { - BDD conditions = cuddMgr->bddZero(); - - for (unsigned int j = 0; j < di->second.size(); ++j) - { - conditions += encEntitiesConj(di->second[j].rctt) * !encEntitiesDisj(di->second[j].inhib); - } - - (*partTrans)[p] = conditions * encEntitySucc(p); - - if (ai == rs->actionEntities.end()) - { - // not an action entity - (*partTrans)[p] += !conditions * !encEntitySucc(p); - } - else - { - // action entity - (*partTrans)[p] += cuddMgr->bddOne(); //(encEntitySucc(p) + !encEntitySucc(p)); - } - } - } - */ - VERB("Reactions ready"); } @@ -362,11 +352,12 @@ void SymRS::mapStateToAct(void) stateToAct.push_back(-1); } } - if (opts->verbose > 9) + const unsigned int verbosity_level = 9; + if (opts->verbose > verbosity_level) { for (unsigned int i = 0; i < stateToAct.size(); ++i) { - cout << "ii VERBOSE(9): stateToAct[" << i << "] = " << stateToAct[i] << endl; + cout << "ii VERBOSE(" << verbosity_level << "): stateToAct[" << i << "] = " << stateToAct[i] << endl; } } } @@ -408,22 +399,64 @@ BDD SymRS::encActStrEntity(std::string name) const } } -BDD *SymRS::getEncCA_InitState(void) +size_t SymRS::getCtxAutStateEncodingSize(void) +{ + size_t bitCount = 0; + size_t bitCountMaxVal = 1; + size_t numStates = rs->ctx_aut->statesCount(); + while (bitCountMaxVal <= numStates) + { + bitCount++; + bitCountMaxVal *= 2; + } + return bitCount; +} + +BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const +{ + // select appropriate BDD vector + vector *enc_vec; + if (succ) + enc_vec = pv_ca_succ; + else + enc_vec = pv_ca; + + BDD r; + State val = state_id; + + for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) + { + if (val != 0) + { + if (val % 2 == 1) + r *= (*enc_vec)[i]; + else + r *= !(*enc_vec)[i]; + val /= 2; + } + else + r *= !(*enc_vec)[i]; + } + + return r; +} + +BDD *SymRS::getEncCtxAutInitState(void) { return new BDD(BDD_TRUE); } -vector *SymRS::getEncCA_PV(void) +vector *SymRS::getEncCtxAutPV(void) { return new vector(); } -vector *SymRS::getEncCA_PVsucc(void) +vector *SymRS::getEncCtxAutPVsucc(void) { return new vector(); } -BDD *SymRS::getEncCA_Trans(void) +BDD *SymRS::getEncCtxAutTrans(void) { return new BDD(BDD_TRUE); } diff --git a/symrs.hh b/symrs.hh index 9f807ec..cc846c8 100644 --- a/symrs.hh +++ b/symrs.hh @@ -36,24 +36,35 @@ class SymRS Cudd *cuddMgr; Options *opts; + // Mapping: entity ID -> action/context entity ID StateEntityToAction stateToAct; 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_noact; vector *partTrans; BDD *monoTrans; + // Context automaton + vector *pv_ca; + vector *pv_ca_succ; + BDD *pv_ca_E; + BDD *pv_ca_succ_E; + unsigned int totalReactions; unsigned int totalStateVars; unsigned int totalActions; + unsigned int totalCtxAutStateVars; + BDD encEntity_raw(Entity entity, bool succ) const; BDD encEntity(Entity entity) const { @@ -106,6 +117,8 @@ class SymRS int getMappedStateToActID(int stateID) const { assert(stateID < static_cast(totalStateVars)); return stateToAct[stateID]; } + size_t getCtxAutStateEncodingSize(void); + public: SymRS(RctSys *rs, Options *opts) { @@ -114,6 +127,7 @@ public: totalStateVars = rs->getEntitiesSize(); totalReactions = rs->getReactionsSize(); totalActions = rs->getActionsSize(); + totalCtxAutStateVars = getCtxAutStateEncodingSize(); partTrans = nullptr; monoTrans = nullptr; @@ -140,11 +154,13 @@ public: bool usingContextAutomaton(void) { return rs->ctx_aut != nullptr; } - BDD *getEncCA_InitState(void); - vector *getEncCA_PV(void); - vector *getEncCA_PVsucc(void); - BDD *getEncCA_Trans(void); - + BDD encCtxAutState_raw(State state_id, bool succ) const; + BDD encCtxAutState(State state_id) const { return encCtxAutState_raw(state_id, false); } + BDD encCtxAutStateSucc(State state_id) const { return encCtxAutState_raw(state_id, true); } + BDD *getEncCtxAutInitState(void); + vector *getEncCtxAutPV(void); + vector *getEncCtxAutPVsucc(void); + BDD *getEncCtxAutTrans(void); }; #endif