diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index edb5fd8a8..c21319204 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -58,10 +58,10 @@ public: /*! * Constructor * - * @param Dtmc The dtmc model which is checked. + * @param model The dtmc model which is checked. */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* dtmc) { - this->dtmc = dtmc; + explicit DtmcPrctlModelChecker(mrmc::models::Dtmc& model) { + this->model = &model; } /*! @@ -70,49 +70,32 @@ public: * @param modelChecker The model checker that is copied. */ explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - this->dtmc = new mrmc::models::Dtmc(modelChecker->getDtmc()); + this->model = new mrmc::models::Dtmc(modelChecker->getModel()); } /*! * Destructor */ virtual ~DtmcPrctlModelChecker() { - delete this->dtmc; + //should not be deleted here, according to ticket #24 + //delete this->dtmc; } /*! * @returns A reference to the dtmc of the model checker. */ - mrmc::models::Dtmc* getDtmc() const { - return this->dtmc; + mrmc::models::Dtmc& getModel() const { + return *(this->model); } /*! - * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all - * other edges from these states) - * - * @param states A bit vector representing a set of states that should become absorbing. - */ - virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0; - - /*! - * Returns all states that are labeled with a given atomic proposition. - * - * @param ap A string representing an atomic proposition. - * @returns The set of states labeled with the atomic proposition ap. + * Sets the DTMC model which is checked + * @param model */ - virtual mrmc::storage::BitVector* getStatesLabeledWith(std::string ap) { - return dtmc->getLabeledStates(ap); + void setModel(mrmc::models::Dtmc& model) { + this->model = &model; } - /*! - * Multiplies the matrix with a given vector; the result again is a vector. - * - * @param vector The vector to multiply the matrix with. - * @returns The result of multiplying the transition probability matrix with vector. - */ - virtual std::vector multiplyMatrixVector(std::vector* vector) = 0; - /*! * The check method for a state formula; Will infer the actual type of formula and delegate it * to the specialized method @@ -120,8 +103,8 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula& formula) { - return formula->check(this); + virtual mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) { + return formula.check(this); } /*! @@ -130,7 +113,7 @@ public: * @param formula The And formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkAnd(mrmc::formula::And& formula) { + virtual mrmc::storage::BitVector* checkAnd(const mrmc::formula::And& formula) { mrmc::storage::BitVector* result = check(formula.getLeft()); mrmc::storage::BitVector* right = check(formula.getRight()); (*result) &= (*right); @@ -144,8 +127,8 @@ public: * @param formula The AP state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkAP(mrmc::formula::AP& formula) { - return getStatesLabeledWith(formula.getAP()); + virtual mrmc::storage::BitVector* checkAP(const mrmc::formula::AP& formula) { + return model->getLabeledStates(formula.getAP()); } /*! @@ -154,7 +137,7 @@ public: * @param formula The Not state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkNot(mrmc::formula::Not& formula) { + virtual mrmc::storage::BitVector* checkNot(const mrmc::formula::Not& formula) { mrmc::storage::BitVector* result = check(formula.getChild()); result->complement(); return result; @@ -166,7 +149,7 @@ public: * @param formula The Or state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or& formula) { + virtual mrmc::storage::BitVector* checkOr(const mrmc::formula::Or& formula) { mrmc::storage::BitVector* result = check(formula.getLeft()); mrmc::storage::BitVector* right = check(formula.getRight()); (*result) |= (*right); @@ -180,7 +163,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator& formula); + virtual mrmc::storage::BitVector checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula); /*! * The check method for a path formula; Will infer the actual type of formula and delegate it @@ -189,8 +172,8 @@ public: * @param formula The path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula& formula) { - return formula->check(this); + virtual std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) { + return formula.check(this); } /*! @@ -199,7 +182,7 @@ public: * @param formula The Bounded Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil& formula) = 0; + virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) = 0; /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -207,7 +190,7 @@ public: * @param formula The Next path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkNext(mrmc::formula::Next& formula) = 0; + virtual std::vector* checkNext(const mrmc::formula::Next& formula) = 0; /*! * The check method for a path formula with an Until operator node as root in its formula tree @@ -215,10 +198,10 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkUntil(mrmc::formula::Until& formula) = 0; + virtual std::vector* checkUntil(const mrmc::formula::Until& formula) = 0; private: - mrmc::models::Dtmc* dtmc; + mrmc::models::Dtmc* model; }; } //namespace modelChecker