From 2f5f8c0918ca5a1b33bccfe7739fc7c59b7749e6 Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 30 Apr 2014 22:31:10 +0200 Subject: [PATCH] PrctlFilter is operational but not yet complete (proper standard output missing). - General function of the filters: The filter as an abstraction layer between the control flow and the formula/modelchecker. |- It has a formula as child but is not a formula itself. |- It invokes the modelchecking process on the child formula and manipulates the result. |- For the purpose of result manipulation it keeps a list of filter actions. |- Each action manipulates the result in a certain way. For example: It returns only the results for states 25 to 140. |- Furthermore the printing of the result to standard out and the log is no longer done by the modelchecker but by the filter. |- That way the tasks of each class becomes more clear: Modelchecker to compute the results, filter to prepare the computed results for write out. - Battled with a major design problem: How to integrate the optimizing operator (aka. min or max probs for non-det. models) into the filter scheme. |- It is now integrated as a separate filter action, which does not touch the results but hold the flag determining whether to maximize or to minimize. |- This action must be the innermost filter action (i.e. the first list entry) to have any effect. |- This is combined with a special fuction of the modelchecker that manipulates the mutable minimizationStack calculates the modelchecking result and resets the stack to its original state. |- This way the information whether to min, to max or not to try is managed by the filter and propagated as needed. |- Remark: Fixed a major risk of undefined behavior in the SparseMdpPrctlModelChecker. |- If the formula to be checked did not have a NoBoundFormula as root then the minimumOperatorStack would be empty and minimumOperatorStack.top() would result in undefined behavior. |- Added tests whether the stack is empty before trying to read out the possibly non existant top element. Next up: Implement similar filters for LTL and CSL and try to get it compiled. Former-commit-id: 577998e02775bf5775d7fea094192dbed76d197a --- src/formula/Actions/Action.h | 13 ++- src/formula/Actions/MinMaxAction.h | 60 ++++++++++ src/formula/Actions/RangeAction.h | 7 ++ src/formula/Prctl/PrctlFilter.h | 85 ++++++++++++-- src/modelchecker/prctl/AbstractModelChecker.h | 104 +++++++----------- .../prctl/SparseDtmcPrctlModelChecker.h | 51 ++++++--- .../prctl/SparseMdpPrctlModelChecker.h | 79 ++++++++----- 7 files changed, 281 insertions(+), 118 deletions(-) create mode 100644 src/formula/Actions/MinMaxAction.h diff --git a/src/formula/Actions/Action.h b/src/formula/Actions/Action.h index f435859b9..dd7bd3502 100644 --- a/src/formula/Actions/Action.h +++ b/src/formula/Actions/Action.h @@ -31,17 +31,26 @@ public: /*! * */ - virtual std::vector evaluate(std::vector input) const = 0; + virtual std::vector evaluate(std::vector input) const { + return input; + } /*! * */ - virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const = 0; + virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const { + return input; + } /*! * */ virtual std::string toString() const = 0; + + /*! + * + */ + virtual std::string toFormulaString() const = 0; }; } //namespace action diff --git a/src/formula/Actions/MinMaxAction.h b/src/formula/Actions/MinMaxAction.h new file mode 100644 index 000000000..2c32bd964 --- /dev/null +++ b/src/formula/Actions/MinMaxAction.h @@ -0,0 +1,60 @@ +/* + * MinMaxAction.h + * + * Created on: Apr 30, 2014 + * Author: Manuel Sascha Weiand + */ + +#ifndef STORM_FORMULA_ACTION_MINMAXACTION_H_ +#define STORM_FORMULA_ACTION_MINMAXACTION_H_ + +#include "src/formula/Actions/Action.h" + +namespace storm { +namespace property { +namespace action { + +template +class MinMaxAction : Action { + +public: + + MinMaxAction() : minimize(true) { + //Intentionally left empty. + } + + explicit MinMaxAction(bool minimize) : minimize(minimize) { + //Intentionally left empty. + } + + /*! + * + */ + virtual std::string toString() const override { + return minimize ? "min" : "max"; + } + + /*! + * + */ + virtual std::string toFormulaString() const override { + return minimize ? "min" : "max"; + } + + /*! + * + */ + bool getMinimize() { + return minimize; + } + +private: + bool minimize; + +}; + +} //namespace action +} //namespace property +} //namespace storm + +#endif /* STORM_FORMULA_ACTION_MINMAXACTION_H_ */ diff --git a/src/formula/Actions/RangeAction.h b/src/formula/Actions/RangeAction.h index 183ad6a13..58a44aa0e 100644 --- a/src/formula/Actions/RangeAction.h +++ b/src/formula/Actions/RangeAction.h @@ -61,6 +61,13 @@ public: return "range, " + from + ", " + to; } + /*! + * + */ + virtual std::string toFormulaString() const override { + return "\"range\", " + from + ", " + to; + } + private: uint_fast64_t from; uint_fast64_t to; diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/Prctl/PrctlFilter.h index 5cf154e6f..f01c0b4b9 100644 --- a/src/formula/Prctl/PrctlFilter.h +++ b/src/formula/Prctl/PrctlFilter.h @@ -43,21 +43,77 @@ public: delete child; } - void check(AbstractModelChecker& modelchecker) const { + void check(AbstractModelChecker const & modelchecker) const { + + // Write out the formula to be checked. + std::cout << std::endl; + LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toFormulaString()); + std::cout << "Model checking formula:\t" << this->toFormulaString() << std::endl; // Do a dynamic cast to test for the actual formula type and call the correct evaluation function. if(dynamic_cast*>(child) != nullptr) { + // Check the formula and apply the filter actions. - storm::storage::BitVector result = evaluate(modelchecker, static_cast*>(child)); + storm::storage::BitVector result; + + try { + result = evaluate(modelchecker, static_cast*>(child)); + } 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."); + std::cout << std::endl << "-------------------------------------------" << std::endl; + + return; + } // Now write out the result. + if(actions.empty()) { + + // There is no filter action given. So provide legacy support: + // Return the results for all states labeled with "init". + LOG4CPLUS_INFO(logger, "Result for initial states:"); + std::cout << "Result for initial states:" << std::endl; + for (auto initialState : modelchecker.getModel>().getInitialStates()) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); + std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; + } + } + + std::cout << std::endl << "-------------------------------------------" << std::endl; + } else if (dynamic_cast*>(child) != nullptr) { + // Check the formula and apply the filter actions. - std::vector result = evaluate(modelchecker, static_cast*>(child)); + std::vector result; + + try { + result = evaluate(modelchecker, static_cast*>(child)); + } 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."); + std::cout << std::endl << "-------------------------------------------" << std::endl; + + return; + } // Now write out the result. + + if(actions.empty()) { + + // There is no filter action given. So provide legacy support: + // Return the results for all states labeled with "init". + LOG4CPLUS_INFO(logger, "Result for initial states:"); + std::cout << "Result for initial states:" << std::endl; + for (auto initialState : modelchecker.getModel>().getInitialStates()) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]); + std::cout << "\t" << initialState << ": " << result[initialState] << std::endl; + } + } + + std::cout << std::endl << "-------------------------------------------" << std::endl; + } else { // This branch should be unreachable. If you ended up here, something strange has happened. @@ -108,9 +164,17 @@ public: private: - BitVector evaluate(AbstractModelChecker& modelchecker, AbstractStateFormula* formula) const { + BitVector evaluate(AbstractModelChecker const & modelchecker, AbstractStateFormula* formula) const { // First, get the model checking result. - BitVector result = formula->check(modelchecker); + BitVector result = modelchecker.checkMinMaxOperator(formula); + + if(getActionCount() != 0 && dynamic_cast*>(getAction(0)) != nullptr) { + // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. + result = modelchecker.checkMinMaxOperator(formula, static_cast*>(getAction(0))->getMinimize()); + } else { + result = formula->check(modelchecker); + } + // Now apply all filter actions and return the result. for(auto action : actions) { @@ -119,9 +183,16 @@ private: return result; } - std::vector evaluate(AbstractModelChecker& modelchecker, AbstractPathFormula* formula) const { + std::vector evaluate(AbstractModelChecker const & modelchecker, AbstractPathFormula* formula) const { // First, get the model checking result. - std::vector result = formula->check(modelchecker); + std::vector result; + + if(getActionCount() != 0 && dynamic_cast*>(getAction(0)) != nullptr) { + // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. + result = modelchecker.checkMinMaxOperator(formula, static_cast*>(getAction(0))->getMinimize()); + } else { + result = formula->check(modelchecker, false); + } // Now apply all filter actions and return the result. for(auto action : actions) { diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 888721a56..cbf5830e4 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -17,6 +17,7 @@ namespace prctl { } } +#include #include "src/exceptions/InvalidPropertyException.h" #include "src/formula/Prctl.h" #include "src/storage/BitVector.h" @@ -119,73 +120,6 @@ public: throw bc; } } - - /*! - * Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula) - * for all initial states, i.e. states that carry the atomic proposition "init". - * - * @param formula The formula to be checked. - */ - void check(storm::property::prctl::AbstractPrctlFormula const& formula) const { - if (dynamic_cast const*>(&formula) != nullptr) { - this->check(static_cast const&>(formula)); - } else if (dynamic_cast const*>(&formula) != nullptr) { - this->check(static_cast const&>(formula)); - } - } - - /*! - * 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(storm::property::prctl::AbstractStateFormula 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; - storm::storage::BitVector result; - try { - result = stateFormula.check(*this); - LOG4CPLUS_INFO(logger, "Result for initial states:"); - std::cout << "Result for initial states:" << std::endl; - for (auto initialState : model.getInitialStates()) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); - std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; - } - } 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."); - } - - std::cout << std::endl << "-------------------------------------------" << std::endl; - } - - /*! - * 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(storm::property::prctl::AbstractNoBoundOperator 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; - std::vector result; - try { - result = this->checkNoBoundOperator(noBoundFormula); - LOG4CPLUS_INFO(logger, "Result for initial states:"); - std::cout << "Result for initial states:" << std::endl; - for (auto initialState : model.getInitialStates()) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]); - std::cout << "\t" << initialState << ": " << result[initialState] << std::endl; - } - } 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."); - } - std::cout << std::endl << "-------------------------------------------" << std::endl; - } /*! * Checks the given formula consisting of a single atomic proposition. @@ -295,6 +229,42 @@ public: return result; } + /*! + * Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula. + * + * @param formula The formula to check. + * @param minimumOperator True iff minimum probabilities/rewards are to be computed. + * @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector. + */ + virtual std::vector checkMinMaxOperator(storm::property::prctl::AbstractPathFormula const & formula, bool minimumOperator) const { + minimumOperatorStack.push(minimumOperator); + std::vector result = formula.check(*this, false); + minimumOperatorStack.pop(); + return result; + } + + /*! + * Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula. + * + * @param formula The formula to check. + * @param minimumOperator True iff minimum probabilities/rewards are to be computed. + * @returns The set of states satisfying the formula represented by a bit vector. + */ + virtual std::vector checkMinMaxOperator(storm::property::prctl::AbstractStateFormula const & formula, bool minimumOperator) const { + minimumOperatorStack.push(minimumOperator); + std::vector result = formula.check(*this); + minimumOperatorStack.pop(); + return result; + } + +protected: + + /*! + * A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively. + * The topmost element is true if and only if we are currently computing minimum probabilities or rewards. + */ + mutable std::stack minimumOperatorStack; + private: /*! diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 2f03603d8..40994ce78 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -60,21 +60,6 @@ public: return AbstractModelChecker::template getModel>(); } - /*! - * Checks the given formula that is a P/R operator without a bound. - * - * @param formula The formula to check. - * @returns The set of states satisfying the formula represented by a bit vector. - */ - std::vector checkNoBoundOperator(storm::property::prctl::AbstractNoBoundOperator 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."); - } - return formula.check(*this, false); - } - - /*! * Checks the given formula that is a bounded-until formula. * @@ -497,6 +482,42 @@ public: return result; } + /*! + * Checks the given formula. + * @note This methods overrides the method of the base class to give an additional warning that declaring that minimal or maximal probabilities + * should be computed for the formula makes no sense in the context of a deterministic model. + * + * @param formula The formula to check. + * @param minimumOperator True iff minimum probabilities/rewards are to be computed. + * @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector. + */ + virtual std::vector checkMinMaxOperator(storm::property::prctl::AbstractPathFormula const & formula, bool minimumOperator) const override { + + LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); + + std::vector result = formula.check(*this, false); + + return result; + } + + /*! + * Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula. + * @note This methods overrides the method of the base class to give an additional warning that declaring that minimal or maximal probabilities + * should be computed for the formula makes no sense in the context of a deterministic model. + * + * @param formula The formula to check. + * @param minimumOperator True iff minimum probabilities/rewards are to be computed. + * @returns The set of states satisfying the formula represented by a bit vector. + */ + virtual std::vector checkMinMaxOperator(storm::property::prctl::AbstractStateFormula const & formula, bool minimumOperator) const override { + + LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); + + std::vector result = formula.check(*this); + + return result; + } + private: // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolver; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 868f78722..1a34b1f3d 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -55,6 +55,13 @@ namespace storm { // Intentionally left empty. } + /*! + * Virtual destructor. Needs to be virtual, because this class has virtual methods. + */ + virtual ~SparseMdpPrctlModelChecker() { + // Intentionally left empty. + } + /*! * Returns a constant reference to the MDP associated with this model checker. * @returns A constant reference to the MDP associated with this model checker. @@ -62,25 +69,7 @@ namespace storm { storm::models::Mdp const& getModel() const { return AbstractModelChecker::template getModel>(); } - - /*! - * Checks the given formula that is a P/R operator without a bound. - * - * @param formula The formula to check. - * @returns The set of states satisfying the formula represented by a bit vector. - */ - virtual std::vector checkNoBoundOperator(const storm::property::prctl::AbstractNoBoundOperator& formula) const { - // Check if the operator was an non-optimality operator and report an error in that case. - if (!formula.isOptimalityOperator()) { - LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); - 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.check(*this, false); - minimumOperatorStack.pop(); - return result; - } - + /*! * Computes the probability to satisfy phi until psi within a limited number of steps for each state. * @@ -95,7 +84,13 @@ namespace storm { * If the qualitative flag is set, exact probabilities might not be computed. */ std::vector checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const { - std::vector result(this->getModel().getNumberOfStates()); + // First test if it is specified if the minimum or maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; + } + + std::vector result(this->getModel().getNumberOfStates()); // Determine the states that have 0 probability of reaching the target states. storm::storage::BitVector statesWithProbabilityGreater0; @@ -166,6 +161,12 @@ namespace storm { * qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkNext(storm::storage::BitVector const& nextStates, bool qualitative) const { + // First test if it is specified if the minimum or maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; + } + // Create the vector with which to multiply and initialize it correctly. std::vector result(this->getModel().getNumberOfStates()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constantOne()); @@ -260,6 +261,12 @@ namespace storm { * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkUntil(const storm::property::prctl::Until& formula, bool qualitative) const { + // First test if it is specified if the minimum or maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; + } + return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft().check(*this), formula.getRight().check(*this), qualitative).first; } @@ -365,6 +372,12 @@ namespace storm { throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; } + // Now test whether it is specified if the minimum or maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; + } + // Initialize result to state rewards of the model. std::vector result(this->getModel().getStateRewardVector()); @@ -391,6 +404,12 @@ namespace storm { throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; } + // Now test whether it is specified if the minimum or maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; + } + // Compute the reward vector to add in each step based on the available reward models. std::vector totalRewardVector; if (this->getModel().hasTransitionRewards()) { @@ -427,6 +446,12 @@ namespace storm { * checker. If the qualitative flag is set, exact values might not be computed. */ virtual std::vector checkReachabilityReward(const storm::property::prctl::ReachabilityReward& formula, bool qualitative) const { + // First test whether it is specified if the minimum or maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; + } + return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild().check(*this), qualitative).first; } @@ -452,6 +477,12 @@ namespace storm { throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; } + // Also test whether it is specified if the minimum or maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; + } + // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); @@ -570,13 +601,7 @@ namespace storm { return storm::storage::TotalScheduler(choices); } - - /*! - * A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively. - * The topmost element is true if and only if we are currently computing minimum probabilities or rewards. - */ - mutable std::stack minimumOperatorStack; - + /*! * A solver that is used for solving systems of linear equations that are the result of nondeterministic choices. */