diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 5517dbacd..d7538defc 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -1,5 +1,5 @@ /* - * DtmcPrctlModelChecker.h + * AbstractModelChecker.h * * Created on: 22.10.2012 * Author: Thomas Heinemann @@ -8,31 +8,42 @@ #ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ #define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ -namespace storm { namespace modelChecker { -template <class Type> class AbstractModelChecker; -}} +// Forward declaration of abstract model checker class needed by the formula classes. +namespace storm { +namespace modelChecker { + + template <class Type> class AbstractModelChecker; + +} +} #include "src/exceptions/InvalidPropertyException.h" #include "src/formula/Formulas.h" #include "src/storage/BitVector.h" #include "src/models/AbstractModel.h" +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + #include <iostream> +extern log4cplus::Logger logger; + namespace storm { namespace modelChecker { /*! * @brief - * Interface for model checker classes. - * - * This class provides basic functions that are the same for all subclasses, but mainly only declares - * abstract methods that are to be implemented in concrete instances. + * (Abstract) interface for all model checker classes. * - * @attention This class is abstract. + * This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares + * abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common + * to all model checkers for state-based models. */ template<class Type> class AbstractModelChecker : + // A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to + // be implemented that performs the corresponding check. public virtual storm::formula::IApModelChecker<Type>, public virtual storm::formula::IAndModelChecker<Type>, public virtual storm::formula::IOrModelChecker<Type>, @@ -51,32 +62,64 @@ class AbstractModelChecker : public virtual storm::formula::IInstantaneousRewardModelChecker<Type> { public: - explicit AbstractModelChecker(storm::models::AbstractModel<Type>& model) - : model(model) { - // Nothing to do here... + /*! + * Constructs an AbstractModelChecker with the given model. + */ + explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) { + // Intentionally left empty. } - explicit AbstractModelChecker(AbstractModelChecker<Type>* modelChecker) - : model(modelChecker->model) { + /*! + * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly + * constructed model checker will have the model of the given model checker as its associated model. + */ + explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelChecker) : model(modelChecker.model) { + // Intentionally left empty. } + /*! + * Returns a pointer to the model checker object that is of the requested type as given by the template parameters. + * @returns A pointer to the model checker object that is of the requested type as given by the template parameters. + * If the model checker is not of the requested type, type casting will fail and result in an exception. + */ template <template <class T> class Target> const Target<Type>* as() const { try { const Target<Type>* target = dynamic_cast<const Target<Type>*>(this); return target; } catch (std::bad_cast& bc) { - std::cerr << "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << std::endl; + LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << "."); + throw bc; } return nullptr; } /*! - * Checks the given state formula on the DTMC and prints the result (true/false) for all initial - * states. + * Retrieves the model associated with this model checker as a constant reference to an object of the type given + * by the template parameter. + * + * @returns A constant reference of the specified type to the model associated with this model checker. If the model + * is not of the requested type, type casting will fail and result in an exception. + */ + template <class Model> + Model const& getModel() const { + try { + Model const& target = dynamic_cast<Model const&>(this->model); + return target; + } catch (std::bad_cast& bc) { + LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << "."); + throw bc; + } + return nullptr; + } + + /*! + * Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e. + * states that carry the atomic proposition "init". + * * @param stateFormula The formula to be checked. */ - void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const { + void check(storm::formula::AbstractStateFormula<Type> const& stateFormula) const { std::cout << std::endl; LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; @@ -92,6 +135,7 @@ public: delete result; } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; + LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); if (result != nullptr) { delete result; } @@ -101,11 +145,12 @@ public: } /*! - * Checks the given operator (with no bound) on the DTMC and prints the result - * (probability/rewards) for all initial states. + * Checks the given formula (with no bound) on the model and prints the result (probability/rewards) for all + * initial states, i.e. states that carry the atomic proposition "init". + * * @param noBoundFormula The formula to be checked. */ - void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const { + void check(storm::formula::NoBoundOperator<Type> const& noBoundFormula) const { std::cout << std::endl; LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; @@ -130,15 +175,15 @@ public: } /*! - * The check method for a formula with an AP node as root in its formula tree + * Checks the given formula consisting of a single atomic proposition. * - * @param formula The Ap state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The formula to be checked. + * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& formula) const { - if (formula.getAp().compare("true") == 0) { + storm::storage::BitVector* checkAp(storm::formula::Ap<Type> const& formula) const { + if (formula.getAp() == "true") { return new storm::storage::BitVector(model.getNumberOfStates(), true); - } else if (formula.getAp().compare("false") == 0) { + } else if (formula.getAp() == "false") { return new storm::storage::BitVector(model.getNumberOfStates()); } @@ -151,12 +196,12 @@ public: } /*! - * The check method for a state formula with an And node as root in its formula tree + * Checks the given formula that is a logical "and" of two formulae. * - * @param formula The And formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The formula to be checked. + * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector* checkAnd(const storm::formula::And<Type>& formula) const { + storm::storage::BitVector* checkAnd(storm::formula::And<Type> const& formula) const { storm::storage::BitVector* result = formula.getLeft().check(*this); storm::storage::BitVector* right = formula.getRight().check(*this); (*result) &= (*right); @@ -165,43 +210,43 @@ public: } /*! - * The check method for a formula with a Not node as root in its formula tree + * Checks the given formula that is a logical "or" of two formulae. * - * @param formula The Not state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The formula to check. + * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector* checkNot(const storm::formula::Not<Type>& formula) const { - storm::storage::BitVector* result = formula.getChild().check(*this); - result->complement(); + virtual storm::storage::BitVector* checkOr(storm::formula::Or<Type> const& 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 an Or node as root in its formula tree + * Checks the given formula that is a logical "not" of a sub-formula. * - * @param formula The Or state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The 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<Type>& formula) const { - storm::storage::BitVector* result = formula.getLeft().check(*this); - storm::storage::BitVector* right = formula.getRight().check(*this); - (*result) |= (*right); - delete right; + storm::storage::BitVector* checkNot(const storm::formula::Not<Type>& formula) const { + storm::storage::BitVector* result = formula.getChild().check(*this); + result->complement(); return result; } + /*! - * The check method for a state formula with a bound operator node as root in - * its formula tree + * Checks the given formula that is a P operator over a path formula featuring a value bound. * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The formula to check. + * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector* checkProbabilisticBoundOperator(const storm::formula::ProbabilisticBoundOperator<Type>& formula) const { + storm::storage::BitVector* checkProbabilisticBoundOperator(storm::formula::ProbabilisticBoundOperator<Type> const& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false); - // Create resulting bit vector, which will hold the yes/no-answer for every state. + // Create resulting bit vector that 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 @@ -218,17 +263,16 @@ public: } /*! - * The check method for a state formula with a bound operator node as root in - * its formula tree + * Checks the given formula that is an R operator over a reward formula featuring a value bound. * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The formula to check. + * @returns The set of states satisfying the formula represented by a bit vector. */ storm::storage::BitVector* checkRewardBoundOperator(const storm::formula::RewardBoundOperator<Type>& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false); - // Create resulting bit vector, which will hold the yes/no-answer for every state. + // Create resulting bit vector that 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 @@ -244,22 +288,19 @@ public: return result; } - void setModel(storm::models::AbstractModel<Type>& model) { - this->model = model; - } - - template <class Model> - Model& getModel() const { - return *dynamic_cast<Model*>(&this->model); - } - private: - storm::models::AbstractModel<Type>& model; + /*! + * A constant reference to the model associated with this model checker. + * + * @note that we do not own this object, but merely have a constant reference to it. That means that using the + * model checker object is unsafe after the object has been destroyed. + */ + storm::models::AbstractModel<Type> const& model; }; -} //namespace modelChecker +} // namespace modelchecker -} //namespace storm +} // namespace storm #endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h similarity index 55% rename from src/modelchecker/DtmcPrctlModelChecker.h rename to src/modelchecker/SparseDtmcPrctlModelChecker.h index 3fa4cc238..ff239cdb4 100644 --- a/src/modelchecker/DtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -1,102 +1,84 @@ /* - * DtmcPrctlModelChecker.h + * SparseDtmcPrctlModelChecker.h * * Created on: 22.10.2012 * Author: Thomas Heinemann */ -#ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ -#define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ - -#include <vector> - -#include "src/formula/Formulas.h" -#include "src/utility/Vector.h" -#include "src/storage/SparseMatrix.h" +#ifndef STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ +#include "src/modelchecker/AbstractModelChecker.h" #include "src/models/Dtmc.h" -#include "src/storage/BitVector.h" -#include "src/exceptions/InvalidPropertyException.h" +#include "src/storage/SparseMatrix.h" #include "src/utility/Vector.h" #include "src/utility/GraphAnalyzer.h" -#include "src/modelchecker/AbstractModelChecker.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; +#include <vector> namespace storm { - namespace modelChecker { /*! * @brief - * Interface for model checker classes. - * - * This class provides basic functions that are the same for all subclasses, but mainly only declares - * abstract methods that are to be implemented in concrete instances. - * - * @attention This class is abstract. + * Interface for all model checkers that can verify PRCTL formulae over DTMCs represented as a sparse matrix. */ template<class Type> -class DtmcPrctlModelChecker : public AbstractModelChecker<Type> { +class SparseDtmcPrctlModelChecker : public AbstractModelChecker<Type> { public: /*! - * Constructor - * - * @param model The dtmc model which is checked. - */ - explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model) : AbstractModelChecker<Type>(model) { - // Intentionally left empty. - } - - /*! - * Copy constructor + * Constructs a SparseDtmcPrctlModelChecker with the given model. * - * @param modelChecker The model checker that is copied. + * @param model The DTMC to be checked. */ - explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) : AbstractModelChecker<Type>(modelChecker) { + explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<Type> const& model) : AbstractModelChecker<Type>(model) { // Intentionally left empty. } /*! - * Destructor + * Copy constructs an SparseDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly + * constructed model checker will have the model of the given model checker as its associated model. */ - virtual ~DtmcPrctlModelChecker() { + explicit SparseDtmcPrctlModelChecker(storm::modelChecker::SparseDtmcPrctlModelChecker<Type> const& modelChecker) : AbstractModelChecker<Type>(modelChecker) { // Intentionally left empty. } /*! - * @returns A reference to the dtmc of the model checker. + * Returns a constant reference to the DTMC associated with this model checker. + * @returns A constant reference to the DTMC associated with this model checker. */ - storm::models::Dtmc<Type>& getModel() const { + storm::models::Dtmc<Type> const& getModel() const { return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>(); } /*! - * The check method for a state formula with a probabilistic operator node without bounds as root - * in its formula tree + * Checks the given formula that is a P/R operator without a bound. * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The formula to check. + * @returns The set of states satisfying the formula represented by a bit vector. */ - std::vector<Type>* checkNoBoundOperator(const storm::formula::NoBoundOperator<Type>& formula) const { + std::vector<Type>* checkNoBoundOperator(storm::formula::NoBoundOperator<Type> const& formula) const { // Check if the operator was an optimality operator and report a warning in that case. if (formula.isOptimalityOperator()) { - LOG4CPLUS_WARN(logger, "Formula contains min/max operator which is not meaningful over deterministic models."); + LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); } return formula.getPathFormula().check(*this, false); } /*! - * The check method for a path formula with a Bounded Until operator node as root in its formula tree + * Checks the given formula that is a bounded-until formula. * - * @param formula The Bounded Until path formula to check - * @returns for each state the probability that the path formula holds. + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + virtual std::vector<Type>* checkBoundedUntil(storm::formula::BoundedUntil<Type> const& formula, bool qualitative) const { + // First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula. storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); @@ -122,12 +104,17 @@ public: } /*! - * The check method for a path formula with a Next operator node as root in its formula tree + * Checks the given formula that is a next formula. * - * @param formula The Next path formula to check - * @returns for each state the probability that the path formula holds. + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const { + virtual std::vector<Type>* checkNext(storm::formula::Next<Type> const& formula, bool qualitative) const { // First, we need to compute the states that satisfy the child formula of the next-formula. storm::storage::BitVector* nextStates = formula.getChild().check(*this); @@ -146,38 +133,52 @@ public: } /*! - * The check method for a path formula with a Bounded Eventually operator node as root in its - * formula tree + * Checks the given formula that is a bounded-eventually formula. * - * @param formula The Bounded Eventually path formula to check - * @returns for each state the probability that the path formula holds + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - virtual std::vector<Type>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula, bool qualitative) const { + virtual std::vector<Type>* checkBoundedEventually(storm::formula::BoundedEventually<Type> const& formula, bool qualitative) const { // Create equivalent temporary bounded until formula and check it. storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound()); return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); } /*! - * The check method for a path formula with an Eventually operator node as root in its formula tree + * Checks the given formula that is an eventually formula. * - * @param formula The Eventually path formula to check - * @returns for each state the probability that the path formula holds + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - virtual std::vector<Type>* checkEventually(const storm::formula::Eventually<Type>& formula, bool qualitative) const { + virtual std::vector<Type>* checkEventually(storm::formula::Eventually<Type> const& formula, bool qualitative) const { // Create equivalent temporary until formula and check it. storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone()); return this->checkUntil(temporaryUntilFormula, qualitative); } /*! - * The check method for a path formula with a Globally operator node as root in its formula tree + * Checks the given formula that is a globally formula. * - * @param formula The Globally path formula to check - * @returns for each state the probability that the path formula holds + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - virtual std::vector<Type>* checkGlobally(const storm::formula::Globally<Type>& formula, bool qualitative) const { - // Create "equivalent" temporary eventually formula and check it. + virtual std::vector<Type>* checkGlobally(storm::formula::Globally<Type> const& formula, bool qualitative) const { + // Create "equivalent" (equivalent up to negation) temporary eventually formula and check it. storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone())); std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative); @@ -187,12 +188,17 @@ public: } /*! - * The check method for a path formula with an Until operator node as root in its formula tree + * Check the given formula that is an until formula. * - * @param formula The Until path formula to check - * @returns for each state the probability that the path formula holds. + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const { + virtual std::vector<Type>* checkUntil(storm::formula::Until<Type> const& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); @@ -256,13 +262,17 @@ public: } /*! - * The check method for a path formula with an Instantaneous Reward operator node as root in its - * formula tree + * Checks the given formula that is an instantaneous reward formula. * - * @param formula The Instantaneous Reward formula to check - * @returns for each state the reward that the instantaneous reward yields + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bound 0. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bound 0. + * @returns The reward values for the given formula for every state of the model associated with this model + * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const { + virtual std::vector<Type>* checkInstantaneousReward(storm::formula::InstantaneousReward<Type> const& 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."); @@ -280,13 +290,17 @@ public: } /*! - * The check method for a path formula with a Cumulative Reward operator node as root in its - * formula tree + * Check the given formula that is a cumulative reward formula. * - * @param formula The Cumulative Reward formula to check - * @returns for each state the reward that the cumulative reward yields + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bound 0. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bound 0. + * @returns The reward values for the given formula for every state of the model associated with this model + * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const { + virtual std::vector<Type>* checkCumulativeReward(storm::formula::CumulativeReward<Type> const& 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."); @@ -304,8 +318,15 @@ public: totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector()); } - std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector()); + // Initialize result to either the state rewards of the model or the null vector. + std::vector<Type>* result = nullptr; + if (this->getModel().hasStateRewards()) { + result = new std::vector<Type>(*this->getModel().getStateRewardVector()); + } else { + result = new std::vector<Type>(this->getModel().getNumberOfStates()); + } + // Perform the actual matrix-vector multiplication as long as the bound of the formula is met. this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound()); // Delete temporary variables and return result. @@ -314,13 +335,17 @@ public: } /*! - * The check method for a path formula with a Reachability Reward operator node as root in its - * formula tree + * Checks the given formula that is a reachability reward formula. * - * @param formula The Reachbility Reward formula to check - * @returns for each state the reward that the reachability reward yields + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bound 0. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bound 0. + * @returns The reward values for the given formula for every state of the model associated with this model + * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const { + virtual std::vector<Type>* checkReachabilityReward(storm::formula::ReachabilityReward<Type> const& 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"); @@ -380,6 +405,7 @@ public: storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getStateRewardVector()); } + // Now solve the resulting equation system. this->solveEquationSystem(*submatrix, x, b); // Set values of resulting vector according to result. @@ -399,13 +425,33 @@ public: } private: + /*! + * Performs (repeated) matrix-vector multiplication with the given parameters. + * + * @param matrix The matrix that is to be multiplied against the vector. + * @param vector The initial vector that is to be multiplied against the matrix. This is also the output parameter, + * i.e. after the method returns, this vector will contain the computed values. + * @param summand If not null, this vector is being added to the result after each matrix-vector multplication. + * @param repetitions Specifies the number of iterations the matrix-vector multiplication is performed. + * @returns The result of the repeated matrix-vector multiplication as the content of the parameter vector. + */ virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const = 0; - virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type> const& b) const = 0; + + /*! + * Solves the equation system A*x = b given by the parameters. + * + * @param A The matrix specifying the coefficients of the linear eqations. + * @param x The solution vector x. The initial values of x represent a guess of the real values to the solver, but + * may be ignored. + * @param b The right-hand side of the equation system. + * @returns The solution vector x of the system of linear equations as the content of the parameter x. + */ + virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const = 0; }; } //namespace modelChecker } //namespace storm -#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ +#endif /* STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ */