diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 694ab7265..32fa4c5a5 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -38,9 +38,9 @@ ExternalProject_Add( #TIMEOUT 10 DOWNLOAD_COMMAND "" SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/gtest-1.7.0" - # Force separate output paths for debug and release builds to allow easy - # identification of correct lib in subsequent TARGET_LINK_LIBRARIES - CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} + # Force the same output paths for debug and release builds so that + # we know in which place the binaries end up when using the Xcode generator + CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 # Disable install step INSTALL_COMMAND "" BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0" diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 17825b23d..87f02c668 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -923,7 +923,6 @@ namespace storm { } public: - static boost::container::flat_set getMinimalLabelSet(storm::logic::Formula const& pathFormula, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabeling()) { @@ -934,7 +933,7 @@ namespace storm { double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { storm::modelchecker::helper::SparseMdpPrctlHelper modelcheckerHelper; - std::vector result = std::move(modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).result); + std::vector result = std::move(modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).values); for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -986,7 +985,7 @@ namespace storm { STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); bool strictBound = comparisonType == storm::logic::ComparisonType::Less; - double bound = probabilityOperator.getBound(); + double threshold = probabilityOperator.getThreshold(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; @@ -1016,7 +1015,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet()); + boost::container::flat_set usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 7c85f7644..3f03440d3 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1628,7 +1628,7 @@ namespace storm { if (checkThresholdFeasible) { storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).result); + std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).values); for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -1692,7 +1692,7 @@ namespace storm { storm::models::sparse::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).result); + std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).values); LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; @@ -1763,7 +1763,7 @@ namespace storm { STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); bool strictBound = comparisonType == storm::logic::ComparisonType::Less; - double bound = probabilityOperator.getBound(); + double threshold = probabilityOperator.getThreshold(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; @@ -1793,7 +1793,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet()); + auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/logic/Bound.h b/src/logic/Bound.h new file mode 100644 index 000000000..d0a98853c --- /dev/null +++ b/src/logic/Bound.h @@ -0,0 +1,33 @@ +#ifndef STORM_LOGIC_BOUND_H_ +#define STORM_LOGIC_BOUND_H_ + +#include "src/logic/ComparisonType.h" + +namespace storm { + namespace logic { + template + struct Bound { + Bound(ComparisonType comparisonType, ValueType const& threshold) : comparisonType(comparisonType), threshold(threshold) { + // Intentionally left empty. + } + + ComparisonType comparisonType; + ValueType threshold; + + template + friend std::ostream& operator<<(std::ostream& out, Bound const& bound); + }; + + template + std::ostream& operator<<(std::ostream& out, Bound const& bound) { + out << bound.comparisonType << bound.threshold; + return out; + } + } + + template + using Bound = typename logic::Bound; +} + +#endif /* STORM_LOGIC_BOUND_H_ */ + diff --git a/src/logic/BoundInfo.h b/src/logic/BoundInfo.h deleted file mode 100644 index 453d9eb08..000000000 --- a/src/logic/BoundInfo.h +++ /dev/null @@ -1,19 +0,0 @@ - -#ifndef BOUNDINFO_H -#define BOUNDINFO_H - -#include "ComparisonType.h" - - -namespace storm { - namespace logic { - template - struct BoundInfo { - BT bound; - ComparisonType boundType; - }; - } -} - -#endif /* BOUNDINFO_H */ - diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp index 98ed6d8cc..ed21be228 100644 --- a/src/logic/ExpectedTimeOperatorFormula.cpp +++ b/src/logic/ExpectedTimeOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -34,12 +34,12 @@ namespace storm { return this->getSubformula().containsNestedProbabilityOperators(); } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr ExpectedTimeOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h index b9b6d57ee..5702610c2 100644 --- a/src/logic/ExpectedTimeOperatorFormula.h +++ b/src/logic/ExpectedTimeOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class ExpectedTimeOperatorFormula : public OperatorFormula { public: ExpectedTimeOperatorFormula(std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~ExpectedTimeOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp index d72317b7d..cfeb30692 100644 --- a/src/logic/LongRunAverageOperatorFormula.cpp +++ b/src/logic/LongRunAverageOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -34,12 +34,12 @@ namespace storm { return this->getSubformula().containsNestedProbabilityOperators(); } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr LongRunAverageOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h index 161823314..89e119f48 100644 --- a/src/logic/LongRunAverageOperatorFormula.h +++ b/src/logic/LongRunAverageOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class LongRunAverageOperatorFormula : public OperatorFormula { public: LongRunAverageOperatorFormula(std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~LongRunAverageOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 768b6b3d0..a9cdc09ae 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) { + OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), bound(bound), optimalityType(optimalityType) { // Intentionally left empty. } @@ -11,19 +11,27 @@ namespace storm { } ComparisonType OperatorFormula::getComparisonType() const { - return comparisonType.get(); + return bound.get().comparisonType; } - void OperatorFormula::setComparisonType(ComparisonType t) { - comparisonType = boost::optional(t); + void OperatorFormula::setComparisonType(ComparisonType newComparisonType) { + bound.get().comparisonType = newComparisonType; } - double OperatorFormula::getBound() const { + double OperatorFormula::getThreshold() const { + return bound.get().threshold; + } + + void OperatorFormula::setThreshold(double newThreshold) { + bound.get().threshold = newThreshold; + } + + Bound const& OperatorFormula::getBound() const { return bound.get(); } - void OperatorFormula::setBound(double b) { - bound = boost::optional(b); + void OperatorFormula::setBound(Bound const& newBound) { + bound = newBound; } bool OperatorFormula::hasOptimalityType() const { @@ -43,7 +51,7 @@ namespace storm { out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max"); } if (hasBound()) { - out << getComparisonType() << getBound(); + out << getBound(); } else { out << "=?"; } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 5c120bf2f..7660799a4 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -4,14 +4,14 @@ #include #include "src/logic/UnaryStateFormula.h" +#include "src/logic/Bound.h" #include "src/solver/OptimizationDirection.h" -#include "src/logic/ComparisonType.h" namespace storm { namespace logic { class OperatorFormula : public UnaryStateFormula { public: - OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~OperatorFormula() { // Intentionally left empty. @@ -19,20 +19,21 @@ namespace storm { bool hasBound() const; ComparisonType getComparisonType() const; - void setComparisonType(ComparisonType); - double getBound() const; - void setBound(double); + void setComparisonType(ComparisonType newComparisonType); + double getThreshold() const; + void setThreshold(double newThreshold); + Bound const& getBound() const; + void setBound(Bound const& newBound); bool hasOptimalityType() const; - OptimizationDirection const& getOptimalityType() const; + storm::solver::OptimizationDirection const& getOptimalityType() const; virtual bool isOperatorFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; protected: std::string operatorSymbol; - boost::optional comparisonType; - boost::optional bound; - boost::optional optimalityType; + boost::optional> bound; + boost::optional optimalityType; }; } } diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index e6cde140d..1f4615556 100644 --- a/src/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -42,12 +42,12 @@ namespace storm { return this->getSubformula().containsProbabilityOperator(); } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr ProbabilityOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index 7f30dd92d..8bae11548 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class ProbabilityOperatorFormula : public OperatorFormula { public: ProbabilityOperatorFormula(std::shared_ptr const& subformula); - ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~ProbabilityOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 627263d36..791d1f5cc 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, bound, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -55,12 +55,12 @@ namespace storm { this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula), rewardModelName(rewardModelName) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula), rewardModelName(rewardModelName) { // Intentionally left empty. } std::shared_ptr RewardOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->rewardModelName, this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->rewardModelName, this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index 37287c6e8..9e90ef01f 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -9,10 +9,10 @@ namespace storm { class RewardOperatorFormula : public OperatorFormula { public: RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~RewardOperatorFormula() { // Intentionally left empty. diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 764b02427..3b0d55ebf 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -175,7 +175,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThreshold()); } else { return result; } @@ -189,7 +189,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } @@ -203,7 +203,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } @@ -217,7 +217,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index cf66f4f06..be56e29e1 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -30,7 +30,7 @@ namespace storm { */ CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) { this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; - this->produceStrategies = true; + this->produceSchedulers = false; this->qualitative = false; if (formula.isOperatorFormula()) { @@ -41,7 +41,7 @@ namespace storm { if (operatorFormula.hasBound()) { if (onlyInitialStatesRelevant) { - this->bound = std::make_pair(operatorFormula.getComparisonType(), static_cast(operatorFormula.getBound())); + this->bound = operatorFormula.getBound(); } if (!optimizationDirection) { @@ -54,7 +54,7 @@ namespace storm { storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); if (probabilityOperatorFormula.hasBound()) { - if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { + if (probabilityOperatorFormula.getThreshold() == storm::utility::zero() || probabilityOperatorFormula.getThreshold() == storm::utility::one()) { this->qualitative = true; } } @@ -63,7 +63,7 @@ namespace storm { this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); if (rewardOperatorFormula.hasBound()) { - if (rewardOperatorFormula.getBound() == storm::utility::zero()) { + if (rewardOperatorFormula.getThreshold() == storm::utility::zero()) { this->qualitative = true; } } @@ -76,7 +76,7 @@ namespace storm { */ template CheckTask replaceFormula(NewFormulaType const& newFormula) const { - return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceStrategies); + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers); } /*! @@ -139,21 +139,21 @@ namespace storm { /*! * Retrieves the value of the bound (if set). */ - ValueType const& getBoundValue() const { - return bound.get().second; + ValueType const& getBoundThreshold() const { + return bound.get().threshold; } /*! * Retrieves the comparison type of the bound (if set). */ storm::logic::ComparisonType const& getBoundComparisonType() const { - return bound.get().first; + return bound.get().comparisonType; } /*! - * Retrieves the bound for the initial states (if set). + * Retrieves the bound (if set). */ - std::pair const& getBound() const { + storm::logic::Bound const& getBound() const { return bound.get(); } @@ -166,10 +166,17 @@ namespace storm { } /*! - * Retrieves whether strategies are to be produced (if supported). + * Sets whether to produce schedulers (if supported). */ - bool isProduceStrategiesSet() const { - return produceStrategies; + void setProduceSchedulers(bool produceSchedulers) { + this->produceSchedulers = produceSchedulers; + } + + /*! + * Retrieves whether scheduler(s) are to be produced (if supported). + */ + bool isProduceSchedulersSet() const { + return produceSchedulers; } private: @@ -181,14 +188,13 @@ namespace storm { * @param rewardModelName If given, the checking has to be done wrt. to this reward model. * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values * for the initial states. - * @param initialStatesBound The bound with which the initial states will be compared. This may only be set - * together with the flag that indicates only initial states of the model are relevant. + * @param bound The bound with which the states will be compared. * @param qualitative A flag specifying whether the property needs to be checked qualitatively, i.e. compared * with bounds 0/1. - * @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve + * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceStrategies(produceStrategies) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { // Intentionally left empty. } @@ -204,15 +210,15 @@ namespace storm { // If set to true, the model checker may decide to only compute the values for the initial states. bool onlyInitialStatesRelevant; - // The bound with which the initial states will be compared. - boost::optional> bound; + // The bound with which the states will be compared. + boost::optional> bound; // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. bool qualitative; - // If supported by the model checker and the model formalism, strategies to achieve a value will be produced + // If supported by the model checker and the model formalism, schedulers to achieve a value will be produced // if this flag is set. - bool produceStrategies; + bool produceSchedulers; }; } diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index fac6e5864..d926917a5 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -184,7 +184,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - return std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, false, minMaxLinearEquationSolverFactory).result); + return std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values); } template diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index eb4025551..710d926a7 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -87,8 +87,12 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), false, *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; } template diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 340b5f33a..1a0d85b2c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,8 +4,6 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/models/sparse/Mdp.h" #include "src/utility/solver.h" -#include "src/logic/BoundInfo.h" -#include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { namespace modelchecker { diff --git a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h index a68a5889e..4ce7bb23f 100644 --- a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h +++ b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h @@ -3,42 +3,38 @@ #include #include -#include "src/storage/PartialScheduler.h" +#include "src/storage/Scheduler.h" namespace storm { namespace storage { class BitVector; } - namespace modelchecker { - - namespace helper { template struct MDPSparseModelCheckingHelperReturnType { + MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete; MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default; - explicit MDPSparseModelCheckingHelperReturnType(std::vector && res) : result(std::move(res)) - { - + MDPSparseModelCheckingHelperReturnType(std::vector&& values, std::unique_ptr&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { + // Intentionally left empty. } - MDPSparseModelCheckingHelperReturnType(std::vector && res, std::unique_ptr && pSched) : - result(std::move(res)), partScheduler(std::move(pSched)) {} - - virtual ~MDPSparseModelCheckingHelperReturnType() { } + virtual ~MDPSparseModelCheckingHelperReturnType() { + // Intentionally left empty. + } + // The values computed for the states. + std::vector values; - std::vector result; - std::unique_ptr partScheduler; + // A scheduler, if it was computed. + std::unique_ptr scheduler; }; } - + } } - #endif /* MDPMODELCHECKINGRETURNTYPE_H */ - diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 2f4d9389d..adec586dd 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1,4 +1,4 @@ -#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" + #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -12,6 +12,7 @@ #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" +#include "src/storage/TotalScheduler.h" #include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/LpSolver.h" @@ -56,7 +57,6 @@ namespace storm { return result; } - template std::vector SparseMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { @@ -73,7 +73,8 @@ namespace storm { template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only."); // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. @@ -96,7 +97,12 @@ namespace storm { // Set values of resulting vector that are known exactly. storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - + + // If requested, we will produce a scheduler. + std::unique_ptr scheduler; + if (produceScheduler) { + scheduler = std::make_unique(transitionMatrix.getRowGroupCount()); + } // Check whether we need to compute exact probabilities for some states. if (qualitative) { @@ -114,31 +120,67 @@ namespace storm { // the accumulated probability of going from state i to some 'yes' state. std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); - // Create vector for results for maybe states. - std::vector x(maybeStates.getNumberOfSetBits()); - - // Solve the corresponding system of equations. - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); - solver->solveEquationSystem(x, b); + MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeUntilProbabilitiesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, x); + storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.values); + + if (produceScheduler) { + storm::storage::Scheduler const& subscheduler = *resultForMaybeStates.scheduler; + uint_fast64_t currentSubState = 0; + for (auto maybeState : maybeStates) { + scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); + ++currentSubState; + } + } } } - return MDPSparseModelCheckingHelperReturnType(std::move(result)); + // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for + // the states with probability 0 or 1 (depending on whether we maximize or minimize). + if (produceScheduler) { + storm::storage::PartialScheduler relevantQualitativeScheduler; + if (goal.minimize()) { + relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb0E(statesWithProbability0, transitionMatrix); + } else { + relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb1E(statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates); + } + for (auto const& stateChoicePair : relevantQualitativeScheduler) { + scheduler->setChoice(stateChoicePair.first, stateChoicePair.second); + } + } + + return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } + template + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // If requested, we will produce a scheduler. + std::unique_ptr scheduler; + + // Create vector for results for maybe states. + std::vector x(submatrix.getRowGroupCount()); + + // Solve the corresponding system of equations. + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); + solver->setTrackScheduler(produceScheduler); + solver->solveEquationSystem(x, b); + + if (produceScheduler) { + scheduler = std::make_unique(std::move(solver->getScheduler())); + } + + return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + } template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { storm::solver::SolveGoal goal(dir); - return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, getPolicy, minMaxLinearEquationSolverFactory)); + return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory)); } template std::vector SparseMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique) { - if (useMecBasedTechnique) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, psiStates); storm::storage::BitVector statesInPsiMecs(transitionMatrix.getRowGroupCount()); @@ -148,9 +190,9 @@ namespace storm { } } - return std::move(computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).result); + return std::move(computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).values); } else { - std::vector result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).result; + std::vector result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values; for (auto& element : result) { element = storm::utility::one() - element; } @@ -519,14 +561,14 @@ namespace storm { initialStatesBitVector.set(initialState); storm::storage::BitVector allStates(initialStatesBitVector.size(), true); - std::vector conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, conditionStates, false, false, minMaxLinearEquationSolverFactory).result); + std::vector conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, conditionStates, false, false, minMaxLinearEquationSolverFactory).values); // If the conditional probability is undefined for the initial state, we return directly. if (storm::utility::isZero(conditionProbabilities[initialState])) { return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::infinity())); } - std::vector targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).result); + std::vector targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).values); storm::storage::BitVector statesWithProbabilityGreater0E(transitionMatrix.getRowGroupCount(), true); storm::storage::sparse::state_type state = 0; @@ -594,7 +636,7 @@ namespace storm { newGoalStates.set(newGoalState); storm::storage::SparseMatrix newTransitionMatrix = builder.build(); storm::storage::SparseMatrix newBackwardTransitions = newTransitionMatrix.transpose(true); - std::vector goalProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).result); + std::vector goalProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).values); return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, dir == OptimizationDirection::Maximize ? goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]] : storm::utility::one() - goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]])); } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 706f61403..0b47759d7 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -36,9 +36,11 @@ namespace storm { static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 3f22b4ff2..08ca016fd 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -79,6 +79,22 @@ namespace storm { } } + template + bool ExplicitQuantitativeCheckResult::hasScheduler() const { + return static_cast(scheduler); + } + + template + void ExplicitQuantitativeCheckResult::setScheduler(std::unique_ptr&& scheduler) { + this->scheduler = std::move(scheduler); + } + + template + storm::storage::Scheduler const& ExplicitQuantitativeCheckResult::getScheduler() const { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return *scheduler.get(); + } + template std::ostream& ExplicitQuantitativeCheckResult::writeToStream(std::ostream& out) const { out << "["; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 9734a176f..ee49b74ec 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -4,9 +4,11 @@ #include #include #include +#include #include "src/modelchecker/results/QuantitativeCheckResult.h" #include "src/storage/sparse/StateType.h" +#include "src/storage/Scheduler.h" #include "src/utility/OsDetection.h" namespace storm { @@ -51,9 +53,16 @@ namespace storm { virtual void oneMinus() override; + bool hasScheduler() const; + void setScheduler(std::unique_ptr&& scheduler); + storm::storage::Scheduler const& getScheduler() const; + private: // The values of the quantitative check result. boost::variant values; + + // An optional scheduler that accompanies the values. + boost::optional> scheduler; }; } } diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index e3c0c9718..c919280b4 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -97,7 +97,7 @@ namespace storm { qi::rule>(), Skipper> start; - qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule, boost::optional>>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule(), Skipper> probabilityOperator; qi::rule(), Skipper> rewardOperator; qi::rule(), Skipper> expectedTimeOperator; @@ -149,10 +149,11 @@ namespace storm { 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 createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; - std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); + std::pair, boost::optional>> createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; + std::shared_ptr createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createExpectedTimeOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); @@ -305,7 +306,7 @@ namespace storm { pathFormula = conditionalFormula; pathFormula.name("path formula"); - operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; + operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -469,20 +470,28 @@ namespace storm { return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::pair, boost::optional>> FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { + if (comparisonType && threshold) { + return std::make_pair(optimizationDirection, storm::logic::Bound(comparisonType.get(), threshold.get())); + } else { + return std::make_pair(optimizationDirection, boost::none); + } + } + + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); } - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, operatorInformation.first, operatorInformation.second, subformula)); } - std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); } - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { - return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); } std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index b2349ebf7..9040f3cf4 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -142,7 +142,7 @@ namespace storm { assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct>()]; assignmentDefinitionList.name("assignment list"); - updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; + updateDefinition = (((expressionParser >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; updateDefinition.name("update"); updateListDefinition %= +updateDefinition(qi::_r1) % "+"; diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index 7059cd1a0..21aa9227c 100644 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ b/src/permissivesched/PermissiveSchedulers.cpp @@ -26,7 +26,7 @@ namespace storm { auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); MilpPermissiveSchedulerComputation> comp(*solver, mdp, goalstates, sinkstates); STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported"); - comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound()); + comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound().threshold); //comp.dumpLpToFile("milpdump.lp"); std::cout << "Found Solution: " << (comp.foundSolution() ? "yes" : "no") << std::endl; if(comp.foundSolution()) { @@ -54,7 +54,7 @@ namespace storm { auto solver = storm::utility::solver::getSmtSolver(*expressionManager); SmtPermissiveSchedulerComputation> comp(*solver, mdp, goalstates, sinkstates); STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported"); - comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound()); + comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound().threshold); if(comp.foundSolution()) { return boost::optional>(comp.getScheduler()); } else { diff --git a/src/solver/AbstractEquationSolver.h b/src/solver/AbstractEquationSolver.h new file mode 100644 index 000000000..904e459bd --- /dev/null +++ b/src/solver/AbstractEquationSolver.h @@ -0,0 +1,53 @@ +#ifndef STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ +#define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ + +#include "src/solver/TerminationCondition.h" + +namespace storm { + namespace solver { + + template + class AbstractEquationSolver { + public: + /*! + * Sets a custom termination condition that is used together with the regular termination condition of the + * solver. + * + * @param terminationCondition An object that can be queried whether to terminate early or not. + */ + void setTerminationCondition(std::unique_ptr> terminationCondition) { + this->terminationCondition = std::move(terminationCondition); + } + + /*! + * Removes a previously set custom termination condition. + */ + void resetTerminationCondition() { + this->terminationCondition = nullptr; + } + + /*! + * Retrieves whether a custom termination condition has been set. + */ + bool hasCustomTerminationCondition() const { + return static_cast(this->terminationCondition); + } + + /*! + * Retrieves the custom termination condition (if any was set). + * + * @return The custom termination condition. + */ + TerminationCondition const& getTerminationCondition() const { + return *terminationCondition; + } + + protected: + // A termination condition to be used (can be unset). + std::unique_ptr> terminationCondition; + }; + + } +} + +#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */ \ No newline at end of file diff --git a/src/solver/AllowEarlyTerminationCondition.cpp b/src/solver/AllowEarlyTerminationCondition.cpp deleted file mode 100644 index 2236c7c78..000000000 --- a/src/solver/AllowEarlyTerminationCondition.cpp +++ /dev/null @@ -1,48 +0,0 @@ -#include "AllowEarlyTerminationCondition.h" -#include "src/utility/vector.h" - -namespace storm { - namespace solver { - - template - TerminateAfterFilteredSumPassesThresholdValue::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold) : - terminationThreshold(threshold), filter(filter) - { - // Intentionally left empty. - } - - template - bool TerminateAfterFilteredSumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { - assert(currentValues.size() >= filter.size()); - ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); - - return currentThreshold >= this->terminationThreshold; - - - } - - template - TerminateAfterFilteredExtremumPassesThresholdValue::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum) : - terminationThreshold(threshold), filter(filter), useMinimumAsExtremum(useMinimum) - { - // Intentionally left empty. - } - - template - bool TerminateAfterFilteredExtremumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { - assert(currentValues.size() >= filter.size()); - - ValueType initVal = terminationThreshold - 1; - ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal); - - return currentThreshold >= this->terminationThreshold; - - - } - - - template class TerminateAfterFilteredExtremumPassesThresholdValue; - template class TerminateAfterFilteredSumPassesThresholdValue; - - } -} diff --git a/src/solver/AllowEarlyTerminationCondition.h b/src/solver/AllowEarlyTerminationCondition.h deleted file mode 100644 index be9084c70..000000000 --- a/src/solver/AllowEarlyTerminationCondition.h +++ /dev/null @@ -1,52 +0,0 @@ -#ifndef ALLOWEARLYTERMINATIONCONDITION_H -#define ALLOWEARLYTERMINATIONCONDITION_H - -#include -#include "src/storage/BitVector.h" - - -namespace storm { - namespace solver { - template - class AllowEarlyTerminationCondition { - public: - virtual bool terminateNow(std::vector const& currentValues) const = 0; - }; - - template - class NoEarlyTerminationCondition : public AllowEarlyTerminationCondition { - public: - bool terminateNow(std::vector const& currentValues) const { return false; } - }; - - template - class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition { - public: - TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold); - bool terminateNow(std::vector const& currentValues) const; - - protected: - ValueType terminationThreshold; - storm::storage::BitVector filter; - }; - - template - class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition{ - public: - TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum); - bool terminateNow(std::vector const& currentValue) const; - - protected: - ValueType terminationThreshold; - storm::storage::BitVector filter; - bool useMinimumAsExtremum; - }; - } -} - - - - - -#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ - diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index ad5729774..3b7bbf476 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -171,7 +171,7 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < maximalNumberOfIterations) { + while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute D^-1 * (b - LU * x) and store result in nextX. gmm::mult(*gmmLU, *currentX, tmpX); gmm::add(b, gmm::scaled(tmpX, -storm::utility::one()), tmpX); diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index e24019e79..07052e6eb 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -5,6 +5,7 @@ #include "src/settings/SettingsManager.h" #include "src/adapters/GmmxxAdapter.h" #include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/storage/TotalScheduler.h" #include "src/utility/vector.h" #include "src/settings/modules/GeneralSettings.h" @@ -14,25 +15,22 @@ namespace storm { namespace solver { template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : - MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), \ - storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative,\ - storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique), - gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { - - + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) : + MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + // Intentionally left empty. } template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackPolicy, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { // Intentionally left empty. } - template void GmmxxMinMaxLinearEquationSolver::solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { if (this->useValueIteration) { - // Set up the environment for the power method. If scratch memory was not provided, we need to create it. + STORM_LOG_THROW(!this->isTrackSchedulerSet(), storm::exceptions::InvalidSettingsException, "Unable to produce a scheduler when using value iteration. Use policy iteration instead."); + + // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(b.size()); @@ -53,7 +51,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult); gmm::add(b, *multiplyResult); @@ -92,7 +90,7 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); + std::vector scheduler(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(rowGroupIndices.size() - 1); @@ -119,13 +117,13 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); submatrix.convertToEquationSystem(); GmmxxLinearEquationSolver gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver::Preconditioner::Ilu, this->relative, 50); - storm::utility::vector::selectVectorValues(subB, this->policy, rowGroupIndices, b); + storm::utility::vector::selectVectorValues(subB, scheduler, rowGroupIndices, b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -139,8 +137,7 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(this->policy)); - + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(scheduler)); // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); @@ -156,6 +153,11 @@ namespace storm { } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } + + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + this->scheduler = std::make_unique(std::move(scheduler)); + } // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.h b/src/solver/GmmxxMinMaxLinearEquationSolver.h index 08432658e..accba556f 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.h +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.h @@ -22,7 +22,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackScheduler = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -33,7 +33,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy = false); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler = false); virtual void performMatrixVectorMultiplication(OptimizationDirection d, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 61f26294e..e85fe3cce 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -3,6 +3,8 @@ #include +#include "src/solver/AbstractEquationSolver.h" + #include "src/storage/SparseMatrix.h" namespace storm { @@ -12,10 +14,9 @@ namespace storm { * An interface that represents an abstract linear equation solver. In addition to solving a system of linear * equations, the functionality to repeatedly multiply a matrix with a given vector is provided. */ - template - class LinearEquationSolver { + template + class LinearEquationSolver : public AbstractEquationSolver { public: - virtual ~LinearEquationSolver() { // Intentionally left empty. } @@ -30,7 +31,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; + virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -44,7 +45,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; }; } // namespace solver diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index f0c2e4869..5041469bc 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -8,9 +8,8 @@ namespace storm { namespace solver { - AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : - precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackPolicy(trackPolicy) - { + template + AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech) : precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackScheduler(trackScheduler) { if(prefTech == MinMaxTechniqueSelection::FROMSETTINGS) { useValueIteration = (storm::settings::generalSettings().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); @@ -19,13 +18,45 @@ namespace storm { } } - void AbstractMinMaxLinearEquationSolver::setPolicyTracking(bool setToTrue) { - trackPolicy = setToTrue; + template + void AbstractMinMaxLinearEquationSolver::setTrackScheduler(bool trackScheduler) { + this->trackScheduler = trackScheduler; } - std::vector AbstractMinMaxLinearEquationSolver::getPolicy() const { - STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!"); - return policy; + template + bool AbstractMinMaxLinearEquationSolver::hasScheduler() const { + return static_cast(scheduler); } + + template + bool AbstractMinMaxLinearEquationSolver::isTrackSchedulerSet() const { + return this->trackScheduler; + } + + template + storm::storage::TotalScheduler const& AbstractMinMaxLinearEquationSolver::getScheduler() const { + STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); + return *scheduler.get(); + } + + template + storm::storage::TotalScheduler& AbstractMinMaxLinearEquationSolver::getScheduler() { + STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); + return *scheduler.get(); + } + + template + void AbstractMinMaxLinearEquationSolver::setOptimizationDirection(OptimizationDirection d) { + direction = convert(d); + } + + template + void AbstractMinMaxLinearEquationSolver::resetOptimizationDirection() { + direction = OptimizationDirectionSetting::Unset; + } + + template class AbstractMinMaxLinearEquationSolver; + template class AbstractMinMaxLinearEquationSolver; + } } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 79d14907b..71ea10ee2 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -4,10 +4,16 @@ #include #include #include -#include "SolverSelectionOptions.h" + +#include + +#include "src/solver/AbstractEquationSolver.h" +#include "src/solver/SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" -#include "AllowEarlyTerminationCondition.h" -#include "OptimizationDirection.h" +#include "src/storage/TotalScheduler.h" +#include "src/solver/OptimizationDirection.h" + +#include "src/exceptions/InvalidSettingsException.h" namespace storm { namespace storage { @@ -15,51 +21,46 @@ namespace storm { } namespace solver { - /** - * Abstract base class which provides value-type independent helpers. + * Abstract base class of min-max linea equation solvers. */ - class AbstractMinMaxLinearEquationSolver { - + template + class AbstractMinMaxLinearEquationSolver : public AbstractEquationSolver { public: - void setPolicyTracking(bool setToTrue=true); - - std::vector getPolicy() const; - - void setOptimizationDirection(OptimizationDirection d) { - direction = convert(d); - } - - void resetOptimizationDirection() { - direction = OptimizationDirectionSetting::Unset; - } + void setTrackScheduler(bool trackScheduler = true); + bool isTrackSchedulerSet() const; + bool hasScheduler() const; + storm::storage::TotalScheduler const& getScheduler() const; + storm::storage::TotalScheduler& getScheduler(); + void setOptimizationDirection(OptimizationDirection d); + void resetOptimizationDirection(); + protected: - AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech); + AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech); - /// The direction in which to optimize, can be unset. + // The direction in which to optimize, can be unset. OptimizationDirectionSetting direction; - - /// The required precision for the iterative methods. + // The required precision for the iterative methods. double precision; - /// Sets whether the relative or absolute error is to be considered for convergence detection. + // Sets whether the relative or absolute error is to be considered for convergence detection. bool relative; - /// The maximal number of iterations to do before iteration is aborted. + // The maximal number of iterations to do before iteration is aborted. uint_fast64_t maximalNumberOfIterations; - /// Whether value iteration or policy iteration is to be used. + // Whether value iteration or policy iteration is to be used. bool useValueIteration; - /// Whether we track the policy we generate. - bool trackPolicy; + // Whether we generate a scheduler during solving. + bool trackScheduler; - /// - mutable std::vector policy; + // The scheduler (if it could be successfully generated). + mutable boost::optional> scheduler; }; /*! @@ -68,16 +69,13 @@ namespace storm { * provided. */ template - class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { + class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { protected: - MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : - AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), - A(matrix), earlyTermination(new NoEarlyTerminationCondition()) { + MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackScheduler, prefTech), A(matrix) { // Intentionally left empty. } public: - virtual ~MinMaxLinearEquationSolver() { // Intentionally left empty. } @@ -107,6 +105,7 @@ namespace storm { assert(isSet(this->direction)); solveEquationSystem(convert(this->direction), x, b, multiplyResult, newX); } + /*! * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes * x[i+1] = min/max(A*x[i] + b) until x[n], where x[0] = x. After each multiplication and addition, the @@ -134,15 +133,8 @@ namespace storm { return performMatrixVectorMultiplication(convert(this->direction), x, b, n, multiplyResult); } - void setEarlyTerminationCriterion(std::unique_ptr> v) { - earlyTermination = std::move(v); - } - - protected: storm::storage::SparseMatrix const& A; - std::unique_ptr> earlyTermination; - }; } // namespace solver diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 414ff1a5e..cb59a2253 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -51,7 +51,7 @@ namespace storm { A.performSuccessiveOverRelaxationStep(omega, x, b); // Now check if the process already converged within our precision. - converged = storm::utility::vector::equalModuloPrecision(x, *tmpX, static_cast(precision), relative); + converged = storm::utility::vector::equalModuloPrecision(x, *tmpX, static_cast(precision), relative) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); // If we did not yet converge, we need to copy the contents of x to *tmpX. if (!converged) { @@ -87,7 +87,7 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < maximalNumberOfIterations) { + while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute D^-1 * (b - LU * x) and store result in nextX. jacobiDecomposition.first.multiplyWithVector(*currentX, tmpX); storm::utility::vector::subtractVectors(b, tmpX, tmpX); diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 1a0881402..22ccf956c 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -2,7 +2,7 @@ #include - +#include "src/storage/TotalScheduler.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/NativeEquationSolverSettings.h" @@ -14,19 +14,12 @@ namespace storm { namespace solver { template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : - MinMaxLinearEquationSolver(A, storm::settings::nativeEquationSolverSettings().getPrecision(), \ - storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, \ - storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique) - { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) : MinMaxLinearEquationSolver(A, storm::settings::nativeEquationSolverSettings().getPrecision(), storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique) { // Intentionally left empty. } template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : - MinMaxLinearEquationSolver(A, precision, \ - relative, \ - maximalNumberOfIterations, trackPolicy, tech) { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech) { // Intentionally left empty. } @@ -53,7 +46,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the // user-specified maximum number of iterations. - while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && (!this->hasCustomTerminationCondition() || this->getTerminationCondition().terminateNow(*currentX))) { // Compute x' = A*x + b. this->A.multiplyWithVector(*currentX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); @@ -93,7 +86,7 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); + std::vector scheduler(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(this->A.getRowGroupIndices().size() - 1); @@ -121,13 +114,13 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); submatrix.convertToEquationSystem(); NativeLinearEquationSolver nativeLinearEquationSolver(submatrix); - storm::utility::vector::selectVectorValues(subB, this->policy, this->A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -141,7 +134,7 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(this->policy)); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(scheduler)); // Determine whether the method converged. @@ -158,8 +151,12 @@ namespace storm { } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } - + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + this->scheduler = std::make_unique(std::move(scheduler)); + } + // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. if (currentX == copyX) { diff --git a/src/solver/NativeMinMaxLinearEquationSolver.h b/src/solver/NativeMinMaxLinearEquationSolver.h index 5fcd76aa9..7920678fa 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.h +++ b/src/solver/NativeMinMaxLinearEquationSolver.h @@ -19,7 +19,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackScheduler = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -30,7 +30,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative = true, bool trackPolicy = false); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative = true, bool trackScheduler = false); virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index f6d109569..642077c05 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -1,36 +1,55 @@ #include "SolveGoal.h" +#include + #include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h" -#include namespace storm { namespace storage { - template class SparseMatrix; + template class SparseMatrix; } namespace solver { - template - std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - std::unique_ptr> p = factory.create(matrix); + template + std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> p = factory.create(matrix); p->setOptimizationDirection(goal.direction()); - p->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.threshold, goal.minimize())); + p->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); return p; } - template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - if(goal.isBounded()) { - return configureMinMaxLinearEquationSolver(static_cast const&>(goal), factory, matrix); + template + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + if (goal.isBounded()) { + return configureMinMaxLinearEquationSolver(static_cast const&>(goal), factory, matrix); } - std::unique_ptr> p = factory.create(matrix); - p->setOptimizationDirection(goal.direction()); - return p; - } + std::unique_ptr> solver = factory.create(matrix); + solver->setOptimizationDirection(goal.direction()); + return solver; + } + + template + std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> solver = factory.create(matrix); + solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.thresholdValue(), goal.boundIsStrict(), goal.minimize())); + return solver; + } + + template + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + if (goal.isBounded()) { + return configureLinearEquationSolver(static_cast const&>(goal), factory, matrix); + } + return factory.create(matrix); + } - template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); } } diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h index fe573dd3a..fb28dfbb3 100644 --- a/src/solver/SolveGoal.h +++ b/src/solver/SolveGoal.h @@ -5,64 +5,107 @@ #include "src/solver/OptimizationDirection.h" #include "src/logic/ComparisonType.h" -#include "src/logic/BoundInfo.h" +#include "src/logic/Bound.h" #include "src/storage/BitVector.h" namespace storm { namespace storage { - template class SparseMatrix; + template class SparseMatrix; } + namespace utility { namespace solver { - template class MinMaxLinearEquationSolverFactory; + template class MinMaxLinearEquationSolverFactory; + template class LinearEquationSolverFactory; } } - namespace solver { - template class MinMaxLinearEquationSolver; + template class MinMaxLinearEquationSolver; + template class LinearEquationSolver; class SolveGoal { public: - SolveGoal(bool minimize) : optDirection(minimize ? OptimizationDirection::Minimize : OptimizationDirection::Maximize) {} - SolveGoal(OptimizationDirection d) : optDirection(d) {} - virtual ~SolveGoal() {} + SolveGoal(bool minimize) : optimizationDirection(minimize ? OptimizationDirection::Minimize : OptimizationDirection::Maximize) { + // Intentionally left empty. + } + + SolveGoal(OptimizationDirection d) : optimizationDirection(d) { + // Intentionally left empty. + } + + virtual ~SolveGoal() { + // Intentionally left empty. + } - bool minimize() const { return optDirection == OptimizationDirection::Minimize; } - OptimizationDirection direction() const { return optDirection; } - virtual bool isBounded() const { return false; } + bool minimize() const { + return optimizationDirection == OptimizationDirection::Minimize; + } + + OptimizationDirection direction() const { + return optimizationDirection; + } + + virtual bool isBounded() const { + return false; + } private: - OptimizationDirection optDirection; - + OptimizationDirection optimizationDirection; }; - - template + template class BoundedGoal : public SolveGoal { public: - BoundedGoal(OptimizationDirection dir, storm::logic::ComparisonType ct, VT const& threshold, storm::storage::BitVector const& relColumns) : SolveGoal(dir), boundType(ct), threshold(threshold), relevantColumnVector(relColumns) {} - BoundedGoal(OptimizationDirection dir, storm::logic::BoundInfo const& bi, storm::storage::BitVector const& relColumns) : SolveGoal(dir), boundType(bi.boundType), threshold(bi.bound), relevantColumnVector(relColumns) {} - virtual ~BoundedGoal() {} + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType comparisonType, ValueType const& threshold, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(comparisonType, threshold), relevantValueVector(relevantValues) { + // Intentionally left empty. + } - bool isBounded() const override { return true; } + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::Bound const& bound, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(bound), relevantValueVector(relevantValues) { + // Intentionally left empty. + } + + virtual ~BoundedGoal() { + // Intentionally left empty. + } + + bool isBounded() const override { + return true; + } bool boundIsALowerBound() const { - return (boundType == storm::logic::ComparisonType::Greater | - boundType == storm::logic::ComparisonType::GreaterEqual); + return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::GreaterEqual); + } + + bool boundIsStrict() const { + return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::Less); + } + + ValueType const& thresholdValue() const { + return bound.threshold; } - VT thresholdValue() const { return threshold; } - storm::storage::BitVector relevantColumns() const { return relevantColumnVector; } - storm::logic::ComparisonType boundType; - VT threshold; - storm::storage::BitVector relevantColumnVector; + storm::storage::BitVector const& relevantValues() const { + return relevantValueVector; + } + + private: + Bound bound; + storm::storage::BitVector relevantValueVector; }; - template - std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template + std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + template + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + template + std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + template + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + } } diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp new file mode 100644 index 000000000..f640ac7e0 --- /dev/null +++ b/src/solver/TerminationCondition.cpp @@ -0,0 +1,41 @@ +#include "src/solver/TerminationCondition.h" +#include "src/utility/vector.h" + +#include "src/utility/macros.h" + +namespace storm { + namespace solver { + + template + bool NoTerminationCondition::terminateNow(std::vector const& currentValues) const { + return false; + } + + template + TerminateIfFilteredSumExceedsThreshold::TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict) : threshold(threshold), filter(filter), strict(strict) { + // Intentionally left empty. + } + + template + bool TerminateIfFilteredSumExceedsThreshold::terminateNow(std::vector const& currentValues) const { + STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch."); + ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); + return strict ? currentThreshold > this->threshold : currentThreshold >= this->threshold; + } + + template + TerminateIfFilteredExtremumExceedsThreshold::TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold(filter, threshold, strict), useMinimum(useMinimum) { + // Intentionally left empty. + } + + template + bool TerminateIfFilteredExtremumExceedsThreshold::terminateNow(std::vector const& currentValues) const { + STORM_LOG_ASSERT(currentValues.size() == this->filter.size(), "Vectors sizes mismatch."); + ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, this->filter) : storm::utility::vector::max_if(currentValues, this->filter); + return this->strict ? currentValue > this->threshold : currentValue >= this->threshold; + } + + template class TerminateIfFilteredSumExceedsThreshold; + template class TerminateIfFilteredExtremumExceedsThreshold; + } +} diff --git a/src/solver/TerminationCondition.h b/src/solver/TerminationCondition.h new file mode 100644 index 000000000..42437bc68 --- /dev/null +++ b/src/solver/TerminationCondition.h @@ -0,0 +1,51 @@ +#ifndef ALLOWEARLYTERMINATIONCONDITION_H +#define ALLOWEARLYTERMINATIONCONDITION_H + +#include +#include "src/storage/BitVector.h" + + +namespace storm { + namespace solver { + template + class TerminationCondition { + public: + virtual bool terminateNow(std::vector const& currentValues) const = 0; + }; + + template + class NoTerminationCondition : public TerminationCondition { + public: + bool terminateNow(std::vector const& currentValues) const; + }; + + template + class TerminateIfFilteredSumExceedsThreshold : public TerminationCondition { + public: + TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict); + bool terminateNow(std::vector const& currentValues) const; + + protected: + ValueType threshold; + storm::storage::BitVector filter; + bool strict; + }; + + template + class TerminateIfFilteredExtremumExceedsThreshold : public TerminateIfFilteredSumExceedsThreshold{ + public: + TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum); + bool terminateNow(std::vector const& currentValue) const; + + protected: + bool useMinimum; + }; + } +} + + + + + +#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ + diff --git a/src/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp index 6f004c315..28076f7a1 100644 --- a/src/storage/PartialScheduler.cpp +++ b/src/storage/PartialScheduler.cpp @@ -22,6 +22,14 @@ namespace storm { return stateChoicePair->second; } + PartialScheduler::map_type::const_iterator PartialScheduler::begin() const { + return stateToChoiceMapping.begin(); + } + + PartialScheduler::map_type::const_iterator PartialScheduler::end() const { + return stateToChoiceMapping.end(); + } + std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) { out << "partial scheduler (defined on " << scheduler.stateToChoiceMapping.size() << " states) [ "; uint_fast64_t remainingEntries = scheduler.stateToChoiceMapping.size(); diff --git a/src/storage/PartialScheduler.h b/src/storage/PartialScheduler.h index e5f9fffb2..4ae503348 100644 --- a/src/storage/PartialScheduler.h +++ b/src/storage/PartialScheduler.h @@ -19,6 +19,9 @@ namespace storm { uint_fast64_t getChoice(uint_fast64_t state) const override; + map_type::const_iterator begin() const; + map_type::const_iterator end() const; + friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler); private: diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp index ae609a4f4..6ae99d212 100644 --- a/src/storage/TotalScheduler.cpp +++ b/src/storage/TotalScheduler.cpp @@ -11,6 +11,10 @@ namespace storm { // Intentionally left empty. } + TotalScheduler::TotalScheduler(std::vector&& choices) : choices(std::move(choices)) { + // Intentionally left empty. + } + void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { if (state > choices.size()) { throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::setChoice: scheduler cannot not define a choice for state " << state << "."; diff --git a/src/storage/TotalScheduler.h b/src/storage/TotalScheduler.h index 32173ac63..6f95edf71 100644 --- a/src/storage/TotalScheduler.h +++ b/src/storage/TotalScheduler.h @@ -25,7 +25,14 @@ namespace storm { * @param choices A vector whose i-th entry defines the choice of state i. */ TotalScheduler(std::vector const& choices); - + + /*! + * Creates a total scheduler that defines the choices for states according to the given vector. + * + * @param choices A vector whose i-th entry defines the choice of state i. + */ + TotalScheduler(std::vector&& choices); + void setChoice(uint_fast64_t state, uint_fast64_t choice) override; bool isChoiceDefined(uint_fast64_t state) const override; diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index bac64948f..0aa8b2836 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -280,7 +280,7 @@ namespace storm { } } if (allSuccessorsInStates) { - result.setChoice(state, choice); + result.setChoice(state, choice - nondeterministicChoiceIndices[state]); break; } } @@ -304,7 +304,7 @@ namespace storm { } } if (oneSuccessorInStates) { - result.setChoice(state, choice); + result.setChoice(state, choice - nondeterministicChoiceIndices[state]); break; } } @@ -356,7 +356,7 @@ namespace storm { // If all successors for a given nondeterministic choice are in the prob1E state set, we // perform a backward search from that state. if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) { - result.setChoice(predecessorEntryIt->getColumn(), row); + result.setChoice(predecessorEntryIt->getColumn(), row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]); currentStates.set(predecessorEntryIt->getColumn(), true); stack.push_back(predecessorEntryIt->getColumn()); break; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 42195cde3..013a800c4 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -91,22 +91,23 @@ namespace storm { } template - void MinMaxLinearEquationSolverFactory::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { + MinMaxLinearEquationSolverFactory& MinMaxLinearEquationSolverFactory::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) { this->solverType = storm::settings::generalSettings().getEquationSolver(); } else { this->solverType = storm::solver::convert(solverTypeSel); } - + return *this; } + template - void MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { + MinMaxLinearEquationSolverFactory& MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { this->prefTech = preferredTech; + return *this; } template - std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackPolicy) const { - + std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackScheduler) const { std::unique_ptr> p1; switch (solverType) { @@ -127,9 +128,8 @@ namespace storm { break; } } - p1->setPolicyTracking(trackPolicy); + p1->setTrackScheduler(trackScheduler); return p1; - } template diff --git a/src/utility/solver.h b/src/utility/solver.h index cf2c63663..ef8120b65 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -113,9 +113,9 @@ namespace storm { /*! * Creates a new min/max linear equation solver instance with the given matrix. */ - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix, bool trackPolicy = false) const; - void setSolverType(storm::solver::EquationSolverTypeSelection solverType); - void setPreferredTechnique(storm::solver::MinMaxTechniqueSelection); + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix, bool trackScheduler = false) const; + MinMaxLinearEquationSolverFactory& setSolverType(storm::solver::EquationSolverTypeSelection solverType); + MinMaxLinearEquationSolverFactory& setPreferredTechnique(storm::solver::MinMaxTechniqueSelection); protected: /// The type of solver which should be created. diff --git a/src/utility/vector.h b/src/utility/vector.h index 665569645..31b1a5493 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -388,55 +388,64 @@ namespace storm { */ template VT sum_if(std::vector const& values, storm::storage::BitVector const& filter) { - assert(values.size() >= filter.size()); + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); VT sum = storm::utility::zero(); - for(uint_fast64_t i : filter) { - sum += values[i]; + for(auto pos : filter) { + sum += values[pos]; } return sum; } /** - * Computes the maximum of the entries from the values that are set to one in the filter vector - * @param values - * @param filter - * @param smallestPossibleValue A value which is not larger than any value in values. If the filter is empty, this value is returned. - * @return The maximum over the subset of the values and the smallestPossibleValue. + * Computes the maximum of the entries from the values that are selected by the (non-empty) filter. + * @param values The values in which to search. + * @param filter The filter to use. + * @return The maximum over the selected values. */ template - VT max_if(std::vector const& values, storm::storage::BitVector const& filter, VT const& smallestPossibleValue) { - assert(values.size() >= filter.size()); + VT max_if(std::vector const& values, storm::storage::BitVector const& filter) { + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); + STORM_LOG_ASSERT(!filter.empty(), "Empty selection."); + + auto it = filter.begin(); + auto ite = filter.end(); + + VT current = values[*it]; + ++it; - VT max = smallestPossibleValue; - for(uint_fast64_t i : filter) { - if(values[i] > max) { - max = values[i]; + for (; it != ite; ++it) { + if (values[*it] > current) { + current = values[*it]; } - } - return max; + } + return current; } /** - * Computes the minimum of the entries from the values that are set to one in the filter vector - * @param values - * @param filter - * @param largestPossibleValue A value which is not smaller than any value in values. If the filter is empty, this value is returned. - * @return The minimum over the subset of the values and the largestPossibleValue. + * Computes the minimum of the entries from the values that are selected by the (non-empty) filter. + * @param values The values in which to search. + * @param filter The filter to use. + * @return The minimum over the selected values. */ template - VT min_if(std::vector const& values, storm::storage::BitVector const& filter, VT const& largestPossibleValue) { - assert(values.size() >= filter.size()); - VT min = largestPossibleValue; - for(uint_fast64_t i : filter) { - if(values[i] < min) { - min = values[i]; + VT min_if(std::vector const& values, storm::storage::BitVector const& filter) { + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); + STORM_LOG_ASSERT(!filter.empty(), "Empty selection."); + + auto it = filter.begin(); + auto ite = filter.end(); + + VT current = values[*it]; + ++it; + + for (; it != ite; ++it) { + if (values[*it] < current) { + current = values[*it]; } - } - return min; + } + return current; } - - /*! * Reduces the given source vector by selecting an element according to the given filter out of each row group. * diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 23184f61f..725e1376d 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -14,6 +14,8 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/parser/AutoParser.h" +#include "src/parser/PrismParser.h" +#include "src/builder/ExplicitPrismModelBuilder.h" TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); @@ -188,3 +190,53 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); } + +TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/scheduler_generation.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); + EXPECT_EQ(4ul, model->getNumberOfStates()); + EXPECT_EQ(11ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(7ul, mdp->getNumberOfChoices()); + + auto solverFactory = std::make_unique>(storm::solver::EquationSolverTypeSelection::Gmmxx); + solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::PolicyIteration); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + checkTask.setProduceSchedulers(true); + + std::unique_ptr result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(0, scheduler.getChoice(0)); + EXPECT_EQ(1, scheduler.getChoice(1)); + EXPECT_EQ(0, scheduler.getChoice(2)); + EXPECT_EQ(0, scheduler.getChoice(3)); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); + + checkTask = storm::modelchecker::CheckTask(*formula); + checkTask.setProduceSchedulers(true); + result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(1, scheduler2.getChoice(0)); + EXPECT_EQ(2, scheduler2.getChoice(1)); + EXPECT_EQ(0, scheduler2.getChoice(2)); + EXPECT_EQ(0, scheduler2.getChoice(3)); +} diff --git a/test/functional/modelchecker/scheduler_generation.nm b/test/functional/modelchecker/scheduler_generation.nm new file mode 100644 index 000000000..f5be3b746 --- /dev/null +++ b/test/functional/modelchecker/scheduler_generation.nm @@ -0,0 +1,16 @@ +mdp + +module one + + s : [0 .. 5] init 0; + + [] s=0 -> 0.5: (s'=1) + 0.5: (s'=3); + [] s=1 -> 0.4 : (s'=4) + 0.6: (s'=3); + [] s=1 -> 1: (s'=4); + [] s=1 -> 0.8: (s'=3) + 0.2: (s'=4); + [] s=0 | s = 2 -> 0.9: (s'=s) + 0.1 : (s'=3); + [] 3 <= s & s <= 4 -> 1: true; + +endmodule + +label "target" = s=3; diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index ff91e660a..1839b1016 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -39,7 +39,8 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio double bound = 0.8; storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); - solver.setEarlyTerminationCriterion(std::make_unique>(storm::storage::BitVector(1, true), bound, true)); + + solver.setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true)); ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -47,11 +48,10 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); bound = 0.6; - solver.setEarlyTerminationCriterion(std::make_unique>(storm::storage::BitVector(1, true), bound, true)); + solver.setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true)); ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); - } TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) { diff --git a/test/functional/utility/VectorTest.cpp b/test/functional/utility/VectorTest.cpp index 9494d6146..0cef4cd9c 100644 --- a/test/functional/utility/VectorTest.cpp +++ b/test/functional/utility/VectorTest.cpp @@ -18,8 +18,8 @@ TEST(VectorTest, max_if) { storm::storage::BitVector f1(5, {2,4}); storm::storage::BitVector f2(5, {3,4}); - ASSERT_EQ(34.0, storm::utility::vector::max_if(a,f1,0.0)); - ASSERT_EQ(16.0, storm::utility::vector::max_if(a,f2,0.0)); + ASSERT_EQ(34.0, storm::utility::vector::max_if(a, f1)); + ASSERT_EQ(16.0, storm::utility::vector::max_if(a, f2)); } @@ -28,6 +28,6 @@ TEST(VectorTest, min_if) { storm::storage::BitVector f1(5, {2,4}); storm::storage::BitVector f2(5, {3,4}); - ASSERT_EQ(16.0, storm::utility::vector::min_if(a,f1,100.0)); - ASSERT_EQ(8.0, storm::utility::vector::min_if(a,f2,100.0)); + ASSERT_EQ(16.0, storm::utility::vector::min_if(a, f1)); + ASSERT_EQ(8.0, storm::utility::vector::min_if(a, f2)); }