From 9a8255a355f57c2b3748884226c6f7627547df9c Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Mon, 2 Apr 2018 22:17:47 +0100 Subject: [PATCH] Encoding DRS transition relation --- formrsctl.cc | 4 +- formrsctl.hh | 5 +- mc.cc | 4 +- rs.hh | 6 +- symrs.cc | 239 +++++++++++++++------------------------------------ symrs.hh | 60 +++++++------ 6 files changed, 113 insertions(+), 205 deletions(-) diff --git a/formrsctl.cc b/formrsctl.cc index 8f465e0..2b97e25 100644 --- a/formrsctl.cc +++ b/formrsctl.cc @@ -76,7 +76,7 @@ BDD BoolContexts::getBDD(const SymRS *srs) const std::string FormRSCTL::toStr(void) const { if (oper == RSCTL_PV) { - return name; + return proc_name + ":" + entity_name; } else if (oper == RSCTL_TF) { if (tf) { @@ -188,7 +188,7 @@ void FormRSCTL::encodeEntities(const SymRS *srs) arg[1]->encodeEntities(srs); } else if (oper == RSCTL_PV) { - bdd = new BDD(srs->encEntity(name)); + bdd = new BDD(srs->encEntity(proc_name, entity_name)); } } diff --git a/formrsctl.hh b/formrsctl.hh index 14990e7..baddbde 100644 --- a/formrsctl.hh +++ b/formrsctl.hh @@ -153,7 +153,8 @@ class FormRSCTL { Oper oper; FormRSCTL *arg[2]; - std::string name; + std::string entity_name; + std::string proc_name; bool tf; BDD *bdd; ActionsVec_f *actions; @@ -169,7 +170,7 @@ class FormRSCTL FormRSCTL(std::string varName) { oper = RSCTL_PV; - name = varName; + entity_name = varName; arg[0] = nullptr; arg[1] = nullptr; bdd = nullptr; diff --git a/mc.cc b/mc.cc index 80b5f2c..00e56c4 100644 --- a/mc.cc +++ b/mc.cc @@ -191,7 +191,9 @@ bool ModelChecker::checkReach(const Entities testState) opts->ver_time = cpuTime(); } - BDD st = srs->getEncState(testState); + // BDD st = srs->getEncState(testState); + BDD st = BDD_FALSE; + assert(0); BDD reach = *initStates; BDD reach_p = cuddMgr->bddZero(); diff --git a/rs.hh b/rs.hh index 233969f..7409336 100644 --- a/rs.hh +++ b/rs.hh @@ -75,10 +75,6 @@ class RctSys { return entities_ids.size(); } - unsigned int getReactionsSize(void) - { - return reactions.size(); - } unsigned int getActionsSize(void) { return actionEntities.size(); @@ -109,7 +105,7 @@ class RctSys } private: - Reactions reactions; // TODO: to be removed later + // Reactions reactions; // TODO: to be removed later ReactionsForProc proc_reactions; EntitiesSets initStates; diff --git a/symrs.cc b/symrs.cc index 08c5429..c81ed72 100644 --- a/symrs.cc +++ b/symrs.cc @@ -13,11 +13,12 @@ SymRS::SymRS(RctSys *rs, Options *opts) mapProcEntities(); + totalEntities = rs->getEntitiesSize(); + // TODO: remove totalActions = 0; totalRctSysStateVars = getTotalProductVariables(); - totalReactions = rs->getReactionsSize(); totalCtxEntities = getTotalCtxEntitiesVariables(); totalCtxAutStateVars = getCtxAutStateEncodingSize(); @@ -43,8 +44,6 @@ void SymRS::encode(void) opts->enc_mem = memUsed(); } - mapStateToAct(); - initBDDvars(); if (usingContextAutomaton()) { @@ -156,7 +155,7 @@ void SymRS::initBDDvars(void) assert(drs_flat_index < totalRctSysStateVars); assert(global_state_idx < totalStateVars); assert(proc_id < numberOfProc); - assert(i < rs->getEntitiesSize()); + assert(i < totalEntities); // Variables for each individual process/component (*pv_drs)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++); @@ -250,7 +249,7 @@ void SymRS::initBDDvars(void) auto proc_id = proc_ent.first; auto entities_count = proc_ent.second.size(); - assert(entities_count < rs->getEntitiesSize()); + assert(entities_count < totalEntities); // adjust the size of the nested vector before we use an index (*pv_proc_ctx)[proc_id].resize(entities_count); @@ -346,46 +345,60 @@ void SymRS::mapProcEntities(void) } } -BDD SymRS::encEntity_raw(Entity entity, bool succ) const +BDD SymRS::encEntity_raw(Process proc_id, Entity entity, bool succ) const { BDD r; + assert(proc_id < numberOfProc); + + auto local_entity_id = getLocalProductEntityIndex(proc_id, entity); + if (succ) { - r = (*pv_succ)[entity]; + r = (*pv_drs_succ)[proc_id][local_entity_id]; } else { - r = (*pv)[entity]; + r = (*pv_drs)[proc_id][local_entity_id]; } return r; } -BDD SymRS::encEntitiesConj_raw(const Entities &entities, bool succ) +BDD SymRS::encCtxEntity(Process proc_id, Entity entity) const +{ + assert(entity < totalEntities); + assert(proc_id < numberOfProc); + + auto local_entity_id = getLocalCtxEntityIndex(proc_id, entity); + + return (*pv_proc_ctx)[proc_id][local_entity_id]; +} + +BDD SymRS::encEntitiesConj_raw(Process proc_id, const Entities &entities, bool succ) { BDD r = BDD_TRUE; for (const auto &entity : entities) { if (succ) { - r *= encEntitySucc(entity); + r *= encEntitySucc(proc_id, entity); } else { - r *= encEntity(entity); + r *= encEntity(proc_id, entity); } } return r; } -BDD SymRS::encEntitiesDisj_raw(const Entities &entities, bool succ) +BDD SymRS::encEntitiesDisj_raw(Process proc_id, const Entities &entities, bool succ) { BDD r = BDD_FALSE; for (const auto &entity : entities) { if (succ) { - r += encEntitySucc(entity); + r += encEntitySucc(proc_id, entity); } else { - r += encEntity(entity); + r += encEntity(proc_id, entity); } } @@ -394,8 +407,9 @@ BDD SymRS::encEntitiesDisj_raw(const Entities &entities, bool succ) BDD SymRS::encStateActEntitiesConj(const Entities &entities) { + assert(0); BDD r = BDD_TRUE; - + /* for (const auto &entity : entities) { BDD state_act = encEntity(entity); int actEntity; @@ -407,14 +421,16 @@ BDD SymRS::encStateActEntitiesConj(const Entities &entities) r *= state_act; } + */ return r; } BDD SymRS::encStateActEntitiesDisj(const Entities &entities) { + assert(0); BDD r = BDD_FALSE; - + /* for (const auto &entity : entities) { BDD state_act = encEntity(entity); int actEntity; @@ -426,24 +442,26 @@ BDD SymRS::encStateActEntitiesDisj(const Entities &entities) r += state_act; } - + */ return r; } BDD SymRS::encActEntitiesConj(const Entities &entities) { + assert(0); BDD r = BDD_TRUE; - + /* for (const auto &entity : entities) { Entity actEntity = getMappedStateToActID(entity); r *= encActEntity(actEntity); } - + */ return r; } BDD SymRS::compState(const BDD &state) const { + assert(0); BDD s = state; for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { @@ -457,6 +475,7 @@ BDD SymRS::compState(const BDD &state) const BDD SymRS::compContext(const BDD &context) const { + assert(0); BDD c = context; for (unsigned int i = 0; i < totalActions; ++i) { @@ -470,20 +489,22 @@ 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) + " "; } } - + */ s += "}"; return s; } void SymRS::printDecodedRctSysStates(const BDD &states) { + assert(0); BDD unproc = states; while (!unproc.IsZero()) { @@ -499,114 +520,51 @@ void SymRS::printDecodedRctSysStates(const BDD &states) } } -void SymRS::encodeTransitions(void) +DecompReactions SymRS::getProductionConditions(Process proc_id) { DecompReactions dr; + for (const auto &rct : rs->proc_reactions[proc_id]) { + ReactionCond cond; + cond.rctt = rct.rctt; + cond.inhib = rct.inhib; + + for (const auto &prod : rct.prod) { + dr[prod].push_back(cond); + } + } + + return dr; +} + +void SymRS::encodeTransitions(void) +{ VERB("Decomposing reactions"); - for (unsigned int i = 0; i < totalReactions; ++i) { - ReactionCond cond; - cond.rctt = rs->reactions[i].rctt; - cond.inhib = rs->reactions[i].inhib; + vector prod_conds(numberOfProc); - for (Entities::iterator p = rs->reactions[i].prod.begin(); - p != rs->reactions[i].prod.end(); ++p) { - dr[*p].push_back(cond); - } + for (auto proc_id = 0; proc_id < numberOfProc; ++proc_id) { + prod_conds[proc_id] = getProductionConditions(proc_id); } VERB("Encoding reactions"); if (opts->part_tr_rel) { VERB("Using partitioned transition relation encoding"); - partTrans = new BDDvec(totalRctSysStateVars); + FERROR("Partitioned transition relation is currently not supported"); } else { VERB("Using monolithic transition relation encoding"); monoTrans = new BDD(BDD_TRUE); } - for (unsigned int p = 0; p < totalRctSysStateVars; ++p) { - VERB_L3("Encoding for successor " << p); - - DecompReactions::iterator di; - - if ((di = dr.find(p)) == dr.end()) { - // there is no reaction producing p: - if (opts->part_tr_rel) { - (*partTrans)[p] = !encEntitySucc(p); - } - else { - *monoTrans *= !encEntitySucc(p); - } - } - else { - // di - reactions producing p - - BDD conditions = BDD_FALSE; - - assert(di->second.size() > 0); - - for (unsigned int j = 0; j < di->second.size(); ++j) { - conditions += encStateActEntitiesConj(di->second[j].rctt) * - !encStateActEntitiesDisj(di->second[j].inhib); - } - - if (opts->part_tr_rel) { - (*partTrans)[p] = conditions * encEntitySucc(p); - (*partTrans)[p] += !conditions * !encEntitySucc(p); - } - else { - *monoTrans *= (conditions * encEntitySucc(p)) + (!conditions * !encEntitySucc( - p)); - } - } - - if (opts->reorder_trans) { - VERB_L2("Reordering"); - Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000); - } - - } - - VERB("Reactions ready"); - - if (usingContextAutomaton()) { - VERB("Augmenting transition relation encoding with the transition relation for context automaton"); - - if (opts->part_tr_rel) { - assert(0); - } - else { - assert(tr_ca != nullptr); - *monoTrans *= *tr_ca; - } - } - - VERB("Transition relation encoded") -} - -BDD SymRS::getEncState(const Entities &entities) -{ - assert(0); - //BDD state = compState(encEntitiesConj(rs->initState)); - //for (RctSys::Entities::iterator at = rs->actionEntities.begin(); at != rs->actionEntities.end(); ++at) - //{ - // state = state.ExistAbstract(encEntity(*at)); - //} - return BDD_FALSE; + FERROR("WORK IN PROGRESS"); } BDD SymRS::encNoContext(void) { - BDD noContextBDD = BDD_TRUE; - - for (unsigned int i = 0; i < totalActions; ++i) { - noContextBDD *= !(*pv_act)[i]; - } - - return noContextBDD; + assert(0); + return BDD_FALSE; } void SymRS::encodeInitStates(void) @@ -616,8 +574,7 @@ void SymRS::encodeInitStates(void) encodeInitStatesForCtxAut(); } else { - VERB("Encoding initial states (for the action entities method -- no CA)"); - encodeInitStatesNoCtxAut(); + FERROR("Context automaton required"); } VERB("Initial states encoded"); @@ -634,67 +591,9 @@ void SymRS::encodeInitStatesForCtxAut(void) *initStates *= getEncCtxAutInitState(); } -void SymRS::encodeInitStatesNoCtxAut(void) -{ -#ifndef NDEBUG - - if (opts->part_tr_rel) { - assert(partTrans != nullptr); - } - -#endif - - initStates = new BDD(BDD_FALSE); - - for (auto state = rs->initStates.begin(); - state != rs->initStates.end(); - ++state) { - VERB("Encoding a single inital state"); - BDD newInitState = compState(encEntitiesConj(*state)); - BDD q = BDD_TRUE; - - if (opts->part_tr_rel) { - for (unsigned int i = 0; i < partTrans->size(); ++i) { - q *= newInitState * (*partTrans)[i] * encNoContext(); - } - } - else { - q *= newInitState * *monoTrans * encNoContext(); - } - - q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv); - q = q.ExistAbstract(*pv_act_E); - - *initStates += q; - } -} - -void SymRS::mapStateToAct(void) -{ - VERB("Mapping state variables to action variables"); - unsigned int j = 0; - - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { - if (rs->isActionEntity(i)) { - stateToAct.push_back(j++); - } - else { - stateToAct.push_back(-1); - } - } - - const unsigned int verbosity_level = 9; - - if (opts->verbose > verbosity_level) { - for (unsigned int i = 0; i < stateToAct.size(); ++i) { - cout << "ii VERBOSE(" << verbosity_level << "): stateToAct[" << i << "] = " << - stateToAct[i] << endl; - } - } -} - BDD SymRS::encActStrEntity(std::string name) const { + /* int id = getMappedStateToActID(rs->getEntityID(name)); if (id < 0) { @@ -704,6 +603,8 @@ BDD SymRS::encActStrEntity(std::string name) const else { return encActEntity(getMappedStateToActID(rs->getEntityID(name))); } + */ + return BDD_FALSE; } size_t SymRS::getCtxAutStateEncodingSize(void) @@ -788,7 +689,7 @@ void SymRS::encodeCtxAutTrans(void) << " -> " << rs->ctx_aut->getStateName(t.dst_state)); BDD enc_src = encCtxAutState(t.src_state); BDD enc_dst = encCtxAutStateSucc(t.dst_state); - assert(0); // enc_ctx + // assert(0); // enc_ctx BDD enc_ctx = BDD_FALSE; //compContext(encActEntitiesConj(t.ctx)); *tr_ca += enc_src * enc_ctx * enc_dst; diff --git a/symrs.hh b/symrs.hh index 673d97b..d6a0b22 100644 --- a/symrs.hh +++ b/symrs.hh @@ -63,7 +63,6 @@ class SymRS { return monoTrans; } - BDD getEncState(const Entities &entities); BDD *getEncInitStates(void) { return initStates; @@ -80,11 +79,10 @@ class SymRS { return totalRctSysStateVars; } - BDD encEntity(std::string name) const + BDD encEntity(std::string proc_name, std::string entity_name) const { - return encEntity(rs->getEntityID(name)); + return encEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name)); } - BDD encActStrEntity(std::string name) const; BDD getBDDtrue(void) const { @@ -249,9 +247,9 @@ class SymRS BDDvec *pv_act; BDD *pv_act_E; + unsigned int totalEntities; unsigned int numberOfProc; /*!< The number of DRS processes */ unsigned int totalStateVars; - unsigned int totalReactions; unsigned int totalRctSysStateVars; /*!< Total number of different entities produced by reactions */ unsigned int totalCtxEntities; /*!< Total number of different process-context entities used */ unsigned int totalActions; @@ -266,37 +264,48 @@ class SymRS size_t getTotalProductVariables(void); size_t getTotalCtxEntitiesVariables(void); - BDD encEntity_raw(Entity entity, bool succ) const; - BDD encEntity(Entity entity) const + unsigned int getLocalProductEntityIndex(Process proc_id, Entity entity) const { - return encEntity_raw(entity, false); + return prod_ent_local_idx.at(proc_id).at(entity); } - BDD encActEntity(Entity entity) const + unsigned int getLocalCtxEntityIndex(Process proc_id, Entity entity) const { - assert(entity < pv_act->size()); - return (*pv_act)[entity]; + return ctx_ent_local_idx.at(proc_id).at(entity); } - BDD encEntitySucc(Entity entity) const + + BDD encEntity_raw(Process proc_id, Entity entity, bool succ) const; + BDD encEntity(Process proc_id, Entity entity) const { - return encEntity_raw(entity, true); + return encEntity_raw(proc_id, entity, false); } - BDD encEntitiesConj_raw(const Entities &entities, bool succ); - BDD encEntitiesConj(const Entities &entities) + BDD encEntitySucc(Process proc_id, Entity entity) const { - return encEntitiesConj_raw(entities, false); + return encEntity_raw(proc_id, entity, true); } - BDD encEntitiesConjSucc(const Entities &entities) + + BDD encCtxEntity(Process proc_id, Entity entity) const; + + BDD encEntitiesConj_raw(Process proc_id, const Entities &entities, bool succ); + BDD encEntitiesConj(Process proc_id, const Entities &entities) { - return encEntitiesConj_raw(entities, true); + return encEntitiesConj_raw(proc_id, entities, false); } - BDD encEntitiesDisj_raw(const Entities &entities, bool succ); - BDD encEntitiesDisj(const Entities &entities) + BDD encEntitiesConjSucc(Process proc_id, const Entities &entities) { - return encEntitiesDisj_raw(entities, false); + return encEntitiesConj_raw(proc_id, entities, true); } - BDD encEntitiesDisjSucc(const Entities &entities) + + + // ---- TODO below: + + BDD encEntitiesDisj_raw(Process proc_id, const Entities &entities, bool succ); + BDD encEntitiesDisj(Process proc_id, const Entities &entities) { - return encEntitiesDisj_raw(entities, true); + return encEntitiesDisj_raw(proc_id, entities, false); + } + BDD encEntitiesDisjSucc(Process proc_id, const Entities &entities) + { + return encEntitiesDisj_raw(proc_id, entities, true); } BDD encStateActEntitiesConj(const Entities &entities); BDD encStateActEntitiesDisj(const Entities &entities); @@ -317,13 +326,12 @@ class SymRS BDD encNoContext(void); + DecompReactions getProductionConditions(Process proc_id); + void initBDDvars(void); void encodeTransitions(void); - void encodeTransitions_old(void); void encodeInitStates(void); void encodeInitStatesForCtxAut(void); - void encodeInitStatesNoCtxAut(void); - void mapStateToAct(void); LocalIndicesForProcEntities buildLocalEntitiesMap(const EntitiesForProc &procEnt); void mapProcEntities(void); void encode(void);