From def86df597789a0ad1fd6f794dd7c77c82025660 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Mon, 26 Mar 2018 19:37:08 +0100 Subject: [PATCH] Doc --- symrs.hh | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/symrs.hh b/symrs.hh index cc846c8..bd9ef99 100644 --- a/symrs.hh +++ b/symrs.hh @@ -152,14 +152,60 @@ public: BDD getBDDtrue(void) const { return BDD_TRUE; } BDD getBDDfalse(void) const { return BDD_FALSE; } + /** + * @brief Checks if context automaton is used + * + * @return True if CA is used + */ bool usingContextAutomaton(void) { return rs->ctx_aut != nullptr; } + /** + * @brief Encodes a context automaton's state + * + * @return Returns the encoded state + */ BDD encCtxAutState_raw(State state_id, bool succ) const; + + /** + * @brief Encodes a context automaton's state (as predecessor/non-primed) + * + * @return Returns the encoded state + */ BDD encCtxAutState(State state_id) const { return encCtxAutState_raw(state_id, false); } + + /** + * @brief Encodes a context automaton's state (as successor/primed) + * + * @return Returns the encoded state + */ BDD encCtxAutStateSucc(State state_id) const { return encCtxAutState_raw(state_id, true); } + + /** + * @brief Encodes the initial state of context automaton + * + * @return Returns the encoded state(s) + */ BDD *getEncCtxAutInitState(void); + + /** + * @brief Getter for context automaton's state variables (predecessor/non-primed) + * + * @return Returns a vector of BDDs + */ vector *getEncCtxAutPV(void); + + /** + * @brief Getter for context automaton's successor (primed) state variables + * + * @return Returns a vector of BDDs + */ vector *getEncCtxAutPVsucc(void); + + /** + * @brief Encodes the monolithic transition relation + * + * @return Returns a BDD encoding the transition relation + */ BDD *getEncCtxAutTrans(void); };