From a74bc58a0c9db08489ccea4907d5c0baad87fabc Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 1 Apr 2018 20:59:10 +0100 Subject: [PATCH] Initialisation of BDD variables --- Makefile | 2 +- rs.hh | 5 + symrs.cc | 282 ++++++++++++++++++++++++++++++++++++++----------------- symrs.hh | 60 +++++++----- types.hh | 3 + 5 files changed, 240 insertions(+), 112 deletions(-) diff --git a/Makefile b/Makefile index 2540cf9..2491bc7 100644 --- a/Makefile +++ b/Makefile @@ -44,7 +44,7 @@ rsin_parser.lex.cc: rsin_parser.ll mv lex.yy.c rsin_parser.lex.cc style: - astyle --max-code-length=78 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh + astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh commit: style git commit -a diff --git a/rs.hh b/rs.hh index 0247a24..233969f 100644 --- a/rs.hh +++ b/rs.hh @@ -103,6 +103,11 @@ class RctSys return ctx_aut != nullptr; } + size_t getNumberOfProcesses(void) + { + return processes_ids.size(); + } + private: Reactions reactions; // TODO: to be removed later ReactionsForProc proc_reactions; diff --git a/symrs.cc b/symrs.cc index 98d51d5..c309fae 100644 --- a/symrs.cc +++ b/symrs.cc @@ -10,13 +10,19 @@ SymRS::SymRS(RctSys *rs, Options *opts) { this->rs = rs; this->opts = opts; - totalRctSysStateVars = rs->getEntitiesSize(); + + mapProcEntities(); + + // TODO: remove + totalActions = 0; + + totalRctSysStateVars = getTotalProductVariables(); totalReactions = rs->getReactionsSize(); - totalActions = rs->getActionsSize(); + totalCtxEntities = getTotalCtxEntitiesVariables(); totalCtxAutStateVars = getCtxAutStateEncodingSize(); - totalStateVars = totalRctSysStateVars + totalCtxAutStateVars; + numberOfProc = rs->getNumberOfProcesses(); partTrans = nullptr; monoTrans = nullptr; @@ -39,8 +45,6 @@ void SymRS::encode(void) mapStateToAct(); - mapProcEntities(); - initBDDvars(); if (usingContextAutomaton()) { @@ -78,6 +82,188 @@ LocalIndicesForProcEntities SymRS::buildLocalEntitiesMap( return ent_map; } +void SymRS::initBDDvars(void) +{ + VERB("Initialising CUDD"); + + cuddMgr = new Cudd(0, 0); + + VERB("Preparing BDD variables"); + + // used for bddVar + unsigned int bdd_var_idx = 0; + + // used for pv, pv_succ + unsigned int global_state_idx = 0; + + // ---------------------------------------------------------- + // Global state + // ---------------------------------------------------------- + // + // Variables for reaction system with CA (if used) + // + + pv = new BDDvec(totalStateVars); + pv_succ = new BDDvec(totalStateVars); + pv_E = new BDD(BDD_TRUE); + pv_succ_E = new BDD(BDD_TRUE); + + // ---------------------------------------------------------- + // Distributed RS + // ---------------------------------------------------------- + + // // Reaction system (no actions, no CA) + // pv_rs = new BDDvec(totalRctSysStateVars); + // pv_rs_succ = new BDDvec(totalRctSysStateVars); + // pv_rs_E = new BDD(BDD_TRUE); + // pv_rs_succ_E = new BDD(BDD_TRUE); + + pv_drs = new vector(numberOfProc); + pv_drs_succ = new vector(numberOfProc); + + pv_drs_flat = new BDDvec(totalRctSysStateVars); + pv_drs_flat_succ = new BDDvec(totalRctSysStateVars); + + pv_drs_flat_E = new BDD(BDD_TRUE); + pv_drs_flat_succ_E = new BDD(BDD_TRUE); + + VERB_LN(3, "DRS processing"); + + unsigned int drs_flat_index = 0; + + for (const auto &proc_ent : usedProducts) { + + auto proc_id = proc_ent.first; + auto entities_count = proc_ent.second.size(); + + // + // The order of entities and their correspondence to the + // correct entities in pv (global) does not matter here. + // + // The correspondence is established in the methods + // returning BDD variables (encoding) of the individual + // enties. + // + // We only need to make sure we have the correct number of + // variables that are going to be used in the encoding. + // + // For efficiency, we do not introduce BDD variables for + // entites that are never produced in a given local component. + // Instead, we only select those that are. We apply the same + // strategy to product entities and context entities. + // + + // First, we need to adjust the sizes of all the nested vectors + (*pv_drs)[proc_id].resize(entities_count); + (*pv_drs_succ)[proc_id].resize(entities_count); + + for (unsigned int i = 0; i < entities_count; ++i) { + + assert(drs_flat_index < totalRctSysStateVars); + assert(global_state_idx < totalStateVars); + assert(proc_id < numberOfProc); + assert(i < rs->getEntitiesSize()); + + // Variables for each individual process/component + (*pv_drs)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++); + (*pv_drs_succ)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++); + + // The DRS part of the system (flattened): these vars do not include CA + (*pv_drs_flat)[drs_flat_index] = (*pv_drs)[proc_id][i]; + (*pv_drs_flat_succ)[drs_flat_index] = (*pv_drs_succ)[proc_id][i]; + ++drs_flat_index; + + // Variables used for the global states + (*pv)[global_state_idx] = (*pv_drs)[proc_id][i]; + (*pv_succ)[global_state_idx] = (*pv_drs_succ)[proc_id][i]; + ++global_state_idx; + } + } + + // ---------------------------------------------------------- + // Context Automaton + // ---------------------------------------------------------- + + if (usingContextAutomaton()) { + VERB("Context automaton variables"); + + pv_ca = new BDDvec(totalCtxAutStateVars); + pv_ca_succ = new BDDvec(totalCtxAutStateVars); + pv_ca_E = new BDD(BDD_TRUE); + pv_ca_succ_E = new BDD(BDD_TRUE); + + for (unsigned int i = 0; i < totalCtxAutStateVars; ++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)[global_state_idx] = (*pv_ca)[i]; + (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i]; + ++global_state_idx; + } + } + + // ---------------------------------------------------------- + // Enabledness of processes + // ---------------------------------------------------------- + // + // These variables indicate which process is + // allowed to perform action + // + pv_proc_enab = new BDDvec(numberOfProc); + + for (unsigned int i = 0; i < numberOfProc; ++i) { + (*pv_proc_enab)[i] = cuddMgr->bddVar(bdd_var_idx++); + } + + // 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]; + } + + // 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"); +} + +size_t SymRS::getTotalProductVariables(void) +{ + size_t total = 0; + + for (const auto &it : usedProducts) { + total += it.second.size(); + } + + return total; +} + +size_t SymRS::getTotalCtxEntitiesVariables(void) +{ + size_t total = 0; + + for (const auto &it : usedCtxEntities) { + total += it.second.size(); + } + + return total; +} + void SymRS::mapProcEntities(void) { // @@ -256,7 +442,7 @@ void SymRS::printDecodedRctSysStates(const BDD &states) cout << decodedRctSysStateToStr(t) << endl; if (opts->verbose > 9) { - t.PrintMinterm(); + BDD_PRINT(t); cout << endl; } @@ -264,86 +450,6 @@ void SymRS::printDecodedRctSysStates(const BDD &states) } } -void SymRS::initBDDvars(void) -{ - VERB("Initialising CUDD"); - - cuddMgr = new Cudd(0, 0); - - VERB("Preparing BDD variables"); - - // used for bddVar - unsigned int bdd_var_idx = 0; - - // 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); - - // 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"); - - 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); - - for (unsigned int i = 0; i < totalCtxAutStateVars; ++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)[global_state_idx] = (*pv_ca)[i]; - (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i]; - ++global_state_idx; - } - } - - // 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(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"); -} - void SymRS::encodeTransitions(void) { DecompReactions dr; @@ -365,7 +471,7 @@ void SymRS::encodeTransitions(void) if (opts->part_tr_rel) { VERB("Using partitioned transition relation encoding"); - partTrans = new vector(totalRctSysStateVars); + partTrans = new BDDvec(totalRctSysStateVars); } else { VERB("Using monolithic transition relation encoding"); @@ -575,7 +681,7 @@ size_t SymRS::getCtxAutStateEncodingSize(void) BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const { // select appropriate BDD vector - vector *enc_vec; + BDDvec *enc_vec; if (succ) { enc_vec = pv_ca_succ; diff --git a/symrs.hh b/symrs.hh index 56db27e..b1385d8 100644 --- a/symrs.hh +++ b/symrs.hh @@ -35,11 +35,11 @@ class SymRS public: SymRS(RctSys *rs, Options *opts); - vector *getEncPV(void) + BDDvec *getEncPV(void) { return pv; } - vector *getEncPVsucc(void) + BDDvec *getEncPVsucc(void) { return pv_succ; } @@ -55,7 +55,7 @@ class SymRS { return pv_act_E; } - vector *getEncPartTrans(void) + BDDvec *getEncPartTrans(void) { return partTrans; } @@ -144,7 +144,7 @@ class SymRS * * @return Returns a vector of BDDs */ - vector *getEncCtxAutPV(void) + BDDvec *getEncCtxAutPV(void) { return pv_ca; } @@ -154,7 +154,7 @@ class SymRS * * @return Returns a vector of BDDs */ - vector *getEncCtxAutPVsucc(void) + BDDvec *getEncCtxAutPVsucc(void) { return pv_ca_succ; } @@ -200,48 +200,62 @@ class SymRS Cudd *cuddMgr; Options *opts; - // Mapping: entity ID -> action/context entity ID - StateEntityToAction stateToAct; + StateEntityToAction + stateToAct; /*!< Mapping: entity ID -> action/context entity ID */ - BDD *initStates; + BDD *initStates; /*!< BDD with initial states encoded */ - vector *pv; - vector *pv_succ; + BDDvec *pv; /*!< PVs for the global state (all the variables, flat) */ + BDDvec *pv_succ; BDD *pv_E; BDD *pv_succ_E; - vector *pv_rs; - vector *pv_rs_succ; + BDDvec *pv_proc_enab; /*!< Variables indicating if a process is enabled */ + + BDDvec *pv_rs; + BDDvec *pv_rs_succ; + BDD *pv_rs_E; BDD *pv_rs_succ_E; - vector *partTrans; + vector *pv_drs; /*!< PVs for the product part of state + (per DRS process) */ + vector *pv_drs_succ; /*!< PVs for the product (successor) + part of state (per DRS process) */ + + BDDvec *pv_drs_flat; /*!< PVs for the DRS product part of state (flat) */ + BDDvec *pv_drs_flat_succ; /*!< PVs for the DRS product (successor) part of state (flat) */ + + BDDvec *partTrans; BDD *monoTrans; // Context automaton - vector *pv_ca; - vector *pv_ca_succ; + BDDvec *pv_ca; + BDDvec *pv_ca_succ; BDD *pv_ca_E; BDD *pv_ca_succ_E; BDD *tr_ca; - vector *pv_act; + BDDvec *pv_act; BDD *pv_act_E; + unsigned int numberOfProc; /*!< The number of DRS processes */ unsigned int totalStateVars; unsigned int totalReactions; - unsigned int totalRctSysStateVars; + 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; unsigned int totalCtxAutStateVars; - EntitiesForProc usedProducts; - EntitiesForProc usedCtxEntities; + EntitiesForProc usedProducts; /*!< Entities used in products (per process) */ + EntitiesForProc usedCtxEntities; /*!< Entities used in context sets (per process) */ - // Local indices for each entity (per process): - // separete for state/product entities and context - LocalIndicesForProcEntities prod_ent_local_idx; - LocalIndicesForProcEntities ctx_ent_local_idx; + LocalIndicesForProcEntities prod_ent_local_idx; /*!< Local indices for each entity (per process): product entities */ + LocalIndicesForProcEntities ctx_ent_local_idx; /*!< Local indices for each entity (per process): context entities */ + + size_t getTotalProductVariables(void); + size_t getTotalCtxEntitiesVariables(void); BDD encEntity_raw(Entity entity, bool succ) const; BDD encEntity(Entity entity) const diff --git a/types.hh b/types.hh index 57bea19..8cb55c8 100644 --- a/types.hh +++ b/types.hh @@ -13,6 +13,9 @@ #include #include #include +#include "cudd.hh" + +typedef std::vector BDDvec; typedef unsigned int Entity; typedef std::set Entities;