diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 516166fd0..a4c8707c7 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -988,35 +988,35 @@ namespace storm { static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp const& labeledMdp, std::shared_ptr> const & formulaPtr) { std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl; // First, we need to check whether the current formula is an Until-Formula. - storm::property::prctl::ProbabilisticBoundOperator const* probBoundFormula = dynamic_cast const*>(formulaPtr); + auto probBoundFormula = std::dynamic_pointer_cast>(formulaPtr); if (probBoundFormula == nullptr) { LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."; } - if (probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS_EQUAL) { + if (probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS_EQUAL) { LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."; } - bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::property::ComparisonType::LESS); + bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS); // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape. double bound = probBoundFormula->getBound(); - storm::property::prctl::AbstractPathFormula const& pathFormula = probBoundFormula->getPathFormula(); + std::shared_ptr> pathFormula = probBoundFormula->getChild(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); try { - storm::property::prctl::Until const& untilFormula = dynamic_cast const&>(pathFormula); + auto untilFormula = std::dynamic_pointer_cast>(pathFormula); - phiStates = untilFormula.getLeft().check(modelchecker); - psiStates = untilFormula.getRight().check(modelchecker); + phiStates = untilFormula->getLeft()->check(modelchecker); + psiStates = untilFormula->getRight()->check(modelchecker); } catch (std::bad_cast const&) { // If the nested formula was not an until formula, it remains to check whether it's an eventually formula. try { - storm::property::prctl::Eventually const& eventuallyFormula = dynamic_cast const&>(pathFormula); + auto eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); - psiStates = eventuallyFormula.getChild().check(modelchecker); + psiStates = eventuallyFormula->getChild()->check(modelchecker); } catch (std::bad_cast const&) { // If the nested formula is neither an until nor a finally formula, we throw an exception. throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation."; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index dbcf4d8b1..9b77821c2 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,14 @@ 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. + } + + /*! + * Virtual destructor. Needs to be virtual, because this class has virtual methods. + */ + virtual ~SparseMarkovAutomatonCslModelChecker() { // Intentionally left empty. } @@ -42,50 +48,89 @@ namespace storm { return AbstractModelChecker::template getModel>(); } - std::vector checkUntil(storm::property::csl::Until const& formula, bool qualitative) const { - storm::storage::BitVector leftStates = formula.getLeft().check(*this); - storm::storage::BitVector rightStates = formula.getRight().check(*this); - return computeUnboundedUntilProbabilities(minimumOperatorStack.top(), leftStates, rightStates, qualitative).first; + /*! + * Checks the given formula that is a P operator over a path formula featuring a value bound. + * + * @param formula The formula to check. + * @returns The set of states satisfying the formula represented by a bit vector. + */ + virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::csl::ProbabilisticBoundOperator const& formula) const override{ + // For P< and P<= the MA satisfies the formula iff the probability maximizing scheduler is used. + // For P> and P>= " iff the probability minimizing " . + if(formula.getComparisonOperator() == storm::properties::LESS || formula.getComparisonOperator() == storm::properties::LESS_EQUAL) { + this->minimumOperatorStack.push(false); + } + else { + this->minimumOperatorStack.push(true); + } + + // First, we need to compute the probability for satisfying the path formula for each state. + std::vector quantitativeResult = formula.getChild()->check(*this, false); + + //Remove the minimizing operator entry from the stack. + this->minimumOperatorStack.pop(); + + // Create resulting bit vector that will hold the yes/no-answer for every state. + storm::storage::BitVector result(quantitativeResult.size()); + + // Now, we can compute which states meet the bound specified in this operator and set the + // corresponding bits to true in the resulting vector. + for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) { + if (formula.meetsBound(quantitativeResult[i])) { + result.set(i, true); + } + } + + return result; + } + + std::vector checkUntil(storm::properties::csl::Until const& formula, bool qualitative) const { + // Test wheter it is specified if the minimum or the maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify either min or max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify either min or 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(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 { return storm::modelchecker::prctl::SparseMdpPrctlModelChecker::computeUnboundedUntilProbabilities(min, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), leftStates, rightStates, nondeterministicLinearEquationSolver, qualitative); } - std::vector checkTimeBoundedUntil(storm::property::csl::TimeBoundedUntil const& formula, bool qualitative) const { + std::vector checkTimeBoundedUntil(storm::properties::csl::TimeBoundedUntil const& formula, bool qualitative) const { throw storm::exceptions::NotImplementedException() << "Model checking Until formulas on Markov automata is not yet implemented."; } - std::vector checkTimeBoundedEventually(storm::property::csl::TimeBoundedEventually const& formula, bool qualitative) const { - storm::storage::BitVector goalStates = formula.getChild().check(*this); + std::vector checkTimeBoundedEventually(storm::properties::csl::TimeBoundedEventually const& formula, bool qualitative) const { + // Test wheter it is specified if the minimum or the maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify either min or max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify either min or 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()); } - std::vector checkGlobally(storm::property::csl::Globally const& formula, bool qualitative) const { + std::vector checkGlobally(storm::properties::csl::Globally const& formula, bool qualitative) const { throw storm::exceptions::NotImplementedException() << "Model checking Globally formulas on Markov automata is not yet implemented."; } - 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; + std::vector checkEventually(storm::properties::csl::Eventually const& formula, bool qualitative) const { + // Test wheter it is specified if the minimum or the maximum probabilities are to be computed. + if(this->minimumOperatorStack.empty()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify either min or max optimality, which is not meaningful over nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify either min or 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 { + std::vector checkNext(storm::properties::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 +625,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/solver/GurobiLpSolver.h b/src/solver/GurobiLpSolver.h index 90bef47eb..f078ef6dd 100644 --- a/src/solver/GurobiLpSolver.h +++ b/src/solver/GurobiLpSolver.h @@ -176,7 +176,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } - virtual uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { + virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index b60cbdc16..46eaa0860 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -13,6 +13,8 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" +#include + // Forward declaration for adapter classes. namespace storm { namespace adapters {