From 8d3f633cbcda856a36898b44a07d0ce5cd19bc9c Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 6 Jan 2017 17:40:40 +0100 Subject: [PATCH] started working on allowing expressions in time-bounds of formulas --- src/storm/logic/BoundedUntilFormula.cpp | 118 ++++++++++++++---- src/storm/logic/BoundedUntilFormula.h | 49 ++++++-- src/storm/logic/CloneVisitor.cpp | 6 +- src/storm/logic/FragmentChecker.cpp | 2 +- .../csl/HybridCtmcCslModelChecker.cpp | 15 ++- .../csl/SparseCtmcCslModelChecker.cpp | 15 ++- .../SparseMarkovAutomatonCslModelChecker.cpp | 15 ++- .../pcaa/SparsePcaaPreprocessor.cpp | 24 ++-- .../prctl/HybridDtmcPrctlModelChecker.cpp | 5 +- .../prctl/HybridMdpPrctlModelChecker.cpp | 5 +- .../prctl/SparseDtmcPrctlModelChecker.cpp | 5 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 4 +- .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 5 +- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 5 +- .../SparseDtmcEliminationModelChecker.cpp | 7 +- src/storm/parser/FormulaParserGrammar.cpp | 34 ++--- src/storm/parser/FormulaParserGrammar.h | 10 +- src/storm/parser/JaniParser.cpp | 4 +- 18 files changed, 229 insertions(+), 99 deletions(-) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index f75854d77..97734340e 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -5,19 +5,12 @@ #include "storm/logic/FormulaVisitor.h" +#include "storm/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, double lowerBound, double upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(std::make_pair(lowerBound, upperBound)) { - STORM_LOG_THROW(lowerBound >= 0 && upperBound >= 0, storm::exceptions::InvalidArgumentException, "Bounded until formula requires non-negative time bounds."); - STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::InvalidArgumentException, "Lower bound of bounded until formula is required to be smaller than the upper bound."); - } - - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, uint_fast64_t upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(upperBound) { - // Intentionally left empty. - } - - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::variant> const& bounds) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(bounds) { - // Intentionally left empty. + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, BoundedType const& boundedType) : BinaryPathFormula(leftSubformula, rightSubformula), lowerBound(lowerBound), upperBound(upperBound), boundedType(boundedType) { + STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); } bool BoundedUntilFormula::isBoundedUntilFormula() const { @@ -31,28 +24,109 @@ namespace storm { boost::any BoundedUntilFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } + + bool BoundedUntilFormula::isStepBounded() const { + return boundedType == BoundedType::Steps; + } + + bool BoundedUntilFormula::isTimeBounded() const { + return boundedType == BoundedType::Time; + } + + bool BoundedUntilFormula::isLowerBoundStrict() const { + return lowerBound.get().isStrict(); + } + + bool BoundedUntilFormula::hasLowerBound() const { + return static_cast(lowerBound); + } + + bool BoundedUntilFormula::hasIntegerLowerBound() const { + return lowerBound.get().getBound().hasIntegerType(); + } + + bool BoundedUntilFormula::isUpperBoundStrict() const { + return upperBound.get().isStrict(); + } + + bool BoundedUntilFormula::hasUpperBound() const { + return static_cast(upperBound); + } + + bool BoundedUntilFormula::hasIntegerUpperBound() const { + return upperBound.get().getBound().hasIntegerType(); + } - bool BoundedUntilFormula::hasDiscreteTimeBound() const { - return bounds.which() == 0; + storm::expressions::Expression const& BoundedUntilFormula::getLowerBound() const { + return lowerBound.get().getBound(); } - - std::pair const& BoundedUntilFormula::getIntervalBounds() const { - return boost::get>(bounds); + + storm::expressions::Expression const& BoundedUntilFormula::getUpperBound() const { + return upperBound.get().getBound(); + } + + template <> + double BoundedUntilFormula::getLowerBound() const { + double bound = this->getLowerBound().evaluateAsDouble(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + double BoundedUntilFormula::getUpperBound() const { + double bound = this->getUpperBound().evaluateAsDouble(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + uint64_t BoundedUntilFormula::getLowerBound() const { + int_fast64_t bound = this->getLowerBound().evaluateAsInt(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return static_cast(bound); } - uint_fast64_t BoundedUntilFormula::getDiscreteTimeBound() const { - return boost::get(bounds); + template <> + uint64_t BoundedUntilFormula::getUpperBound() const { + int_fast64_t bound = this->getUpperBound().evaluateAsInt(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return static_cast(bound); } std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const { this->getLeftSubformula().writeToStream(out); out << " U"; - if (!this->hasDiscreteTimeBound()) { - std::pair const& intervalBounds = getIntervalBounds(); - out << "[" << intervalBounds.first << "," << intervalBounds.second << "] "; + if (this->hasLowerBound()) { + if (this->hasUpperBound()) { + if (this->isLowerBoundStrict()) { + out << "("; + } else { + out << "["; + } + out << this->getLowerBound(); + out << ", "; + out << this->getUpperBound(); + if (this->isUpperBoundStrict()) { + out << ")"; + } else { + out << "]"; + } + } else { + if (this->isLowerBoundStrict()) { + out << ">"; + } else { + out << ">="; + } + out << getLowerBound(); + } } else { - out << "<=" << getDiscreteTimeBound() << " "; + if (this->isUpperBoundStrict()) { + out << "<"; + } else { + out << "<="; + } + out << this->getUpperBound(); } this->getRightSubformula().writeToStream(out); diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 97f0fdbae..6780061f8 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -1,17 +1,32 @@ #ifndef STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ #define STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ -#include +#include #include "storm/logic/BinaryPathFormula.h" namespace storm { namespace logic { + class UntilBound { + public: + UntilBound(bool strict, storm::expressions::Expression bound); + + storm::expressions::Expression const& getBound() const; + bool isStrict() const; + + private: + bool strict; + storm::expressions::Expression bound; + }; + class BoundedUntilFormula : public BinaryPathFormula { public: - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, double lowerBound, double upperBound); - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, uint_fast64_t upperBound); - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::variant> const& bounds); + enum class BoundedType { + Steps, + Time + }; + + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, BoundedType const& boundedType = BoundedType::Time); virtual bool isBoundedUntilFormula() const override; @@ -19,15 +34,33 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; - bool hasDiscreteTimeBound() const; + bool isStepBounded() const; + bool isTimeBounded() const; - std::pair const& getIntervalBounds() const; - uint_fast64_t getDiscreteTimeBound() const; + bool isLowerBoundStrict() const; + bool hasLowerBound() const; + bool hasIntegerLowerBound() const; + + bool isUpperBoundStrict() const; + bool hasUpperBound() const; + bool hasIntegerUpperBound() const; + + storm::expressions::Expression const& getLowerBound() const; + storm::expressions::Expression const& getUpperBound() const; + + template + ValueType getLowerBound() const; + + template + ValueType getUpperBound() const; virtual std::ostream& writeToStream(std::ostream& out) const override; private: - boost::variant> bounds; + BoundedType boundedType; + + boost::optional lowerBound; + boost::optional upperBound; }; } } diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index adb6c4cb3..e19d9477d 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -31,11 +31,7 @@ namespace storm { boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); - if (f.hasDiscreteTimeBound()) { - return std::static_pointer_cast(std::make_shared(left, right, f.getDiscreteTimeBound())); - } else { - return std::static_pointer_cast(std::make_shared(left, right, f.getIntervalBounds())); - } + return std::static_pointer_cast(std::make_shared(f)); } boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 3dc27fe5f..c47b8ea5d 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -58,7 +58,7 @@ namespace storm { result = result && !f.getLeftSubformula().isPathFormula(); result = result && !f.getRightSubformula().isPathFormula(); } - if (f.hasDiscreteTimeBound()) { + if (f.isStepBounded()) { result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed(); } else { result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed(); diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index ca07fbc07..21f73b0b7 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -12,6 +12,8 @@ #include "storm/logic/FragmentSpecification.h" +#include "storm/exceptions/NotImplementedException.h" + namespace storm { namespace modelchecker { template @@ -67,14 +69,17 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + + STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; - if (!pathFormula.hasDiscreteTimeBound()) { - std::pair const& intervalBounds = pathFormula.getIntervalBounds(); - lowerBound = intervalBounds.first; - upperBound = intervalBounds.second; + if (pathFormula.hasLowerBound()) { + lowerBound = pathFormula.getLowerBound(); + } + if (pathFormula.hasUpperBound()) { + upperBound = pathFormula.getUpperBound(); } else { - upperBound = pathFormula.getDiscreteTimeBound(); + upperBound = storm::utility::infinity(); } return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 22aa11c1e..ca224b1a3 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -59,16 +59,19 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; - if (!pathFormula.hasDiscreteTimeBound()) { - std::pair const& intervalBounds = pathFormula.getIntervalBounds(); - lowerBound = intervalBounds.first; - upperBound = intervalBounds.second; + if (pathFormula.hasLowerBound()) { + lowerBound = pathFormula.getLowerBound(); + } + if (pathFormula.hasUpperBound()) { + upperBound = pathFormula.getUpperBound(); } else { - upperBound = pathFormula.getDiscreteTimeBound(); + upperBound = storm::utility::infinity(); } - + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index cb5275abc..4aef07d8d 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -53,16 +53,19 @@ namespace storm { STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported."); double lowerBound = 0; double upperBound = 0; - if (!pathFormula.hasDiscreteTimeBound()) { - std::pair const& intervalBounds = pathFormula.getIntervalBounds(); - lowerBound = intervalBounds.first; - upperBound = intervalBounds.second; + if (pathFormula.hasLowerBound()) { + lowerBound = pathFormula.getLowerBound(); + } + if (pathFormula.hasUpperBound()) { + upperBound = pathFormula.getUpperBound(); } else { - upperBound = pathFormula.getDiscreteTimeBound(); + upperBound = storm::utility::infinity(); } - + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index c1dcf8c09..daef0687c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -224,22 +224,20 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support step-bounded properties for Markov automata."); - if(formula.hasDiscreteTimeBound()) { - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getDiscreteTimeBound()); + if (formula.hasLowerBound()) { + STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula."); + currentObjective.lowerTimeBound = formula.getLowerBound(); + } + if (formula.hasUpperBound()) { + STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula."); + currentObjective.upperTimeBound = formula.getUpperBound(); } else { - if(result.originalModel.isOfType(storm::models::ModelType::Mdp)) { - STORM_LOG_THROW(formula.getIntervalBounds().first == std::round(formula.getIntervalBounds().first), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete lower time bound but got " << formula << "."); - STORM_LOG_THROW(formula.getIntervalBounds().second == std::round(formula.getIntervalBounds().second), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete upper time bound but got " << formula << "."); - } else { - STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula which can not be checked for the current model type."); - STORM_LOG_THROW(formula.getIntervalBounds().second > formula.getIntervalBounds().first, storm::exceptions::InvalidPropertyException, "Neither empty nor point intervalls are allowed but got " << formula << "."); - } - if(!storm::utility::isZero(formula.getIntervalBounds().first)) { - currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getIntervalBounds().first); - } - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getIntervalBounds().second); + currentObjective.upperTimeBound = storm::utility::infinity(); } + STORM_LOG_THROW(currentObjective.lowerTimeBound < currentObjective.upperTimeBound, storm::exceptions::InvalidPropertyException, "Empty or point time intervals are currently not supported by multi-objective model checking."); + preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); } diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 0b5b6ea0f..723c2ca1b 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -70,12 +70,13 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 2e6b0d5fb..6ef453636 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -68,12 +68,13 @@ namespace storm { std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index d063817be..509a8db06 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -42,12 +42,13 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *linearEquationSolverFactory); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); return result; } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 2f82bf57c..637380920 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -58,11 +58,13 @@ namespace storm { std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 389584275..7f32c666d 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -70,12 +70,13 @@ namespace storm { template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index dadfe5ce5..55b5f4539 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -70,12 +70,13 @@ namespace storm { std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 854a6f51d..010fe8b23 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -323,6 +323,9 @@ namespace storm { std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -331,7 +334,7 @@ namespace storm { // Start by determining the states that have a non-zero probability of reaching the target states within the // time bound. - storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, pathFormula.getDiscreteTimeBound()); + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, pathFormula.getUpperBound()); statesWithProbabilityGreater0 &= ~psiStates; // Determine whether we need to perform some further computation. @@ -350,7 +353,7 @@ namespace storm { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); if (furtherComputationNeeded) { - uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound(); + uint_fast64_t timeBound = pathFormula.getUpperBound(); if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 2ee1861a7..d30f29f94 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -66,7 +66,7 @@ namespace storm { conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; conditionalFormula.name("conditional formula"); - timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1]; + timeBound = (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_1, qi::_2)] | ((qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)]; timeBound.name("time bound"); pathFormula = conditionalFormula(qi::_r1); @@ -167,6 +167,20 @@ namespace storm { this->identifiers_.add(identifier, expression); } + std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const { + storm::logic::UntilBound lower(false, lowerBound); + storm::logic::UntilBound upper(false, upperBound); + return std::make_pair(lower, upper); + } + + std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const { + if (upperBound) { + return std::make_pair(boost::none, storm::logic::UntilBound(strict, bound)); + } else { + return std::make_pair(storm::logic::UntilBound(strict, bound), boost::none); + } + } + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { if (timeBound.which() == 0) { return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); @@ -208,14 +222,9 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { - if (timeBound.get().which() == 0) { - std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second)); - } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); - } + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time)); } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -229,14 +238,9 @@ namespace storm { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { - if (timeBound.get().which() == 0) { - std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second)); - } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(boost::get(timeBound.get())))); - } + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time)); } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 21989d97d..affbd96b0 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -148,7 +148,8 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - qi::rule, uint_fast64_t>(), Skipper> timeBound; + + qi::rule>(), qi::locals, Skipper> timeBound; qi::rule(), Skipper> rewardPathFormula; qi::rule(), Skipper> cumulativeRewardFormula; @@ -160,6 +161,9 @@ namespace storm { // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; + + std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const; + std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const; // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; @@ -169,10 +173,10 @@ namespace storm { std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 0d36b6201..06b0a83c2 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -345,7 +345,7 @@ namespace storm { upperBound--; } STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative"); - return std::make_shared(args[0], args[1], upperBound); + return std::make_shared(args[0], args[1], std::make_pair(pi.lowerBound, !pi.lowerBoundStrict), std::make_pair(pi.upperBound, !pi.upperBoundStrict), storm::logic::BoundedUntilFormula::BoundedType::Steps); } else if (propertyStructure.count("time-bounds") > 0) { storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds")); STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); @@ -356,7 +356,7 @@ namespace storm { double upperBound = pi.upperBound.evaluateAsDouble(); STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); - return std::make_shared(args[0], args[1], upperBound); + return std::make_shared(args[0], args[1], std::make_pair(pi.lowerBound, !pi.lowerBoundStrict), std::make_pair(pi.upperBound, !pi.upperBoundStrict), storm::logic::BoundedUntilFormula::BoundedType::Time); } else if (propertyStructure.count("reward-bounds") > 0 ) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");