From e3ed26e4a1d77d181749b08f7c72ceb917cc0fdc Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 30 Mar 2018 17:51:29 +0100 Subject: [PATCH] Entities used per process (in reactions) --- macro.hh | 3 + symrs.cc | 102 +++++++++++++++++-------- symrs.hh | 223 +++++++++++++++++++++++++++++-------------------------- 3 files changed, 190 insertions(+), 138 deletions(-) diff --git a/macro.hh b/macro.hh index 27934c8..1e86fac 100644 --- a/macro.hh +++ b/macro.hh @@ -39,4 +39,7 @@ if (opts->verbose >= (n)) { \ std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ } + +#define SET_ADD(set1, set2) (set1).insert((set2).begin(), (set2).end()) + #endif diff --git a/symrs.cc b/symrs.cc index c64e0e1..3044b3a 100644 --- a/symrs.cc +++ b/symrs.cc @@ -28,6 +28,77 @@ SymRS::SymRS(RctSys *rs, Options *opts) encode(); } +void SymRS::encode(void) +{ + VERB("Encoding..."); + + if (opts->measure) { + opts->enc_time = cpuTime(); + opts->enc_mem = memUsed(); + } + + mapStateToAct(); + + mapProcEntities(); + + initBDDvars(); + + if (usingContextAutomaton()) { + encodeCtxAutTrans(); + } + else { + VERB_LN(3, "Not using context automata, not encoding TR for CA") + } + + encodeTransitions(); + encodeInitStates(); + + if (opts->measure) { + opts->enc_time = cpuTime() - opts->enc_time; + opts->enc_mem = memUsed() - opts->enc_mem; + } + + VERB("Encoding done"); +} + +void SymRS::mapProcEntities(void) +{ + + // Reactions + + for (const auto &proc_rcts : rs->proc_reactions) { + Process proc_id = proc_rcts.first; + + for (const auto &rct : proc_rcts.second) { + + // collect entities that can be produced + // locally by the process with proc_id + + SET_ADD(usedEntities[proc_id], rct.prod); + } + } + + // Context automaton + // for () + + printUsedEntitiesPerProc(); + +} + +void SymRS::printUsedEntitiesPerProc(void) +{ + for (const auto &proc_entities : usedEntities) { + std::string proc_name = rs->getProcessName(proc_entities.first); + cout << proc_name << ": "; + + for (const auto &ent : proc_entities.second) { + cout << rs->getEntityName(ent) << " "; + } + + cout << endl; + } +} + BDD SymRS::encEntity_raw(Entity entity, bool succ) const { BDD r; @@ -455,37 +526,6 @@ void SymRS::mapStateToAct(void) } } -void SymRS::encode(void) -{ - VERB("Encoding..."); - - if (opts->measure) { - opts->enc_time = cpuTime(); - opts->enc_mem = memUsed(); - } - - mapStateToAct(); - - initBDDvars(); - - if (usingContextAutomaton()) { - encodeCtxAutTrans(); - } - else { - VERB_LN(3, "Not using context automata, not encoding TR for CA") - } - - encodeTransitions(); - encodeInitStates(); - - if (opts->measure) { - opts->enc_time = cpuTime() - opts->enc_time; - opts->enc_mem = memUsed() - opts->enc_mem; - } - - VERB("Encoding done"); -} - BDD SymRS::encActStrEntity(std::string name) const { int id = getMappedStateToActID(rs->getEntityID(name)); diff --git a/symrs.hh b/symrs.hh index 060b819..63d6fd1 100644 --- a/symrs.hh +++ b/symrs.hh @@ -32,113 +32,6 @@ class SymRS friend class ModelChecker; friend class FormRSCTL; - RctSys *rs; - Cudd *cuddMgr; - Options *opts; - - // Mapping: entity ID -> action/context entity ID - StateEntityToAction stateToAct; - - BDD *initStates; - - vector *pv; - vector *pv_succ; - BDD *pv_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; - - // Context automaton - vector *pv_ca; - vector *pv_ca_succ; - BDD *pv_ca_E; - BDD *pv_ca_succ_E; - BDD *tr_ca; - - vector *pv_act; - BDD *pv_act_E; - - unsigned int totalStateVars; - unsigned int totalReactions; - unsigned int totalRctSysStateVars; - unsigned int totalActions; - unsigned int totalCtxAutStateVars; - - BDD encEntity_raw(Entity entity, bool succ) const; - BDD encEntity(Entity entity) const - { - return encEntity_raw(entity, false); - } - BDD encActEntity(Entity entity) const - { - assert(entity < pv_act->size()); - return (*pv_act)[entity]; - } - BDD encEntitySucc(Entity entity) const - { - return encEntity_raw(entity, true); - } - BDD encEntitiesConj_raw(const Entities &entities, bool succ); - BDD encEntitiesConj(const Entities &entities) - { - return encEntitiesConj_raw(entities, false); - } - BDD encEntitiesConjSucc(const Entities &entities) - { - return encEntitiesConj_raw(entities, true); - } - BDD encEntitiesDisj_raw(const Entities &entities, bool succ); - BDD encEntitiesDisj(const Entities &entities) - { - return encEntitiesDisj_raw(entities, false); - } - BDD encEntitiesDisjSucc(const Entities &entities) - { - return encEntitiesDisj_raw(entities, true); - } - BDD encStateActEntitiesConj(const Entities &entities); - BDD encStateActEntitiesDisj(const Entities &entities); - - BDD encActEntitiesConj(const Entities &entities); - - /** - * @brief Complements an encoding of a given state by negating all the variables that are not set to true - * - * @return Returns the encoded state - */ - BDD compState(const BDD &state) const; - - BDD compContext(const BDD &context) const; - - std::string decodedRctSysStateToStr(const BDD &state); - void printDecodedRctSysStates(const BDD &states); - - BDD encNoContext(void); - - void initBDDvars(void); - void encodeTransitions(void); - void encodeTransitions_old(void); - void encodeInitStates(void); - void encodeInitStatesForCtxAut(void); - void encodeInitStatesNoCtxAut(void); - void mapStateToAct(void); - void encode(void); - - int getMappedStateToActID(int stateID) const - { - assert(stateID < static_cast(totalRctSysStateVars)); - return stateToAct[stateID]; - } - - size_t getCtxAutStateEncodingSize(void); - public: SymRS(RctSys *rs, Options *opts); @@ -300,6 +193,122 @@ class SymRS { return tr_ca; } + + private: + + RctSys *rs; + Cudd *cuddMgr; + Options *opts; + + // Mapping: entity ID -> action/context entity ID + StateEntityToAction stateToAct; + + BDD *initStates; + + vector *pv; + vector *pv_succ; + BDD *pv_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; + + // Context automaton + vector *pv_ca; + vector *pv_ca_succ; + BDD *pv_ca_E; + BDD *pv_ca_succ_E; + BDD *tr_ca; + + vector *pv_act; + BDD *pv_act_E; + + unsigned int totalStateVars; + unsigned int totalReactions; + unsigned int totalRctSysStateVars; + unsigned int totalActions; + unsigned int totalCtxAutStateVars; + + EntitiesForProc usedEntities; + + BDD encEntity_raw(Entity entity, bool succ) const; + BDD encEntity(Entity entity) const + { + return encEntity_raw(entity, false); + } + BDD encActEntity(Entity entity) const + { + assert(entity < pv_act->size()); + return (*pv_act)[entity]; + } + BDD encEntitySucc(Entity entity) const + { + return encEntity_raw(entity, true); + } + BDD encEntitiesConj_raw(const Entities &entities, bool succ); + BDD encEntitiesConj(const Entities &entities) + { + return encEntitiesConj_raw(entities, false); + } + BDD encEntitiesConjSucc(const Entities &entities) + { + return encEntitiesConj_raw(entities, true); + } + BDD encEntitiesDisj_raw(const Entities &entities, bool succ); + BDD encEntitiesDisj(const Entities &entities) + { + return encEntitiesDisj_raw(entities, false); + } + BDD encEntitiesDisjSucc(const Entities &entities) + { + return encEntitiesDisj_raw(entities, true); + } + BDD encStateActEntitiesConj(const Entities &entities); + BDD encStateActEntitiesDisj(const Entities &entities); + + BDD encActEntitiesConj(const Entities &entities); + + /** + * @brief Complements an encoding of a given state by negating all the variables that are not set to true + * + * @return Returns the encoded state + */ + BDD compState(const BDD &state) const; + + BDD compContext(const BDD &context) const; + + std::string decodedRctSysStateToStr(const BDD &state); + void printDecodedRctSysStates(const BDD &states); + + BDD encNoContext(void); + + void initBDDvars(void); + void encodeTransitions(void); + void encodeTransitions_old(void); + void encodeInitStates(void); + void encodeInitStatesForCtxAut(void); + void encodeInitStatesNoCtxAut(void); + void mapStateToAct(void); + void mapProcEntities(void); + void encode(void); + + void printUsedEntitiesPerProc(void); + + int getMappedStateToActID(int stateID) const + { + assert(stateID < static_cast(totalRctSysStateVars)); + return stateToAct[stateID]; + } + + size_t getCtxAutStateEncodingSize(void); + + }; #endif