diff --git a/bdd_macro.hh b/bdd_macro.hh index 0751d77..43136af 100644 --- a/bdd_macro.hh +++ b/bdd_macro.hh @@ -1,8 +1,12 @@ #ifndef __BDD_MACRO_HH__ #define __BDD_MACRO_HH__ -#define BDD_IFF(p,q) (!(p+q)+(p*q)) -#define BDD_TRUE (cuddMgr->bddOne()) -#define BDD_FALSE (cuddMgr->bddZero()) +#define BDD_IFF(p,q) (!(p+q)+(p*q)) +#define BDD_TRUE (cuddMgr->bddOne()) +#define BDD_FALSE (cuddMgr->bddZero()) + +#define BDD_PRINT(t) ((t).PrintMinterm()) #endif + +/** EOF **/ diff --git a/main.cc b/main.cc index 3464b6c..afc90f7 100644 --- a/main.cc +++ b/main.cc @@ -233,3 +233,4 @@ int main(int argc, char **argv) return 0; } +/** EOF **/ diff --git a/mc.cc b/mc.cc index 081daeb..c113a96 100644 --- a/mc.cc +++ b/mc.cc @@ -37,7 +37,7 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts) // ca_init_state = srs->getEncCtxAutInitState(); pv_ca = srs->getEncCtxAutPV(); pv_ca_succ = srs->getEncCtxAutPVsucc(); - ca_tr = srs->getEncCtxAutTrans(); + // ca_tr = srs->getEncCtxAutTrans(); } // Initialise the set of reachable states diff --git a/symrs.cc b/symrs.cc index a58ac66..680135c 100644 --- a/symrs.cc +++ b/symrs.cc @@ -21,6 +21,7 @@ SymRS::SymRS(RctSys *rs, Options *opts) pv_ca = nullptr; pv_ca_succ = nullptr; + tr_ca = nullptr; encode(); } @@ -176,24 +177,86 @@ void SymRS::initBDDvars(void) cuddMgr = new Cudd(0,0); VERB("Preparing BDD variables"); + + unsigned int needed_state_vars = totalStateVars; + if (usingContextAutomaton()) + needed_state_vars += totalCtxAutStateVars; - pv = new vector(totalStateVars); - pv_succ = new vector(totalStateVars); + pv = new vector(needed_state_vars); + pv_succ = new vector(needed_state_vars); pv_act = new vector(totalActions); pv_E = new BDD(BDD_TRUE); pv_succ_E = new BDD(BDD_TRUE); pv_act_E = new BDD(BDD_TRUE); - for (unsigned int i = 0; i < totalStateVars; ++i) + 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); + } + + 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) + { + 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_E *= (*pv)[i]; + *pv_ca_succ_E *= (*pv_succ)[i]; + } } - unsigned int offset = totalStateVars * 2; + // 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) { @@ -201,32 +264,6 @@ void SymRS::initBDDvars(void) *pv_act_E *= (*pv_act)[i]; } - if (usingContextAutomaton()) - { - VERB("Context automaton variables"); - - offset += totalActions; - - 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"); } @@ -310,6 +347,22 @@ void SymRS::encodeTransitions(void) } 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) @@ -434,6 +487,16 @@ void SymRS::encode(void) mapStateToAct(); initBDDvars(); + + if (usingContextAutomaton()) + { + encodeCtxAutTrans(); + } + else + { + VERB_LN(3, "Not using context automata, not encoding TR for CA") + } + encodeTransitions(); encodeInitStates(); @@ -472,6 +535,8 @@ size_t SymRS::getCtxAutStateEncodingSize(void) bitCount++; bitCountMaxVal *= 2; } + + VERB_LN(3, "Bits required for CA: " << bitCount); return bitCount; } @@ -507,6 +572,8 @@ BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const r *= !(*enc_vec)[i]; } + cout << "STATE:" << endl; + BDD_PRINT(r); return r; } @@ -519,22 +586,33 @@ BDD SymRS::getEncCtxAutInitState(void) return encCtxAutState(state); } -BDD *SymRS::getEncCtxAutTrans(void) +void SymRS::encodeCtxAutTrans(void) { VERB_LN(2, "Encoding context automaton's transition relation"); - BDD *r = new BDD(BDD_FALSE); + if (tr_ca != nullptr) + { + VERB_LN(1, "Encoding for context automaton already present, not replacing") + return; + } + + tr_ca = new BDD(BDD_FALSE); for (auto &t : rs->ctx_aut->transitions) { + VERB_LN(2, "Encoding CA transition " << rs->ctx_aut->getStateName(t.src_state) + << " -> " << rs->ctx_aut->getStateName(t.dst_state)); BDD enc_src = encCtxAutState(t.src_state); BDD enc_dst = encCtxAutStateSucc(t.dst_state); - BDD enc_ctx = encActEntitiesConj(t.ctx); + BDD enc_ctx = compContext(encActEntitiesConj(t.ctx)); - *r += enc_src * enc_ctx * enc_dst; + *tr_ca += enc_src * enc_ctx * enc_dst; + // cout << "tr_ca:" << endl; + // BDD_PRINT(*tr_ca); } - - return r; + + // cout << "tr_ca:" << endl; + // BDD_PRINT(*tr_ca); } /** EOF **/ diff --git a/symrs.hh b/symrs.hh index c36624a..9bdc8ef 100644 --- a/symrs.hh +++ b/symrs.hh @@ -59,6 +59,7 @@ class SymRS vector *pv_ca_succ; BDD *pv_ca_E; BDD *pv_ca_succ_E; + BDD *tr_ca; unsigned int totalReactions; unsigned int totalStateVars; @@ -118,7 +119,11 @@ class SymRS void mapStateToAct(void); void encode(void); - int getMappedStateToActID(int stateID) const { assert(stateID < static_cast(totalStateVars)); return stateToAct[stateID]; } + int getMappedStateToActID(int stateID) const + { + assert(stateID < static_cast(totalStateVars)); + return stateToAct[stateID]; + } size_t getCtxAutStateEncodingSize(void); @@ -192,15 +197,20 @@ public: * @return Returns a vector of BDDs */ vector *getEncCtxAutPVsucc(void) { return pv_ca_succ; } + + /** + * @brief Encodes the monolithic transition relation + */ + void encodeCtxAutTrans(void); /** - * @brief Encodes the monolithic transition relation + * @brief Getter for context automaton's transition relation * * @return Returns a BDD encoding the transition relation */ - BDD *getEncCtxAutTrans(void); + BDD *getEncCtxAutTrans(void) { return tr_ca; } }; #endif -/** EOF **/ \ No newline at end of file +/** EOF **/