From a6f20400dfd707a3b8045883899a0e3de91b739f Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 7 May 2014 22:00:18 +0200 Subject: [PATCH] Added similar filters for Ltl and Csl. - Fixed similar undefined behavior for the MarkovAutomaton Csl modelchecker. Next up: Make necessary changes to the formula parsers. Former-commit-id: e8765fe58be01788fda3ff7d97c3eefd7fcdb3d2 --- src/formula/Csl/CslFilter.h | 211 ++++++++++++++++++ src/formula/Ltl/LtlFilter.h | 138 ++++++++++++ src/formula/Prctl/PrctlFilter.h | 10 +- src/modelchecker/csl/AbstractModelChecker.h | 108 ++++----- .../SparseMarkovAutomatonCslModelChecker.h | 51 +++-- src/modelchecker/ltl/AbstractModelChecker.h | 26 --- src/modelchecker/prctl/AbstractModelChecker.h | 8 +- .../prctl/SparseDtmcPrctlModelChecker.h | 4 +- .../prctl/SparseMdpPrctlModelChecker.h | 7 +- 9 files changed, 428 insertions(+), 135 deletions(-) create mode 100644 src/formula/Csl/CslFilter.h create mode 100644 src/formula/Ltl/LtlFilter.h diff --git a/src/formula/Csl/CslFilter.h b/src/formula/Csl/CslFilter.h new file mode 100644 index 000000000..db59a59a7 --- /dev/null +++ b/src/formula/Csl/CslFilter.h @@ -0,0 +1,211 @@ +/* + * CslFilter.h + * + * Created on: May 7, 2014 + * Author: Manuel Sascha Weiand + */ + +#ifndef STORM_FORMULA_PRCTL_CSLFILTER_H_ +#define STORM_FORMULA_PRCTL_CSLFILTER_H_ + +#include "src/formula/AbstractFilter.h" +#include "src/formula/Csl/AbstractCslFormula.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/Csl/AbstractStateFormula.h" + +namespace storm { +namespace property { +namespace csl { + +template +class CslFilter : storm::property::AbstractFilter { + +public: + + CslFilter() : child(nullptr) { + // Intentionally left empty. + } + + CslFilter(AbstractCslFormula* child) : child(child) { + // Intentionally left empty. + } + + CslFilter(AbstractCslFormula* child, action::Action* action) : child(child) { + actions.push_back(action); + } + + CslFilter(AbstractCslFormula* child, std::vector*> actions) : child(child), actions(actions) { + // Intentionally left empty. + } + + virtual ~CslFilter() { + actions.clear(); + delete child; + } + + 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; + + 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; + + 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. + //TODO: Error here. + } + } + + bool validate() const { + // Test whether the stored filter actions are consistent in relation to themselves and to the ingoing modelchecking result. + + // Do a dynamic cast to test for the actual formula type. + if(dynamic_cast*>(child) != nullptr) { + //TODO: Actual validation. + } + else if (dynamic_cast*>(child) != nullptr) { + //TODO: Actual validation. + } + else { + // This branch should be unreachable. If you ended up here, something strange has happened. + //TODO: Error here. + } + + return true; + } + + std::string toFormulaString() const { + std::string desc = "filter("; + return desc; + } + + std::string toString() const { + std::string desc = "Filter: "; + desc += "\nActions:"; + for(auto action : actions) { + desc += "\n\t" + action.toString(); + } + desc += "\nFormula:\n\t" + child->toString(); + return desc; + } + + void setChild(AbstractCslFormula* child) { + this->child = child; + } + + AbstractFormula* getChild() const { + return child; + } + +private: + + BitVector evaluate(AbstractModelChecker const & modelchecker, AbstractStateFormula* formula) const { + // First, get the model checking result. + 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) { + result = action->evaluate(result); + } + return result; + } + + std::vector evaluate(AbstractModelChecker const & modelchecker, AbstractPathFormula* formula) const { + // First, get the model checking result. + 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) { + result = action->evaluate(result); + } + return result; + } + + AbstractCslFormula* child; +}; + +} //namespace csl +} //namespace property +} //namespace storm + +#endif /* STORM_FORMULA_CSL_CSLFILTER_H_ */ diff --git a/src/formula/Ltl/LtlFilter.h b/src/formula/Ltl/LtlFilter.h new file mode 100644 index 000000000..6fbb6398e --- /dev/null +++ b/src/formula/Ltl/LtlFilter.h @@ -0,0 +1,138 @@ +/* + * LtlFilter.h + * + * Created on: May 7, 2014 + * Author: Manuel Sascha Weiand + */ + +#ifndef STORM_FORMULA_LTL_LTLFILTER_H_ +#define STORM_FORMULA_LTL_LTLFILTER_H_ + +namespace storm { +namespace property { +namespace ltl { + +template +class LtlFilter : storm::property::AbstractFilter { + +public: + + LtlFilter() : child(nullptr) { + // Intentionally left empty. + } + + LtlFilter(AbstractLtlFormula* child) : child(child) { + // Intentionally left empty. + } + + LtlFilter(AbstractLtlFormula* child, action::Action* action) : child(child) { + actions.push_back(action); + } + + LtlFilter(AbstractLtlFormula* child, std::vector*> actions) : child(child), actions(actions) { + // Intentionally left empty. + } + + virtual ~LtlFilter() { + actions.clear(); + delete child; + } + + + /*!Description copied from the MC. + * 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(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; + + + // Check the formula and apply the filter actions. + storm::storage::BitVector result; + + try { + result = evaluate(modelchecker, 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; + } + + bool validate() const { + // Test whether the stored filter actions are consistent in relation to themselves and to the ingoing modelchecking result. + + //TODO: Actual validation. + + return true; + } + + std::string toFormulaString() const { + std::string desc = "filter("; + return desc; + } + + std::string toString() const { + std::string desc = "Filter: "; + desc += "\nActions:"; + for(auto action : actions) { + desc += "\n\t" + action.toString(); + } + desc += "\nFormula:\n\t" + child->toString(); + return desc; + } + + void setChild(AbstractLtlFormula* child) { + this->child = child; + } + + AbstractFormula* getChild() const { + return child; + } + +private: + + storm::storage::BitVector evaluate(AbstractModelChecker const & modelchecker, AbstractLtlFormula* formula) const { + // First, get the model checking result. + storm::storage::BitVector result = formula->check(modelchecker); + + // Now apply all filter actions and return the result. + for(auto action : actions) { + result = action->evaluate(result); + } + return result; + } + + AbstractLtlFormula* child; +}; + + +} //namespace ltl +} //namespace property +} //namespace storm + +#endif /* STORM_FORMULA_LTL_LTLFILTER_H_ */ diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/Prctl/PrctlFilter.h index f01c0b4b9..9af9dc39a 100644 --- a/src/formula/Prctl/PrctlFilter.h +++ b/src/formula/Prctl/PrctlFilter.h @@ -26,15 +26,15 @@ public: // Intentionally left empty. } - PrctlFilter(AbstractFormula* child) : child(child) { + PrctlFilter(AbstractPrctlFormula* child) : child(child) { // Intentionally left empty. } - PrctlFilter(AbstractFormula* child, action::Action* action) : child(child) { + PrctlFilter(AbstractPrctlFormula* child, action::Action* action) : child(child) { actions.push_back(action); } - PrctlFilter(AbstractFormula* child, std::vector*> actions) : child(child), actions(actions) { + PrctlFilter(AbstractPrctlFormula* child, std::vector*> actions) : child(child), actions(actions) { // Intentionally left empty. } @@ -154,7 +154,7 @@ public: return desc; } - void setChild(AbstractFormula* child) { + void setChild(AbstractPrctlFormula* child) { this->child = child; } @@ -164,7 +164,7 @@ public: private: - BitVector evaluate(AbstractModelChecker const & modelchecker, AbstractStateFormula* formula) const { + BitVector evaluate(AbstractModelChecker const & modelchecker, AbstractStateFormula* formula) const { // First, get the model checking result. BitVector result = modelchecker.checkMinMaxOperator(formula); diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h index 36499884a..a80b39445 100644 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ b/src/modelchecker/csl/AbstractModelChecker.h @@ -8,6 +8,7 @@ #ifndef STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ #define STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ +#include #include "src/exceptions/InvalidPropertyException.h" #include "src/formula/Csl.h" #include "src/storage/BitVector.h" @@ -52,14 +53,14 @@ public: /*! * Constructs an AbstractModelChecker with the given model. */ - explicit AbstractModelChecker(storm::models::AbstractModel const& model) : model(model) { + explicit AbstractModelChecker(storm::models::AbstractModel const& model) : minimumOperatorStack(), model(model) { // Intentionally left empty. } /*! * 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 const& modelchecker) : model(modelchecker.model) { + explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : minimumOperatorStack(), model(modelchecker.model) { // Intentionally left empty. } @@ -105,71 +106,6 @@ public: } } - /*! - * 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::csl::AbstractCslFormula 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::csl::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::csl::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; - } - std::cout << std::endl << "-------------------------------------------" << std::endl; - } - /*! * Checks the given formula consisting of a single atomic proposition. * @@ -254,6 +190,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::csl::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 storm::storage::BitVector checkMinMaxOperator(storm::property::csl::AbstractStateFormula const & formula, bool minimumOperator) const { + minimumOperatorStack.push(minimumOperator); + storm::storage::BitVector 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: /*! @@ -269,4 +241,4 @@ private: } // namespace modelchecker } // namespace storm -#endif /* STORM_MODELCHECKER_CSL_DTMCPRCTLMODELCHECKER_H_ */ +#endif /* STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ */ diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index a4cd0844a..629e809af 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -1,7 +1,6 @@ #ifndef STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ #define STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ -#include #include #include "src/modelchecker/csl/AbstractModelChecker.h" @@ -22,7 +21,7 @@ namespace storm { template class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker { public: - explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton const& model, std::shared_ptr> nondeterministicLinearEquationSolver) : AbstractModelChecker(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { + explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton const& model, std::shared_ptr> nondeterministicLinearEquationSolver) : AbstractModelChecker(model), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { // Intentionally left empty. } @@ -30,7 +29,7 @@ namespace storm { This Second constructor is NEEDED and a workaround for a common Bug in C++ with nested templates See: http://stackoverflow.com/questions/14401308/visual-c-cannot-deduce-given-template-arguments-for-function-used-as-defaul */ - explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton const& model) : AbstractModelChecker(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver()) { + explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton const& model) : AbstractModelChecker(model), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver()) { // Intentionally left empty. } @@ -43,9 +42,15 @@ namespace storm { } std::vector checkUntil(storm::property::csl::Until const& formula, bool qualitative) const { - storm::storage::BitVector leftStates = formula.getLeft().check(*this); + // 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."; + } + + storm::storage::BitVector leftStates = formula.getLeft().check(*this); storm::storage::BitVector rightStates = formula.getRight().check(*this); - return computeUnboundedUntilProbabilities(minimumOperatorStack.top(), leftStates, rightStates, qualitative).first; + return computeUnboundedUntilProbabilities(this->minimumOperatorStack.top(), leftStates, rightStates, qualitative).first; } std::pair, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool min, storm::storage::BitVector const& leftStates, storm::storage::BitVector const& rightStates, bool qualitative) const { @@ -57,7 +62,13 @@ namespace storm { } std::vector checkTimeBoundedEventually(storm::property::csl::TimeBoundedEventually const& formula, bool qualitative) const { - storm::storage::BitVector goalStates = formula.getChild().check(*this); + // 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."; + } + + storm::storage::BitVector goalStates = formula.getChild().check(*this); return this->checkTimeBoundedEventually(this->minimumOperatorStack.top(), goalStates, formula.getLowerBound(), formula.getUpperBound()); } @@ -66,26 +77,20 @@ namespace storm { } std::vector checkEventually(storm::property::csl::Eventually const& formula, bool qualitative) const { - storm::storage::BitVector subFormulaStates = formula.getChild().check(*this); - return computeUnboundedUntilProbabilities(minimumOperatorStack.top(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), subFormulaStates, qualitative).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."; + } + + storm::storage::BitVector subFormulaStates = formula.getChild().check(*this); + return computeUnboundedUntilProbabilities(this->minimumOperatorStack.top(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), subFormulaStates, qualitative).first; } std::vector checkNext(storm::property::csl::Next const& formula, bool qualitative) const { throw storm::exceptions::NotImplementedException() << "Model checking Next formulas on Markov automata is not yet implemented."; } - std::vector checkNoBoundOperator(storm::property::csl::AbstractNoBoundOperator const& 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 for nondeterministic models."); - throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful for nondeterministic models."; - } - minimumOperatorStack.push(formula.isMinimumOperator()); - std::vector result = formula.check(*this, false); - minimumOperatorStack.pop(); - return result; - } - static void computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps) { // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. @@ -580,12 +585,6 @@ namespace storm { return result; } - /*! - * 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. */ diff --git a/src/modelchecker/ltl/AbstractModelChecker.h b/src/modelchecker/ltl/AbstractModelChecker.h index 8cc06cdbd..03284fed6 100644 --- a/src/modelchecker/ltl/AbstractModelChecker.h +++ b/src/modelchecker/ltl/AbstractModelChecker.h @@ -104,32 +104,6 @@ public: } } - /*! - * 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::ltl::AbstractLtlFormula const& ltlFormula) const { - std::cout << std::endl; - LOG4CPLUS_INFO(logger, "Model checking formula\t" << ltlFormula.toString()); - std::cout << "Model checking formula:\t" << ltlFormula.toString() << std::endl; - storm::storage::BitVector result; - try { - result = ltlFormula.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 consisting of a single atomic proposition. * diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index cbf5830e4..5eaa14f80 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -67,14 +67,14 @@ public: /*! * Constructs an AbstractModelChecker with the given model. */ - explicit AbstractModelChecker(storm::models::AbstractModel const& model) : model(model){ + explicit AbstractModelChecker(storm::models::AbstractModel const& model) : minimumOperatorStack(), model(model) { // Intentionally left empty. } /*! * 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 const& modelchecker) : model(modelchecker.model) { + explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : minimumOperatorStack(), model(modelchecker.model) { // Intentionally left empty. } @@ -250,9 +250,9 @@ public: * @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 { + virtual storm::storage::BitVector checkMinMaxOperator(storm::property::prctl::AbstractStateFormula const & formula, bool minimumOperator) const { minimumOperatorStack.push(minimumOperator); - std::vector result = formula.check(*this); + storm::storage::BitVector result = formula.check(*this); minimumOperatorStack.pop(); return result; } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 40994ce78..ba61201c7 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -509,11 +509,11 @@ public: * @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 { + virtual storm::storage::BitVector 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); + storm::storage::BitVector result = formula.check(*this); return result; } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 1a34b1f3d..7a9c7c29c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -9,7 +9,6 @@ #define STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_ #include -#include #include #include "src/modelchecker/prctl/AbstractModelChecker.h" @@ -38,11 +37,11 @@ namespace storm { * * @param model The MDP to be checked. */ - explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model) : AbstractModelChecker(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver()) { + explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model) : AbstractModelChecker(model), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver()) { // Intentionally left empty. } - explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model, std::shared_ptr> nondeterministicLinearEquationSolver) : AbstractModelChecker(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { + explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model, std::shared_ptr> nondeterministicLinearEquationSolver) : AbstractModelChecker(model), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { // Intentionally left empty. } @@ -51,7 +50,7 @@ namespace storm { * constructed model checker will have the model of the given model checker as its associated model. */ explicit SparseMdpPrctlModelChecker(storm::modelchecker::prctl::SparseMdpPrctlModelChecker const& modelchecker) - : AbstractModelChecker(modelchecker), minimumOperatorStack(), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver()) { + : AbstractModelChecker(modelchecker), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver()) { // Intentionally left empty. }