From 73623ff3f6ee72e5a72e65f99832919f18677696 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 17 Feb 2013 15:50:02 +0100 Subject: [PATCH] Added boolean parameter qualitative to all path formulas, i.e. to the checking and the callback methods. --- src/formula/AbstractPathFormula.h | 2 +- src/formula/BoundedEventually.h | 6 +-- src/formula/BoundedNaryUntil.h | 6 +-- src/formula/BoundedUntil.h | 6 +-- src/formula/CumulativeReward.h | 6 +-- src/formula/Eventually.h | 6 +-- src/formula/Globally.h | 6 +-- src/formula/InstantaneousReward.h | 6 +-- src/formula/Next.h | 6 +-- src/formula/ReachabilityReward.h | 6 +-- src/formula/Until.h | 6 +-- src/modelchecker/AbstractModelChecker.h | 4 +- src/modelchecker/DtmcPrctlModelChecker.h | 48 +++++-------------- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 24 +++++----- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 24 +++++----- src/modelchecker/MdpPrctlModelChecker.h | 48 +++++-------------- 16 files changed, 83 insertions(+), 127 deletions(-) diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h index 5d7d6e281..d0ee74efd 100644 --- a/src/formula/AbstractPathFormula.h +++ b/src/formula/AbstractPathFormula.h @@ -61,7 +61,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const = 0; + virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; }; } //namespace formula diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h index 3bb72d07e..fe7776f33 100644 --- a/src/formula/BoundedEventually.h +++ b/src/formula/BoundedEventually.h @@ -36,7 +36,7 @@ class IBoundedEventuallyModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkBoundedEventually(const BoundedEventually& obj) const = 0; + virtual std::vector* checkBoundedEventually(const BoundedEventually& obj, bool qualitative) const = 0; }; /*! @@ -157,8 +157,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkBoundedEventually(*this); + virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkBoundedEventually(*this, qualitative); } /*! diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h index 91bd44713..7c98af61e 100644 --- a/src/formula/BoundedNaryUntil.h +++ b/src/formula/BoundedNaryUntil.h @@ -37,7 +37,7 @@ class IBoundedNaryUntilModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkBoundedNaryUntil(const BoundedNaryUntil& obj) const = 0; + virtual std::vector* checkBoundedNaryUntil(const BoundedNaryUntil& obj, bool qualitative) const = 0; }; /*! @@ -179,8 +179,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkBoundedNaryUntil(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkBoundedNaryUntil(*this, qualitative); } /*! diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 7b4a7e07c..de0a88d2c 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -34,7 +34,7 @@ class IBoundedUntilModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkBoundedUntil(const BoundedUntil& obj) const = 0; + virtual std::vector* checkBoundedUntil(const BoundedUntil& obj, bool qualitative) const = 0; }; /*! @@ -186,8 +186,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkBoundedUntil(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkBoundedUntil(*this, qualitative); } /*! diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h index e89bcfbaf..6275621db 100644 --- a/src/formula/CumulativeReward.h +++ b/src/formula/CumulativeReward.h @@ -35,7 +35,7 @@ class ICumulativeRewardModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkCumulativeReward(const CumulativeReward& obj) const = 0; + virtual std::vector* checkCumulativeReward(const CumulativeReward& obj, bool qualitative) const = 0; }; /*! @@ -121,8 +121,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkCumulativeReward(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkCumulativeReward(*this, qualitative); } /*! diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h index 53b7b0dd1..668546f0c 100644 --- a/src/formula/Eventually.h +++ b/src/formula/Eventually.h @@ -33,7 +33,7 @@ class IEventuallyModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkEventually(const Eventually& obj) const = 0; + virtual std::vector* checkEventually(const Eventually& obj, bool qualitative) const = 0; }; /*! @@ -131,8 +131,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkEventually(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkEventually(*this, qualitative); } /*! diff --git a/src/formula/Globally.h b/src/formula/Globally.h index 05041ee17..7b58580e9 100644 --- a/src/formula/Globally.h +++ b/src/formula/Globally.h @@ -34,7 +34,7 @@ class IGloballyModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkGlobally(const Globally& obj) const = 0; + virtual std::vector* checkGlobally(const Globally& obj, bool qualitative) const = 0; }; /*! @@ -132,8 +132,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkGlobally(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkGlobally(*this, qualitative); } /*! diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h index 8f55b2c7c..ed0f7affa 100644 --- a/src/formula/InstantaneousReward.h +++ b/src/formula/InstantaneousReward.h @@ -35,7 +35,7 @@ class IInstantaneousRewardModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkInstantaneousReward(const InstantaneousReward& obj) const = 0; + virtual std::vector* checkInstantaneousReward(const InstantaneousReward& obj, bool qualitative) const = 0; }; /*! @@ -121,8 +121,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkInstantaneousReward(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkInstantaneousReward(*this, qualitative); } /*! diff --git a/src/formula/Next.h b/src/formula/Next.h index a91a39ce1..91d68d05a 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -33,7 +33,7 @@ class INextModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkNext(const Next& obj) const = 0; + virtual std::vector* checkNext(const Next& obj, bool qualitative) const = 0; }; /*! @@ -133,8 +133,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkNext(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkNext(*this, qualitative); } /*! diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h index a725e202a..ff8155eb5 100644 --- a/src/formula/ReachabilityReward.h +++ b/src/formula/ReachabilityReward.h @@ -32,7 +32,7 @@ class IReachabilityRewardModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkReachabilityReward(const ReachabilityReward& obj) const = 0; + virtual std::vector* checkReachabilityReward(const ReachabilityReward& obj, bool qualitative) const = 0; }; /*! @@ -127,8 +127,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkReachabilityReward(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkReachabilityReward(*this, qualitative); } /*! diff --git a/src/formula/Until.h b/src/formula/Until.h index 82ac05c9d..29c0e497d 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -32,7 +32,7 @@ class IUntilModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkUntil(const Until& obj) const = 0; + virtual std::vector* checkUntil(const Until& obj, bool qualitative) const = 0; }; /*! @@ -160,8 +160,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkUntil(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkUntil(*this, qualitative); } /*! diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 991a7edc7..244b35df1 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -110,7 +110,7 @@ public: */ 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); + std::vector* quantitativeResult = formula.getPathFormula().check(*this, false); // Create resulting bit vector, which will hold the yes/no-answer for every state. storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size()); @@ -137,7 +137,7 @@ public: */ 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); + std::vector* quantitativeResult = formula.getPathFormula().check(*this, false); // Create resulting bit vector, which will hold the yes/no-answer for every state. storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size()); diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h index 5b1f16600..61a9b2ffd 100644 --- a/src/modelchecker/DtmcPrctlModelChecker.h +++ b/src/modelchecker/DtmcPrctlModelChecker.h @@ -160,17 +160,6 @@ public: storm::utility::printSeparationLine(std::cout); } - /*! - * The check method for a state formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkStateFormula(const storm::formula::AbstractStateFormula& formula) const { - return formula.check(*this); - } - /*! * The check method for a state formula with a probabilistic operator node without bounds as root * in its formula tree @@ -183,18 +172,7 @@ public: if (formula.isOptimalityOperator()) { LOG4CPLUS_WARN(logger, "Formula contains min/max operator which is not meaningful over deterministic models."); } - return formula.getPathFormula().check(*this); - } - - /*! - * The check method for a path formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @param formula The path formula to check - * @returns for each state the probability that the path formula holds. - */ - std::vector* checkPathFormula(const storm::formula::AbstractPathFormula& formula) const { - return formula.check(*this); + return formula.getPathFormula().check(*this, false); } /*! @@ -203,7 +181,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(const storm::formula::BoundedUntil& formula) const = 0; + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -211,7 +189,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(const storm::formula::Next& formula) const = 0; + virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Bounded Eventually operator node as root in its @@ -220,10 +198,10 @@ public: * @param formula The Bounded Eventually path formula to check * @returns for each state the probability that the path formula holds */ - virtual std::vector* checkBoundedEventually(const storm::formula::BoundedEventually& formula) const { + virtual std::vector* checkBoundedEventually(const storm::formula::BoundedEventually& formula, bool qualitative) const { // Create equivalent temporary bounded until formula and check it. storm::formula::BoundedUntil temporaryBoundedUntilFormula(new storm::formula::Ap("true"), formula.getChild().clone(), formula.getBound()); - return this->checkBoundedUntil(temporaryBoundedUntilFormula); + return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); } /*! @@ -232,10 +210,10 @@ public: * @param formula The Eventually path formula to check * @returns for each state the probability that the path formula holds */ - virtual std::vector* checkEventually(const storm::formula::Eventually& formula) const { + virtual std::vector* checkEventually(const storm::formula::Eventually& formula, bool qualitative) const { // Create equivalent temporary until formula and check it. storm::formula::Until temporaryUntilFormula(new storm::formula::Ap("true"), formula.getChild().clone()); - return this->checkUntil(temporaryUntilFormula); + return this->checkUntil(temporaryUntilFormula, qualitative); } /*! @@ -244,10 +222,10 @@ public: * @param formula The Globally path formula to check * @returns for each state the probability that the path formula holds */ - virtual std::vector* checkGlobally(const storm::formula::Globally& formula) const { + virtual std::vector* checkGlobally(const storm::formula::Globally& formula, bool qualitative) const { // Create "equivalent" temporary eventually formula and check it. storm::formula::Eventually temporaryEventuallyFormula(new storm::formula::Not(formula.getChild().clone())); - std::vector* result = this->checkEventually(temporaryEventuallyFormula); + std::vector* result = this->checkEventually(temporaryEventuallyFormula, qualitative); // Now subtract the resulting vector from the constant one vector to obtain final result. storm::utility::subtractFromConstantOneVector(result); @@ -260,7 +238,7 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkUntil(const storm::formula::Until& formula) const = 0; + virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const = 0; /*! * The check method for a path formula with an Instantaneous Reward operator node as root in its @@ -269,7 +247,7 @@ public: * @param formula The Instantaneous Reward formula to check * @returns for each state the reward that the instantaneous reward yields */ - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula) const = 0; + virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Cumulative Reward operator node as root in its @@ -278,7 +256,7 @@ public: * @param formula The Cumulative Reward formula to check * @returns for each state the reward that the cumulative reward yields */ - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula) const = 0; + virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Reachability Reward operator node as root in its @@ -287,7 +265,7 @@ public: * @param formula The Reachbility Reward formula to check * @returns for each state the reward that the reachability reward yields */ - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula) const = 0; + virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const = 0; private: storm::models::Dtmc& model; diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index ac5d97158..a75276405 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -45,10 +45,10 @@ public: virtual ~GmmxxDtmcPrctlModelChecker() { } - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula) const { + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); // Copy the matrix before we make any changes. storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); @@ -81,9 +81,9 @@ public: return result; } - virtual std::vector* checkNext(const storm::formula::Next& formula) const { + virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formula of the next-formula. - storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); + storm::storage::BitVector* nextStates = formula.getChild().check(*this); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); @@ -106,10 +106,10 @@ public: return result; } - virtual std::vector* checkUntil(const storm::formula::Until& formula) const { + virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. @@ -169,7 +169,7 @@ public: return result; } - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula) const { + virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const { // Only compute the result if the model has a state-based reward model. if (!this->getModel().hasStateRewards()) { LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); @@ -198,7 +198,7 @@ public: return result; } - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula) const { + virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); @@ -241,7 +241,7 @@ public: return result; } - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula) const { + virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); @@ -249,7 +249,7 @@ public: } // Determine the states for which the target predicate holds. - storm::storage::BitVector* targetStates = this->checkStateFormula(formula.getChild()); + storm::storage::BitVector* targetStates = formula.getChild().check(*this); // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index 41efbd145..1c8741ebd 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -43,10 +43,10 @@ public: virtual ~GmmxxMdpPrctlModelChecker() { } - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula) const { + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); // Copy the matrix before we make any changes. storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); @@ -88,9 +88,9 @@ public: return result; } - virtual std::vector* checkNext(const storm::formula::Next& formula) const { + virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formula of the next-formula. - storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); + storm::storage::BitVector* nextStates = formula.getChild().check(*this); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); @@ -124,10 +124,10 @@ public: return result; } - virtual std::vector* checkUntil(const storm::formula::Until& formula) const { + virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. @@ -191,7 +191,7 @@ public: return result; } - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula) const { + virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const { // Only compute the result if the model has a state-based reward model. if (!this->getModel().hasStateRewards()) { LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); @@ -220,7 +220,7 @@ public: return result; } - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula) const { + virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); @@ -263,7 +263,7 @@ public: return result; } - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula) const { + virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); @@ -271,7 +271,7 @@ public: } // Determine the states for which the target predicate holds. - storm::storage::BitVector* targetStates = this->checkStateFormula(formula.getChild()); + storm::storage::BitVector* targetStates = formula.getChild().check(*this); // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); diff --git a/src/modelchecker/MdpPrctlModelChecker.h b/src/modelchecker/MdpPrctlModelChecker.h index d1a948ed5..c2fad0b21 100644 --- a/src/modelchecker/MdpPrctlModelChecker.h +++ b/src/modelchecker/MdpPrctlModelChecker.h @@ -140,17 +140,6 @@ public: storm::utility::printSeparationLine(std::cout); } - /*! - * The check method for a state formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkStateFormula(const storm::formula::AbstractStateFormula& formula) const { - return formula.check(*this); - } - /*! * The check method for a formula with an AP node as root in its formula tree * @@ -187,29 +176,18 @@ public: throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; } minimumOperatorStack.push(formula.isMinimumOperator()); - std::vector* result = formula.getPathFormula().check(*this); + std::vector* result = formula.getPathFormula().check(*this, false); minimumOperatorStack.pop(); return result; } - /*! - * The check method for a path formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @param formula The path formula to check - * @returns for each state the probability that the path formula holds. - */ - std::vector* checkPathFormula(const storm::formula::AbstractPathFormula& formula) const { - return formula.check(*this); - } - /*! * The check method for a path formula with a Bounded Until operator node as root in its formula tree * * @param formula The Bounded Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula) const = 0; + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -217,7 +195,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(const storm::formula::Next& formula) const = 0; + virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Bounded Eventually operator node as root in its @@ -226,10 +204,10 @@ public: * @param formula The Bounded Eventually path formula to check * @returns for each state the probability that the path formula holds */ - virtual std::vector* checkBoundedEventually(const storm::formula::BoundedEventually& formula) const { + virtual std::vector* checkBoundedEventually(const storm::formula::BoundedEventually& formula, bool qualitative) const { // Create equivalent temporary bounded until formula and check it. storm::formula::BoundedUntil temporaryBoundedUntilFormula(new storm::formula::Ap("true"), formula.getChild().clone(), formula.getBound()); - return this->checkBoundedUntil(temporaryBoundedUntilFormula); + return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); } /*! @@ -238,10 +216,10 @@ public: * @param formula The Eventually path formula to check * @returns for each state the probability that the path formula holds */ - virtual std::vector* checkEventually(const storm::formula::Eventually& formula) const { + virtual std::vector* checkEventually(const storm::formula::Eventually& formula, bool qualitative) const { // Create equivalent temporary until formula and check it. storm::formula::Until temporaryUntilFormula(new storm::formula::Ap("true"), formula.getChild().clone()); - return this->checkUntil(temporaryUntilFormula); + return this->checkUntil(temporaryUntilFormula, qualitative); } /*! @@ -250,10 +228,10 @@ public: * @param formula The Globally path formula to check * @returns for each state the probability that the path formula holds */ - virtual std::vector* checkGlobally(const storm::formula::Globally& formula) const { + virtual std::vector* checkGlobally(const storm::formula::Globally& formula, bool qualitative) const { // Create "equivalent" temporary eventually formula and check it. storm::formula::Eventually temporaryEventuallyFormula(new storm::formula::Not(formula.getChild().clone())); - std::vector* result = this->checkEventually(temporaryEventuallyFormula); + std::vector* result = this->checkEventually(temporaryEventuallyFormula, qualitative); // Now subtract the resulting vector from the constant one vector to obtain final result. storm::utility::subtractFromConstantOneVector(result); @@ -266,7 +244,7 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkUntil(const storm::formula::Until& formula) const = 0; + virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const = 0; /*! * The check method for a path formula with an Instantaneous Reward operator node as root in its @@ -275,7 +253,7 @@ public: * @param formula The Instantaneous Reward formula to check * @returns for each state the reward that the instantaneous reward yields */ - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula) const = 0; + virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Cumulative Reward operator node as root in its @@ -284,7 +262,7 @@ public: * @param formula The Cumulative Reward formula to check * @returns for each state the reward that the cumulative reward yields */ - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula) const = 0; + virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const = 0; /*! * The check method for a path formula with a Reachability Reward operator node as root in its @@ -293,7 +271,7 @@ public: * @param formula The Reachbility Reward formula to check * @returns for each state the reward that the reachability reward yields */ - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula) const = 0; + virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const = 0; private: storm::models::Mdp& model;