From 5ba7f63bc22191101a3025d1fd1d168ef14e305b Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 17 Feb 2013 15:06:00 +0100 Subject: [PATCH] Splitted RewardBoundOperator and ProbabilisticBoundOperator checking methods for model checkers (needed for enabling qualititative model checking for P operator with bounds 0/1). Moved some methods of DtmcModelChecker one level up to AbstractModelChecker. TODO: this should be done for other methods as well, but there are more changes needed for that to work. --- src/formula/Formulas.h | 1 + src/formula/PathBoundOperator.h | 33 +----- src/formula/ProbabilisticBoundOperator.h | 27 +++++ src/formula/RewardBoundOperator.h | 27 +++++ src/modelchecker/AbstractModelChecker.h | 98 ++++++++++++++- src/modelchecker/DtmcPrctlModelChecker.h | 112 ++++-------------- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 4 +- src/modelchecker/MdpPrctlModelChecker.h | 67 ----------- 8 files changed, 181 insertions(+), 188 deletions(-) diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 6e03975dd..193114cb1 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -35,6 +35,7 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +// FIXME: Why is this needed? To me this makes no sense. #include "modelchecker/DtmcPrctlModelChecker.h" #endif /* STORM_FORMULA_FORMULAS_H_ */ diff --git a/src/formula/PathBoundOperator.h b/src/formula/PathBoundOperator.h index d0f04975f..42002e04a 100644 --- a/src/formula/PathBoundOperator.h +++ b/src/formula/PathBoundOperator.h @@ -20,18 +20,6 @@ namespace formula { template class PathBoundOperator; -/*! - * @brief Interface class for model checkers that support PathBoundOperator. - * - * All model checkers that support the formula class PathBoundOperator must inherit - * this pure virtual class. - */ -template -class IPathBoundOperatorModelChecker { - public: - virtual storm::storage::BitVector* checkPathBoundOperator(const PathBoundOperator& obj) const = 0; -}; - /*! * @brief * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval @@ -132,10 +120,10 @@ public: virtual std::string toString() const { std::string result = ""; switch (comparisonOperator) { - case LESS: result += "< "; break; - case LESS_EQUAL: result += "<= "; break; - case GREATER: result += "> "; break; - case GREATER_EQUAL: result += ">= "; break; + case LESS: result += "<"; break; + case LESS_EQUAL: result += "<="; break; + case GREATER: result += ">"; break; + case GREATER_EQUAL: result += ">="; break; } result += std::to_string(bound); result += " ["; @@ -163,19 +151,6 @@ public: */ virtual AbstractStateFormula* clone() const = 0; - /*! - * Calls the model checker to check this formula. - * Needed to infer the correct type of formula class. - * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. - * - * @returns A bit vector indicating all states that satisfy the formula represented by the called object. - */ - virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkPathBoundOperator(*this); - } - /*! * @brief Checks if the subtree conforms to some logic. * diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index e9183950d..7104da47a 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -16,6 +16,20 @@ namespace storm { namespace formula { +template class ProbabilisticBoundOperator; + +/*! + * @brief Interface class for model checkers that support ProbabilisticBoundOperator. + * + * All model checkers that support the formula class PathBoundOperator must inherit + * this pure virtual class. + */ +template +class IProbabilisticBoundOperatorModelChecker { + public: + virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator& obj) const = 0; +}; + /*! * @brief * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval @@ -86,6 +100,19 @@ public: result->setPathFormula(this->getPathFormula().clone()); return result; } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkProbabilisticBoundOperator(*this); + } }; } //namespace formula diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index 3d08c6c95..ec507176a 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -16,6 +16,20 @@ namespace storm { namespace formula { +template class RewardBoundOperator; + +/*! + * @brief Interface class for model checkers that support RewardBoundOperator. + * + * All model checkers that support the formula class PathBoundOperator must inherit + * this pure virtual class. + */ +template +class IRewardBoundOperatorModelChecker { + public: + virtual storm::storage::BitVector* checkRewardBoundOperator(const RewardBoundOperator& obj) const = 0; +}; + /*! * @brief * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root. @@ -83,6 +97,19 @@ public: result->setPathFormula(this->getPathFormula().clone()); return result; } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkRewardBoundOperator(*this); + } }; } //namespace formula diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 69bbeb9da..991a7edc7 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -12,6 +12,7 @@ namespace storm { namespace modelChecker { template class AbstractModelChecker; }} +#include "src/exceptions/InvalidPropertyException.h" #include "src/formula/Formulas.h" #include "src/storage/BitVector.h" @@ -42,7 +43,8 @@ class AbstractModelChecker : public virtual storm::formula::IBoundedUntilModelChecker, public virtual storm::formula::IBoundedEventuallyModelChecker, public virtual storm::formula::INoBoundOperatorModelChecker, - public virtual storm::formula::IPathBoundOperatorModelChecker, + public virtual storm::formula::IProbabilisticBoundOperatorModelChecker, + public virtual storm::formula::IRewardBoundOperatorModelChecker, public virtual storm::formula::IReachabilityRewardModelChecker, public virtual storm::formula::ICumulativeRewardModelChecker, public virtual storm::formula::IInstantaneousRewardModelChecker { @@ -58,6 +60,100 @@ public: } return nullptr; } + + /*! + * The check method for a state formula with an And node as root in its formula tree + * + * @param formula The And formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + storm::storage::BitVector* checkAnd(const storm::formula::And& formula) const { + storm::storage::BitVector* result = formula.getLeft().check(*this); + storm::storage::BitVector* right = formula.getRight().check(*this); + (*result) &= (*right); + delete right; + return result; + } + + /*! + * The check method for a formula with a Not node as root in its formula tree + * + * @param formula The Not state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + storm::storage::BitVector* checkNot(const storm::formula::Not& formula) const { + storm::storage::BitVector* result = formula.getChild().check(*this); + result->complement(); + return result; + } + + /*! + * The check method for a state formula with an Or node as root in its formula tree + * + * @param formula The Or state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual storm::storage::BitVector* checkOr(const storm::formula::Or& formula) const { + storm::storage::BitVector* result = formula.getLeft().check(*this); + storm::storage::BitVector* right = formula.getRight().check(*this); + (*result) |= (*right); + delete right; + return result; + } + + /*! + * The check method for a state formula with a bound operator node as root in + * its formula tree + * + * @param formula The state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + storm::storage::BitVector* checkProbabilisticBoundOperator(const storm::formula::ProbabilisticBoundOperator& formula) const { + // First, we need to compute the probability for satisfying the path formula for each state. + std::vector* quantitativeResult = formula.getPathFormula().check(*this); + + // Create resulting bit vector, which will hold the yes/no-answer for every state. + storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size()); + + // Now, we can compute which states meet the bound specified in this operator and set the + // corresponding bits to true in the resulting vector. + for (uint_fast64_t i = 0; i < quantitativeResult->size(); ++i) { + if (formula.meetsBound((*quantitativeResult)[i])) { + result->set(i, true); + } + } + + // Delete the probabilities computed for the states and return result. + delete quantitativeResult; + return result; + } + + /*! + * The check method for a state formula with a bound operator node as root in + * its formula tree + * + * @param formula The state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + storm::storage::BitVector* checkRewardBoundOperator(const storm::formula::RewardBoundOperator& formula) const { + // First, we need to compute the probability for satisfying the path formula for each state. + std::vector* quantitativeResult = formula.getPathFormula().check(*this); + + // Create resulting bit vector, which will hold the yes/no-answer for every state. + storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size()); + + // Now, we can compute which states meet the bound specified in this operator and set the + // corresponding bits to true in the resulting vector. + for (uint_fast64_t i = 0; i < quantitativeResult->size(); ++i) { + if (formula.meetsBound((*quantitativeResult)[i])) { + result->set(i, true); + } + } + + // Delete the probabilities computed for the states and return result. + delete quantitativeResult; + return result; + } }; } //namespace modelChecker diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h index 32e1baa21..5b1f16600 100644 --- a/src/modelchecker/DtmcPrctlModelChecker.h +++ b/src/modelchecker/DtmcPrctlModelChecker.h @@ -47,7 +47,7 @@ public: * @param model The dtmc model which is checked. */ explicit DtmcPrctlModelChecker(storm::models::Dtmc& model) : model(model) { - + // Intentionally left empty. } /*! @@ -81,6 +81,27 @@ public: this->model = &model; } + /*! + * The check method for a formula with an AP node as root in its formula tree + * + * @param formula The Ap state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + storm::storage::BitVector* checkAp(const storm::formula::Ap& formula) const { + if (formula.getAp().compare("true") == 0) { + return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true); + } else if (formula.getAp().compare("false") == 0) { + return new storm::storage::BitVector(this->getModel().getNumberOfStates()); + } + + if (!this->getModel().hasAtomicProposition(formula.getAp())) { + LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); + throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; + } + + return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); + } + /*! * Checks the given state formula on the DTMC and prints the result (true/false) for all initial * states. @@ -150,95 +171,6 @@ public: return formula.check(*this); } - /*! - * The check method for a state formula with an And node as root in its formula tree - * - * @param formula The And formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkAnd(const storm::formula::And& formula) const { - storm::storage::BitVector* result = checkStateFormula(formula.getLeft()); - storm::storage::BitVector* right = checkStateFormula(formula.getRight()); - (*result) &= (*right); - delete right; - return result; - } - - /*! - * The check method for a formula with an AP node as root in its formula tree - * - * @param formula The Ap state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkAp(const storm::formula::Ap& formula) const { - if (formula.getAp().compare("true") == 0) { - return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true); - } else if (formula.getAp().compare("false") == 0) { - return new storm::storage::BitVector(this->getModel().getNumberOfStates()); - } - - if (!this->getModel().hasAtomicProposition(formula.getAp())) { - LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); - throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; - return nullptr; - } - - return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); - } - - /*! - * The check method for a formula with a Not node as root in its formula tree - * - * @param formula The Not state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkNot(const storm::formula::Not& formula) const { - storm::storage::BitVector* result = checkStateFormula(formula.getChild()); - result->complement(); - return result; - } - - /*! - * The check method for a state formula with an Or node as root in its formula tree - * - * @param formula The Or state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - virtual storm::storage::BitVector* checkOr(const storm::formula::Or& formula) const { - storm::storage::BitVector* result = checkStateFormula(formula.getLeft()); - storm::storage::BitVector* right = checkStateFormula(formula.getRight()); - (*result) |= (*right); - delete right; - return result; - } - - /*! - * The check method for a state formula with a bound operator node as root in - * its formula tree - * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkPathBoundOperator(const storm::formula::PathBoundOperator& formula) const { - // First, we need to compute the probability for satisfying the path formula for each state. - std::vector* quantitativeResult = this->checkPathFormula(formula.getPathFormula()); - - // Create resulting bit vector, which will hold the yes/no-answer for every state. - storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates()); - - // Now, we can compute which states meet the bound specified in this operator and set the - // corresponding bits to true in the resulting vector. - for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { - if (formula.meetsBound((*quantitativeResult)[i])) { - result->set(i, true); - } - } - - // Delete the probabilities computed for the states and return result. - delete quantitativeResult; - return result; - } - /*! * The check method for a state formula with a probabilistic operator node without bounds as root * in its formula tree diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index 308a6e80e..ac5d97158 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -39,7 +39,9 @@ template class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { public: - explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } + explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { + // Intentionally left empty. + } virtual ~GmmxxDtmcPrctlModelChecker() { } diff --git a/src/modelchecker/MdpPrctlModelChecker.h b/src/modelchecker/MdpPrctlModelChecker.h index 7dfb88825..d1a948ed5 100644 --- a/src/modelchecker/MdpPrctlModelChecker.h +++ b/src/modelchecker/MdpPrctlModelChecker.h @@ -151,20 +151,6 @@ public: return formula.check(*this); } - /*! - * The check method for a state formula with an And node as root in its formula tree - * - * @param formula The And formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkAnd(const storm::formula::And& formula) const { - storm::storage::BitVector* result = checkStateFormula(formula.getLeft()); - storm::storage::BitVector* right = checkStateFormula(formula.getRight()); - (*result) &= (*right); - delete right; - return result; - } - /*! * The check method for a formula with an AP node as root in its formula tree * @@ -187,59 +173,6 @@ public: return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); } - /*! - * The check method for a formula with a Not node as root in its formula tree - * - * @param formula The Not state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkNot(const storm::formula::Not& formula) const { - storm::storage::BitVector* result = checkStateFormula(formula.getChild()); - result->complement(); - return result; - } - - /*! - * The check method for a state formula with an Or node as root in its formula tree - * - * @param formula The Or state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - virtual storm::storage::BitVector* checkOr(const storm::formula::Or& formula) const { - storm::storage::BitVector* result = checkStateFormula(formula.getLeft()); - storm::storage::BitVector* right = checkStateFormula(formula.getRight()); - (*result) |= (*right); - delete right; - return result; - } - - /*! - * The check method for a state formula with a bound operator node as root in - * its formula tree - * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkPathBoundOperator(const storm::formula::PathBoundOperator& formula) const { - // First, we need to compute the probability for satisfying the path formula for each state. - std::vector* quantitativeResult = this->checkPathFormula(formula.getPathFormula()); - - // Create resulting bit vector, which will hold the yes/no-answer for every state. - storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates()); - - // Now, we can compute which states meet the bound specified in this operator and set the - // corresponding bits to true in the resulting vector. - for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { - if (formula.meetsBound((*quantitativeResult)[i])) { - result->set(i, true); - } - } - - // Delete the probabilities computed for the states and return result. - delete quantitativeResult; - return result; - } - /*! * The check method for a state formula with a probabilistic operator node without bounds as root * in its formula tree