diff --git a/resources/examples/testfiles/imdp/tiny-03.drn b/resources/examples/testfiles/imdp/tiny-03.drn index 46767f506c..01c8fd5858 100644 --- a/resources/examples/testfiles/imdp/tiny-03.drn +++ b/resources/examples/testfiles/imdp/tiny-03.drn @@ -14,8 +14,8 @@ state 0 init 1 : [0.4, 0.9] 2 : [0.5, 0.8] action 1 - 1 : [0.4, 0.9] - 2 : [0.5, 0.8] + 1 : [0.3, 0.7] + 2 : [0.4, 0.8] state 1 target action 0 1 : [1, 1] diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 8cdc5d0ef6..f8e1badbd0 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -9,6 +9,7 @@ #include "storm-parsers/parser/ValueParser.h" #include "storm/adapters/IntervalAdapter.h" +#include "storm/adapters/IntervalForward.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/exceptions/AbortException.h" @@ -87,6 +88,8 @@ bool isCompatibleValueType(DirectEncodingValueType fileValueType) { return fileValueType == Double || fileValueType == Rational; } else if constexpr (std::is_same_v) { return fileValueType == Double || fileValueType == Rational || fileValueType == DoubleInterval || fileValueType == RationalInterval; + } else if constexpr (std::is_same_v) { + return fileValueType == Double || fileValueType == Rational || fileValueType == DoubleInterval || fileValueType == RationalInterval; } else if constexpr (std::is_same_v) { return fileValueType == Double || fileValueType == Rational || fileValueType == Parametric; } else { @@ -581,6 +584,8 @@ template std::shared_ptr> pa std::filesystem::path const& file, DirectEncodingParserOptions const& options); template std::shared_ptr> parseDirectEncodingModel(std::filesystem::path const& file, DirectEncodingParserOptions const& options); +template std::shared_ptr> parseDirectEncodingModel( + std::filesystem::path const& file, DirectEncodingParserOptions const& options); template std::shared_ptr> parseDirectEncodingModel( std::filesystem::path const& file, DirectEncodingParserOptions const& options); diff --git a/src/storm-parsers/parser/ValueParser.cpp b/src/storm-parsers/parser/ValueParser.cpp index 00df851f84..4bb0e35e88 100644 --- a/src/storm-parsers/parser/ValueParser.cpp +++ b/src/storm-parsers/parser/ValueParser.cpp @@ -119,6 +119,51 @@ bool parseInterval(std::string const& value, storm::Interval& result) { return true; } +bool parseRationalInterval(std::string const& value, storm::RationalInterval& result) { + // Try whether it is a constant. + if (storm::RationalNumber pointResult; parseNumber(value, pointResult)) { + result = storm::RationalInterval(pointResult); + return true; + } + + std::string intermediate = value; + boost::trim(intermediate); + carl::BoundType leftBound; + carl::BoundType rightBound; + if (intermediate.front() == '(') { + leftBound = carl::BoundType::STRICT; + } else if (intermediate.front() == '[') { + leftBound = carl::BoundType::WEAK; + } else { + return false; // Expect start with '(' or '['. + } + if (intermediate.back() == ')') { + rightBound = carl::BoundType::STRICT; + } else if (intermediate.back() == ']') { + rightBound = carl::BoundType::WEAK; + } else { + return false; // Expected end with ')' or ']'. + } + intermediate = intermediate.substr(1, intermediate.size() - 2); + + std::vector words; + boost::split(words, intermediate, boost::is_any_of(",")); + if (words.size() != 2) { + return false; // Did not find exactly one comma. + } + storm::RationalNumber leftVal, rightVal; + boost::trim(words[0]); + if (!parseNumber(words[0], leftVal)) { + return false; // lower value of interval invalid. + } + boost::trim(words[1]); + if (!parseNumber(words[1], rightVal)) { + return false; // upper value of interval invalid. + } + result = storm::RationalInterval(leftVal, leftBound, rightVal, rightBound); + return true; +} + template bool parseNumber(std::string const& value, NumberType& result) { if constexpr (std::is_same_v) { @@ -127,6 +172,8 @@ bool parseNumber(std::string const& value, NumberType& result) { return carl::try_parse(value, result); } else if constexpr (std::is_same_v) { return parseInterval(value, result); + } else if constexpr (std::is_same_v) { + return parseRationalInterval(value, result); } else { return boost::conversion::try_lexical_convert(value, result); } @@ -137,6 +184,7 @@ template class ValueParser; template class ValueParser; template class ValueParser; template class ValueParser; +template class ValueParser; template std::size_t parseNumber(std::string const&); diff --git a/src/storm/adapters/IntervalForward.h b/src/storm/adapters/IntervalForward.h index ddc9a5d284..f0fc334b2e 100644 --- a/src/storm/adapters/IntervalForward.h +++ b/src/storm/adapters/IntervalForward.h @@ -1,5 +1,7 @@ #pragma once +#include "storm/adapters/RationalNumberForward.h" + namespace carl { template class Interval; @@ -11,6 +13,7 @@ namespace storm { * Interval type */ typedef carl::Interval Interval; +typedef carl::Interval RationalInterval; namespace detail { template @@ -23,6 +26,11 @@ struct IntervalMetaProgrammingHelper { using BaseType = double; static const bool isInterval = true; }; +template<> +struct IntervalMetaProgrammingHelper { + using BaseType = storm::RationalNumber; + static const bool isInterval = true; +}; } // namespace detail /*! diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 4f7a195177..55dbcfdc8a 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -431,6 +431,7 @@ template class ExplicitModelBuilder, uint32_t>; template class ExplicitModelBuilder, uint32_t>; // TODO: where is this used? template class ExplicitModelBuilder, uint32_t>; +template class ExplicitModelBuilder, uint32_t>; } // namespace builder } // namespace storm diff --git a/src/storm/builder/RewardModelBuilder.cpp b/src/storm/builder/RewardModelBuilder.cpp index 6b01224047..d6681c99ad 100644 --- a/src/storm/builder/RewardModelBuilder.cpp +++ b/src/storm/builder/RewardModelBuilder.cpp @@ -66,6 +66,7 @@ template class RewardModelBuilder; template class RewardModelBuilder; template class RewardModelBuilder; template class RewardModelBuilder; +template class RewardModelBuilder; } // namespace builder } // namespace storm diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index 6350cb0d6d..a082330868 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -205,5 +205,6 @@ template struct Choice; template struct Choice; template struct Choice; template struct Choice; +template struct Choice; } // namespace generator } // namespace storm diff --git a/src/storm/generator/Distribution.cpp b/src/storm/generator/Distribution.cpp index 32969b24a3..8ef23fc3fb 100644 --- a/src/storm/generator/Distribution.cpp +++ b/src/storm/generator/Distribution.cpp @@ -129,10 +129,12 @@ template class Distribution; template class Distribution; template class Distribution; template class Distribution; +template class Distribution; template class Distribution; template class Distribution; template class Distribution; template class Distribution; +template class Distribution; } // namespace storm::generator diff --git a/src/storm/generator/DistributionEntry.cpp b/src/storm/generator/DistributionEntry.cpp index 1545afdc81..9c48bc39d5 100644 --- a/src/storm/generator/DistributionEntry.cpp +++ b/src/storm/generator/DistributionEntry.cpp @@ -1,4 +1,5 @@ #include "storm/generator/DistributionEntry.h" +#include #include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -41,10 +42,12 @@ template class DistributionEntry; template class DistributionEntry; template class DistributionEntry; template class DistributionEntry; +template class DistributionEntry; template class DistributionEntry; template class DistributionEntry; template class DistributionEntry; template class DistributionEntry; +template class DistributionEntry; } // namespace storm::generator diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 4bb73c6394..aa3d1cf334 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -363,5 +363,9 @@ template class NextStateGenerator; template class ActionMask; template class StateValuationFunctionMask; template class NextStateGenerator; + +template class ActionMask; +template class StateValuationFunctionMask; +template class NextStateGenerator; } // namespace generator } // namespace storm diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index f9a7cd251a..e020c7d6f7 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -1100,5 +1100,6 @@ template class PrismNextStateGenerator; template class PrismNextStateGenerator; template class PrismNextStateGenerator; template class PrismNextStateGenerator; +template class PrismNextStateGenerator; } // namespace generator } // namespace storm diff --git a/src/storm/generator/StateBehavior.cpp b/src/storm/generator/StateBehavior.cpp index f09edce0e6..533a1d4a85 100644 --- a/src/storm/generator/StateBehavior.cpp +++ b/src/storm/generator/StateBehavior.cpp @@ -76,5 +76,6 @@ template class StateBehavior; template class StateBehavior; template class StateBehavior; template class StateBehavior; +template class StateBehavior; } // namespace generator } // namespace storm diff --git a/src/storm/io/DirectEncodingExporter.cpp b/src/storm/io/DirectEncodingExporter.cpp index 39366362e3..26679ca7f0 100644 --- a/src/storm/io/DirectEncodingExporter.cpp +++ b/src/storm/io/DirectEncodingExporter.cpp @@ -72,6 +72,8 @@ void explicitExportSparseModel(std::ostream& os, std::shared_ptr) { os << "double-interval"; + } else if constexpr (std::is_same_v) { + os << "rational-interval"; } else if constexpr (std::is_same_v) { os << "parametric"; } else { @@ -338,5 +340,8 @@ template void explicitExportSparseModel(std::ostream& o std::vector const& parameters, DirectEncodingExporterOptions const& options); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters, DirectEncodingExporterOptions const& options); +template void explicitExportSparseModel(std::ostream& os, + std::shared_ptr> sparseModel, + std::vector const& parameters, DirectEncodingExporterOptions const& options); } // namespace io } // namespace storm diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 92122e5605..1a02acc28e 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -473,6 +473,9 @@ template class AbstractModelChecker>; template class AbstractModelChecker>>; template class AbstractModelChecker>>; +template class AbstractModelChecker>>; +template class AbstractModelChecker>>; + template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; @@ -491,6 +494,9 @@ template class AbstractModelChecker>; template class AbstractModelChecker>; +template class AbstractModelChecker>; +template class AbstractModelChecker>; + // DD template class AbstractModelChecker>; template class AbstractModelChecker>; diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index d1ec2e86ff..51261bddce 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -15,13 +15,31 @@ class CheckResult; template class AbstractModelChecker { + private: + // Due to a GCC bug we have to add this dummy template type here + // https://stackoverflow.com/questions/49707184/explicit-specialization-in-non-namespace-scope-does-not-compile-in-gcc + template + struct GetSolutionType { + using type = T; + }; + + template + struct GetSolutionType { + using type = double; + }; + + template + struct GetSolutionType { + using type = storm::RationalNumber; + }; + public: virtual ~AbstractModelChecker() { // Intentionally left empty. } typedef typename ModelType::ValueType ValueType; - using SolutionType = typename std::conditional, double, ValueType>::type; + using SolutionType = typename GetSolutionType::type; /*! * Returns the name of the model checker class (e.g., for display in error messages). diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index e4e5f820b1..6e15e9e9be 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -105,7 +105,8 @@ std::unique_ptr SparseMarkovAutomatonCslModelChecker subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities( - env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + env, checkTask.getOptimizationDirection(), checkTask.getUncertaintyResolutionMode(), this->getModel().getTransitionMatrix(), + subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp index 02cb13fbca..b4a53af606 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp @@ -1,9 +1,14 @@ #include "storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h" +#include "storm/adapters/IntervalAdapter.h" +#include "storm/adapters/IntervalForward.h" +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/adapters/RationalNumberForward.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/BitVector.h" #include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -17,22 +22,20 @@ namespace storm { namespace modelchecker { namespace helper { -template -SparseNondeterministicStepBoundedHorizonHelper::SparseNondeterministicStepBoundedHorizonHelper( +template +SparseNondeterministicStepBoundedHorizonHelper::SparseNondeterministicStepBoundedHorizonHelper( /*storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions*/) // transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions) { // Intentionally left empty. } -template -std::vector SparseNondeterministicStepBoundedHorizonHelper::compute(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& phiStates, - storm::storage::BitVector const& psiStates, uint64_t lowerBound, - uint64_t upperBound, ModelCheckerHint const& hint) { - std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); +template +std::vector SparseNondeterministicStepBoundedHorizonHelper::compute( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + uint64_t lowerBound, uint64_t upperBound, ModelCheckerHint const& hint) { + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); storm::storage::BitVector makeZeroColumns; // Determine the states that have 0 probability of reaching the target states. @@ -56,34 +59,60 @@ std::vector SparseNondeterministicStepBoundedHorizonHelper STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0."); if (!maybeStates.empty()) { - // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false, makeZeroColumns); - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, psiStates); + storm::storage::SparseMatrix submatrix; + std::vector b; + uint64_t subresultSize; + + if constexpr (storm::IsIntervalType) { + // For intervals, we cannot remove all non maybe states as that would lead to the upper probability of rows summing to below 1. + // Instead we only drop all outgoing transitions of non maybe states. + // See src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp:624 for more details. + submatrix = transitionMatrix.filterEntries(transitionMatrix.getRowFilter(maybeStates)); + + storm::utility::vector::setAllValues(b, transitionMatrix.getRowFilter(psiStates)); + + subresultSize = transitionMatrix.getRowCount(); + } else { + // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. + submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false, makeZeroColumns); + + b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, psiStates); + subresultSize = maybeStates.getNumberOfSetBits(); + } // Create the vector with which to multiply. - std::vector subresult(maybeStates.getNumberOfSetBits()); + std::vector subresult(subresultSize); - auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); if (lowerBound == 0) { - multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound, goal.getUncertaintyResolutionMode()); } else { - multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1); - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); - auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1, goal.getUncertaintyResolutionMode()); + + storm::storage::SparseMatrix submatrix; + if constexpr (storm::IsIntervalType) { + submatrix = transitionMatrix.filterEntries(transitionMatrix.getRowFilter(maybeStates)); + } else { + submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); + } + + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); b = std::vector(b.size(), storm::utility::zero()); - multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, lowerBound - 1); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, lowerBound - 1, goal.getUncertaintyResolutionMode()); } // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); } if (lowerBound == 0) { - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } return result; } template class SparseNondeterministicStepBoundedHorizonHelper; template class SparseNondeterministicStepBoundedHorizonHelper; +template class SparseNondeterministicStepBoundedHorizonHelper; +template class SparseNondeterministicStepBoundedHorizonHelper; } // namespace helper } // namespace modelchecker } // namespace storm \ No newline at end of file diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h index fae2a12eae..304cee3ed9 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h @@ -10,15 +10,15 @@ namespace storm { namespace modelchecker { namespace helper { -template +template class SparseNondeterministicStepBoundedHorizonHelper { public: SparseNondeterministicStepBoundedHorizonHelper(); - std::vector compute(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, - storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound, - ModelCheckerHint const& hint = ModelCheckerHint()); + std::vector compute(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound, + ModelCheckerHint const& hint = ModelCheckerHint()); private: }; diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 80d87e91bd..3c241c4688 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -373,7 +373,7 @@ void LraViHelper::performIterationSte } else { // Also keep track of the choices made. std::vector tsChoices(_TsTransitions.getRowGroupCount()); - _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices); + _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), UncertaintyResolutionMode::Unset, &tsChoices); // Note that nondeterminism within the timed states means that there can not be instant states (We either have MDPs or MAs) // Hence, in this branch we don't have to care for choices at instant states. STORM_LOG_ASSERT(!_hasInstantStates, "Nondeterministic timed states are only supported if there are no instant states."); diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp index e35a064071..915155cf78 100644 --- a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp @@ -122,6 +122,7 @@ template class ExplicitModelCheckerHint; template class ExplicitModelCheckerHint; template class ExplicitModelCheckerHint; template class ExplicitModelCheckerHint; +template class ExplicitModelCheckerHint; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/hints/ModelCheckerHint.cpp b/src/storm/modelchecker/hints/ModelCheckerHint.cpp index af5991fb16..073e6b884f 100644 --- a/src/storm/modelchecker/hints/ModelCheckerHint.cpp +++ b/src/storm/modelchecker/hints/ModelCheckerHint.cpp @@ -34,6 +34,8 @@ template ExplicitModelCheckerHint const& ModelCheckerHi template ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint(); template ExplicitModelCheckerHint const& ModelCheckerHint::asExplicitModelCheckerHint() const; template ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint(); +template ExplicitModelCheckerHint const& ModelCheckerHint::asExplicitModelCheckerHint() const; +template ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint(); } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index e54a69b4ef..e5ee8b3c78 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -141,7 +141,7 @@ template std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities( Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); - if (storm::IsIntervalType) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(checkTask.isUncertaintyResolutionModeSet(), storm::exceptions::InvalidSettingsException, "Uncertainty resolution mode must be set for uncertain (interval) models."); STORM_LOG_THROW(checkTask.getUncertaintyResolutionMode() != UncertaintyResolutionMode::Robust && @@ -297,7 +297,7 @@ template std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards( Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); - if (storm::IsIntervalType) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(checkTask.isUncertaintyResolutionModeSet(), storm::exceptions::InvalidSettingsException, "Uncertainty resolution mode must be set for uncertain (interval) models."); STORM_LOG_THROW(checkTask.getUncertaintyResolutionMode() != UncertaintyResolutionMode::Robust && @@ -537,5 +537,6 @@ template class SparseDtmcPrctlModelChecker>; template class SparseDtmcPrctlModelChecker>; template class SparseDtmcPrctlModelChecker>; template class SparseDtmcPrctlModelChecker>; +template class SparseDtmcPrctlModelChecker>; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 6372205cdc..551b6a48cc 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -1,5 +1,6 @@ #pragma once +#include "storm/adapters/IntervalForward.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/models/sparse/Dtmc.h" @@ -11,7 +12,7 @@ class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker, double, ValueType>::type; + using SolutionType = storm::IntervalBaseType; explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 0d21f5c533..54f0fb436c 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -1,6 +1,7 @@ #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "storm/adapters/IntervalAdapter.h" +#include "storm/adapters/IntervalForward.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -37,13 +38,16 @@ template bool SparseMdpPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { if (formula.isInFragment(storm::logic::propositional())) { return true; } if (formula.isInFragment(storm::logic::reachability())) { return true; } + if (formula.isInFragment(storm::logic::prctlstar().setBoundedUntilFormulasAllowed(true))) { + return true; + } } else { if (formula.isInFragment(storm::logic::prctlstar() .setLongRunAverageRewardFormulasAllowed(true) @@ -111,14 +115,14 @@ bool SparseMdpPrctlModelChecker::canHandle(CheckTask std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities( Environment const& env, CheckTask const& checkTask) { - if constexpr (std::is_same_v) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented bounded until with intervals"); - return nullptr; - } else { - storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, - "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, + "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented multi dimensional bounded until with intervals"); + return nullptr; + } else { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking non-trivial bounded until formulas is not optimized w.r.t. qualitative queries"); @@ -131,23 +135,21 @@ std::unique_ptr SparseMdpPrctlModelChecker::com auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeRewardBoundedValues( env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - } else { - STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); - STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, - "Formula lower step bound must be discrete/integral."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, - "Formula needs to have discrete upper time bound."); - std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); - std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); - storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper helper; - std::vector numericResult = - helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), - pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), checkTask.getHint()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + } else { + STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); + storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper helper; + std::vector numericResult = + helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), + pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } } @@ -160,7 +162,8 @@ std::unique_ptr SparseMdpPrctlModelChecker::com std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities( - env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + env, checkTask.getOptimizationDirection(), checkTask.getUncertaintyResolutionMode(), this->getModel().getTransitionMatrix(), + subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -206,7 +209,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com template std::unique_ptr SparseMdpPrctlModelChecker::computeHOAPathProbabilities( Environment const& env, CheckTask const& checkTask) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented automata-props with intervals"); } else { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); @@ -233,7 +236,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com template std::unique_ptr SparseMdpPrctlModelChecker::computeLTLProbabilities( Environment const& env, CheckTask const& checkTask) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented LTL with intervals"); } else { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); @@ -278,7 +281,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { throw exceptions::NotImplementedException() << "Conditional Probabilities are not supported with interval models"; } else { return storm::modelchecker::computeConditionalProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), @@ -290,28 +293,27 @@ std::unique_ptr SparseMdpPrctlModelChecker::com template std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards( Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Cumulative reward properties are not implemented for interval models."); + } storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { - if constexpr (std::is_same_v) { - throw exceptions::NotImplementedException() << "Multi-reward bounded is not supported with interval models"; - } else { - STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, - "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model."); - STORM_LOG_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException, - "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given."); - STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries"); - storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection()); - if (checkTask.isBoundSet()) { - opInfo.bound = checkTask.getBound(); - } - auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo); - helper::rewardbounded::MultiDimensionalRewardUnfolding rewardUnfolding(this->getModel(), formula); - auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeRewardBoundedValues( - env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, + "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model."); + STORM_LOG_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException, + "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given."); + STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries"); + storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection()); + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo); + helper::rewardbounded::MultiDimensionalRewardUnfolding rewardUnfolding(this->getModel(), formula); + auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeRewardBoundedValues( + env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); @@ -328,6 +330,12 @@ std::unique_ptr SparseMdpPrctlModelChecker +std::unique_ptr SparseMdpPrctlModelChecker>::computeDiscountedCumulativeRewards( + Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Discounted properties are not implemented for interval models."); +} + template std::unique_ptr SparseMdpPrctlModelChecker::computeDiscountedCumulativeRewards( Environment const& env, CheckTask const& checkTask) { @@ -417,6 +425,12 @@ std::unique_ptr SparseMdpPrctlModelChecker +std::unique_ptr SparseMdpPrctlModelChecker>::computeDiscountedTotalRewards( + Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Discounted properties are not implemented for interval models."); +} + template std::unique_ptr SparseMdpPrctlModelChecker::computeDiscountedTotalRewards( Environment const& env, CheckTask const& checkTask) { @@ -439,7 +453,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com template std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities( Environment const& env, CheckTask const& checkTask) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented LRA probabilities with intervals"); } else { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); @@ -464,7 +478,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com template std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageRewards( Environment const& env, CheckTask const& checkTask) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lra with intervals"); } else { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, @@ -485,7 +499,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com template std::unique_ptr SparseMdpPrctlModelChecker::checkMultiObjectiveFormula( Environment const& env, CheckTask const& checkTask) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented multi-objective with intervals"); } else { return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula(), checkTask.isProduceSchedulersSet()); @@ -495,7 +509,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::che template std::unique_ptr SparseMdpPrctlModelChecker::checkLexObjectiveFormula( const Environment& env, const CheckTask& checkTask) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lexicographic model checking with intervals"); } else { auto formulaChecker = [&](storm::logic::Formula const& formula) { @@ -510,7 +524,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::che template std::unique_ptr SparseMdpPrctlModelChecker::checkQuantileFormula( Environment const& env, CheckTask const& checkTask) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented quantile formulas with intervals"); } else { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, @@ -533,5 +547,6 @@ std::unique_ptr SparseMdpPrctlModelChecker::che template class SparseMdpPrctlModelChecker>; template class SparseMdpPrctlModelChecker>; template class SparseMdpPrctlModelChecker>; +template class SparseMdpPrctlModelChecker>; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index aa39728344..5a7f10a1fe 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -14,7 +14,7 @@ class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker, double, ValueType>::type; + using SolutionType = storm::IntervalBaseType; explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index a8c6153e06..ba0bd28c3a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -939,6 +939,7 @@ template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper, double>; +template class SparseDtmcPrctlHelper, storm::RationalNumber>; } // namespace helper } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp index 275318d813..9ef02c1c25 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp @@ -105,7 +105,7 @@ SparseMdpEndComponentInformation SparseMdpEndComponentInformation* columnSumVector, std::vector* summandResultVector, bool gatherExitChoices) { SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); // TODO: Just like SparseMdpPrctlHelper::computeFixedPointSystemUntilProbabilities, this method must be adapted for intervals. - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support the elimination of end components and the creation of an adequate equation system with interval models."); } @@ -247,7 +247,7 @@ SparseMdpEndComponentInformation SparseMdpEndComponentInformation& submatrix, std::vector& subvector, bool gatherExitChoices) { SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); // TODO: Just like SparseMdpPrctlHelper::computeFixedPointSystemUntilProbabilities, this method must be adapted for intervals. - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support the elimination of end components and the creation of an adequate equation system with interval models."); } @@ -421,6 +421,7 @@ void SparseMdpEndComponentInformation::setScheduler(storm::storage::S template class SparseMdpEndComponentInformation; template class SparseMdpEndComponentInformation; template class SparseMdpEndComponentInformation; +template class SparseMdpEndComponentInformation; template void SparseMdpEndComponentInformation::setScheduler(storm::storage::Scheduler& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix const& transitionMatrix, @@ -438,6 +439,11 @@ template void SparseMdpEndComponentInformation::setScheduler(st storm::storage::SparseMatrix const& backwardTransitions, std::vector const& fromResult); +template void SparseMdpEndComponentInformation::setScheduler( + storm::storage::Scheduler& scheduler, storm::storage::BitVector const& maybeStates, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, std::vector const& fromResult); + // template class SparseMdpEndComponentInformation; } // namespace helper diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index ce93657d0d..7e10f08ed4 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -43,7 +43,7 @@ template std::map SparseMdpPrctlHelper::computeRewardBoundedValues( Environment const& env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing reward bounded values with interval models."); } else { storm::utility::Stopwatch swAll(true), swBuild, swCheck; @@ -131,20 +131,16 @@ std::map SparseMdpPrctlHelper< template std::vector SparseMdpPrctlHelper::computeNextProbabilities( - Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::BitVector const& nextStates) { - if constexpr (std::is_same_v) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support next probabilities with reward models."); - } else { - // Create the vector with which to multiply and initialize it correctly. - std::vector result(transitionMatrix.getRowGroupCount()); - storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); + Environment const& env, OptimizationDirection dir, UncertaintyResolutionMode uncertaintyResolutionMode, + storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates) { + // Create the vector with which to multiply and initialize it correctly. + std::vector result(transitionMatrix.getRowGroupCount()); + storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); - auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->multiplyAndReduce(env, dir, result, nullptr, result); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->multiplyAndReduce(env, dir, result, nullptr, result, uncertaintyResolutionMode); - return result; - } + return result; } template @@ -612,7 +608,7 @@ void computeFixedPointSystemUntilProbabilities(storm::solver::SolveGoal const& transitionMatrix, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix& submatrix, std::vector& b) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { // For non-interval based models, we can eliminate the rows and columns from the original transition probability matrix for states // whose probabilities are already known... However, there is information in the transition to those states. // Thus, we cannot eliminate them all. @@ -757,7 +753,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support this end component with interval models."); } else { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); @@ -768,7 +764,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper) { + if constexpr (!storm::IsIntervalType) { // For non-interval models, we only operated on the maybe states, and we must recover the qualitative values for the other state. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); } else { @@ -777,8 +773,8 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper>(*scheduler, resultForMaybeStates.getScheduler(), - qualitativeStateSets.maybeStates); + extractSchedulerChoices>(*scheduler, resultForMaybeStates.getScheduler(), + qualitativeStateSets.maybeStates); } } } @@ -833,7 +829,7 @@ template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards( Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support instantenous rewards with interval models."); } else { // Only compute the result if the model has a state-based reward this->getModel(). @@ -843,7 +839,7 @@ std::vector SparseMdpPrctlHelper::compute std::vector result(rewardModel.getStateRewardVector()); auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, nullptr, stepCount); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, nullptr, stepCount, goal.getUncertaintyResolutionMode()); return result; } @@ -854,7 +850,7 @@ template std::vector SparseMdpPrctlHelper::computeCumulativeRewards( Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support cumulative rewards with interval models."); } else { // Only compute the result if the model has at least one reward this->getModel(). @@ -867,7 +863,7 @@ std::vector SparseMdpPrctlHelper::compute std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound, goal.getUncertaintyResolutionMode()); return result; } @@ -989,7 +985,8 @@ std::vector SparseMdpPrctlHelper::compute std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->repeatedMultiplyAndReduceWithFactor(env, goal.direction(), result, &totalRewardVector, stepBound, discountFactor); + multiplier->repeatedMultiplyAndReduceWithFactor(env, goal.direction(), result, &totalRewardVector, stepBound, discountFactor, + goal.getUncertaintyResolutionMode()); return result; } @@ -1061,27 +1058,69 @@ std::vector SparseMdpPrctlHelper::compute bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative) { // Only compute the result if the reward model is not empty. STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - return computeReachabilityRewardsHelper( - env, std::move(goal), transitionMatrix, backwardTransitions, - [&](uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { - std::vector result; - result.reserve(rowCount); - std::vector subIntervalVector = intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); - for (auto const& interval : subIntervalVector) { - result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper()); - } - return result; - }, - targetStates, qualitative, false, - [&]() { - return intervalRewardModel.getStatesWithFilter( - transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); }); - }, - [&]() { - return intervalRewardModel.getChoicesWithFilter( - transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); }); - }) - .values; + if constexpr (std::is_same_v) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support double interval rewards with rational interval models."); + } else { + return computeReachabilityRewardsHelper( + env, std::move(goal), transitionMatrix, backwardTransitions, + [&](uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { + std::vector result; + result.reserve(rowCount); + std::vector subIntervalVector = intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); + for (auto const& interval : subIntervalVector) { + result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper()); + } + return result; + }, + targetStates, qualitative, false, + [&]() { + return intervalRewardModel.getStatesWithFilter( + transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); }); + }, + [&]() { + return intervalRewardModel.getChoicesWithFilter( + transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); }); + }) + .values; + } +} + +template +std::vector SparseMdpPrctlHelper::computeReachabilityRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, + storm::storage::BitVector const& targetStates, bool qualitative) { + // Only compute the result if the reward model is not empty. + STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + if constexpr (std::is_same_v) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support rational interval rewards with double interval models."); + } else { + return computeReachabilityRewardsHelper( + env, std::move(goal), transitionMatrix, backwardTransitions, + [&](uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { + std::vector result; + result.reserve(rowCount); + std::vector subIntervalVector = + intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); + for (auto const& interval : subIntervalVector) { + result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper()); + } + return result; + }, + targetStates, qualitative, false, + [&]() { + return intervalRewardModel.getStatesWithFilter(transitionMatrix, [&](storm::RationalInterval const& i) { + return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); + }); + }, + [&]() { + return intervalRewardModel.getChoicesWithFilter(transitionMatrix, [&](storm::RationalInterval const& i) { + return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); + }); + }) + .values; + } } template<> @@ -1092,6 +1131,15 @@ std::vector SparseMdpPrctlHelper:: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Computing reachability rewards is unsupported for this data type."); } +template<> +std::vector SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&&, + storm::storage::SparseMatrix const&, + storm::storage::SparseMatrix const&, + storm::models::sparse::StandardRewardModel const&, bool, + storm::storage::BitVector const&, bool) { + STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Computing reachability rewards is unsupported for this data type."); +} + struct QualitativeStateSetsReachabilityRewards { storm::storage::BitVector maybeStates; storm::storage::BitVector infinityStates; @@ -1332,7 +1380,7 @@ template void computeUpperRewardBounds(SparseMdpHintType& hintInformation, storm::OptimizationDirection const& direction, storm::storage::SparseMatrix const& submatrix, std::vector const& choiceRewards, std::vector const& oneStepTargetProbabilities) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing upper reward bounds with interval models."); } else { // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17). @@ -1371,7 +1419,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper> scheduler; if (produceScheduler) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support producing schedulers in this function with interval models."); } else { scheduler = std::make_unique>(transitionMatrix.getRowGroupCount()); @@ -1416,7 +1464,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper> ecInformation; if (hintInformation.getEliminateEndComponents()) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models."); } else { ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents( @@ -1441,7 +1489,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models."); } else { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); @@ -1472,7 +1520,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelperisDeterministicScheduler(), "Expected a deterministic scheduler"); STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { return MDPSparseModelCheckingHelperReturnType(std::move(result)); } else { return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); @@ -1546,6 +1594,30 @@ template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint); +template class SparseMdpPrctlHelper; +template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards( + Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount); +template std::vector SparseMdpPrctlHelper::computeCumulativeRewards( + Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound); +template MDPSparseModelCheckingHelperReturnType +SparseMdpPrctlHelper::computeReachabilityRewards( + Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, + bool produceScheduler, ModelCheckerHint const& hint); +template MDPSparseModelCheckingHelperReturnType +SparseMdpPrctlHelper::computeTotalRewards( + Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative, bool produceScheduler, + ModelCheckerHint const& hint); + } // namespace helper } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index eb9576b0da..12f2ebbc18 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -7,6 +7,7 @@ #include "storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h" #include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" #include "storm/solver/SolveGoal.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/storage/MaximalEndComponent.h" #include "storm/storage/SparseMatrix.h" @@ -38,6 +39,7 @@ class SparseMdpPrctlHelper { storm::storage::BitVector const& initialStates); static std::vector computeNextProbabilities(Environment const& env, OptimizationDirection dir, + UncertaintyResolutionMode uncertaintyResolutionMode, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates); @@ -98,6 +100,12 @@ class SparseMdpPrctlHelper { storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative); + static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::models::sparse::StandardRewardModel const& intervalRewardModel, + bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative); + private: static MDPSparseModelCheckingHelperReturnType computeReachabilityRewardsHelper( Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index d0f2648c07..120fac31db 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -65,6 +65,11 @@ template class SparsePropositionalModelChecker>>; template class SparsePropositionalModelChecker>>; +template class SparsePropositionalModelChecker< + storm::models::sparse::Mdp>>; +template class SparsePropositionalModelChecker< + storm::models::sparse::Smg>>; + template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; @@ -82,5 +87,8 @@ template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; + +template class SparsePropositionalModelChecker>; +template class SparsePropositionalModelChecker>; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.h index 52a6c3c137..7de1792319 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.h +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.h @@ -8,10 +8,28 @@ namespace modelchecker { template class SparsePropositionalModelChecker : public AbstractModelChecker { + private: + // Due to a GCC bug we have to add this dummy template type here + // https://stackoverflow.com/questions/49707184/explicit-specialization-in-non-namespace-scope-does-not-compile-in-gcc + template + struct GetSolutionType { + using type = T; + }; + + template + struct GetSolutionType { + using type = double; + }; + + template + struct GetSolutionType { + using type = storm::RationalNumber; + }; + public: typedef typename SparseModelType::ValueType ValueType; typedef typename SparseModelType::RewardModelType RewardModelType; - using SolutionType = typename std::conditional, double, ValueType>::type; + using SolutionType = typename GetSolutionType::type; explicit SparsePropositionalModelChecker(SparseModelType const& model); diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index f02feee29b..8b70af8ea4 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -1,5 +1,6 @@ #pragma once +#include "storm/adapters/IntervalForward.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/models/sparse/Dtmc.h" #include "storm/solver/stateelimination/StatePriorityQueue.h" @@ -27,7 +28,7 @@ class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker typedef typename SparseDtmcModelType::RewardModelType RewardModelType; typedef typename storm::storage::FlexibleSparseMatrix::row_type FlexibleRowType; typedef typename FlexibleRowType::iterator FlexibleRowIterator; - using SolutionType = typename std::conditional, double, ValueType>::type; + using SolutionType = storm::IntervalBaseType; /*! * Creates an elimination-based model checker for the given model. diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h index 95db1271bb..9fb3228f0d 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -4,6 +4,7 @@ #include #include +#include "storm/adapters/IntervalForward.h" #include "storm/adapters/JsonForward.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" #include "storm/models/sparse/StateLabeling.h" diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index ccb39cad09..88ebbbd7e6 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -96,8 +96,10 @@ storm::storage::SparseMatrix Ctmc::comput template class Ctmc; template class Ctmc; template class Ctmc>; +template class Ctmc>; template class Ctmc; template class Ctmc; +template class Ctmc; } // namespace sparse } // namespace models } // namespace storm diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 956c4e2e0c..c4d326380f 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -65,7 +65,9 @@ void DeterministicModel::writeDotToStream(std::ostre template class DeterministicModel; template class DeterministicModel>; template class DeterministicModel; +template class DeterministicModel>; template class DeterministicModel; +template class DeterministicModel; template class DeterministicModel; } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/Dtmc.cpp b/src/storm/models/sparse/Dtmc.cpp index 29ff1bd0a3..887dceff3d 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -3,6 +3,7 @@ #include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" +#include "storm/adapters/RationalNumberForward.h" #include "storm/models/sparse/StandardRewardModel.h" namespace storm { @@ -47,7 +48,9 @@ void Dtmc::reduceToStateBasedRewards() { template class Dtmc; template class Dtmc>; template class Dtmc; +template class Dtmc>; template class Dtmc; +template class Dtmc; template class Dtmc; } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 73d18d6b2f..c5fd21397e 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -250,7 +250,9 @@ void MarkovAutomaton::printModelInformationToStream( template class MarkovAutomaton; template class MarkovAutomaton>; template class MarkovAutomaton; +template class MarkovAutomaton>; template class MarkovAutomaton; +template class MarkovAutomaton; template class MarkovAutomaton; } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index d07bbf49da..60d4f636d3 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -44,7 +44,9 @@ Mdp::Mdp(storm::storage::sparse::ModelComponents; template class Mdp>; template class Mdp; +template class Mdp>; template class Mdp; +template class Mdp; template class Mdp; } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index c07374e25d..4838cb89a2 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -643,7 +643,7 @@ bool Model::supportsParameters() const { template bool Model::supportsUncertainty() const { - return std::is_same::value; + return storm::IsIntervalType; } template @@ -728,7 +728,9 @@ std::set getAllParameters(Model; template class Model>; template class Model; +template class Model>; template class Model; +template class Model; template class Model; } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 0a256f75a4..5ee47ec3ed 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -190,8 +190,10 @@ uint_least64_t NondeterministicModel::getChoiceIndex template class NondeterministicModel; template class NondeterministicModel>; -template class NondeterministicModel; template class NondeterministicModel; +template class NondeterministicModel>; +template class NondeterministicModel; +template class NondeterministicModel; template class NondeterministicModel; } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index 69ecda855d..8f52964b25 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -156,7 +156,9 @@ std::size_t Pomdp::hash() const { template class Pomdp; template class Pomdp>; template class Pomdp; +template class Pomdp>; template class Pomdp; +template class Pomdp; template class Pomdp; } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp index 2aa8d5e57f..c381e135b7 100644 --- a/src/storm/models/sparse/Smg.cpp +++ b/src/storm/models/sparse/Smg.cpp @@ -90,7 +90,9 @@ storm::storage::BitVector Smg::computeStatesOfCoalit template class Smg; template class Smg>; template class Smg; +template class Smg>; template class Smg; +template class Smg; template class Smg; } // namespace sparse diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index bdcdf92ecd..6c8c8f03c6 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -662,6 +662,48 @@ template storm::storage::BitVector StandardRewardModel::getChoi storm::storage::SparseMatrix const& transitionMatrix) const; template class StandardRewardModel; template std::ostream& operator<< (std::ostream& out, StandardRewardModel const& rewardModel); + +template std::vector StandardRewardModel::getTotalRewardVector( + uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; +template std::vector StandardRewardModel::getTotalRewardVector( + storm::storage::SparseMatrix const& transitionMatrix) const; +template std::vector StandardRewardModel::getTotalRewardVector( + storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; +template std::vector StandardRewardModel::getTotalRewardVector( + uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; +template std::vector StandardRewardModel::getTotalRewardVector( + storm::storage::SparseMatrix const& transitionMatrix) const; +template std::vector StandardRewardModel::getTotalRewardVector( + storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; +template std::vector StandardRewardModel::getTotalActionRewardVector( + storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; +template storm::storage::BitVector StandardRewardModel::getStatesWithFilter( + storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; +template storm::storage::BitVector StandardRewardModel::getStatesWithFilter( + storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; +template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter( + storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; +template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter( + storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; +template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const& newValue); +template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalInterval const& newValue); +template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const& newValue); +template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalInterval const& newValue); +template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, + storm::storage::SparseMatrix const& transitionMatrix); +template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, + storm::storage::SparseMatrix const& transitionMatrix); +template void StandardRewardModel::reduceToStateBasedRewards( + storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); +template void StandardRewardModel::reduceToStateBasedRewards( + storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, + std::vector const* weights); +template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward( + storm::storage::SparseMatrix const& transitionMatrix) const; +template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward( + storm::storage::SparseMatrix const& transitionMatrix) const; +template class StandardRewardModel; +template std::ostream& operator<< (std::ostream& out, StandardRewardModel const& rewardModel); } // namespace sparse } // namespace models diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp index 47cc89ea67..c85bc0b163 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp @@ -63,8 +63,10 @@ storm::models::sparse::ChoiceLabeling const& StochasticTwoPlayerGame; template class StochasticTwoPlayerGame>; -template class StochasticTwoPlayerGame; template class StochasticTwoPlayerGame; +template class StochasticTwoPlayerGame>; +template class StochasticTwoPlayerGame; +template class StochasticTwoPlayerGame; template class StochasticTwoPlayerGame; } // namespace sparse diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 3fe6aa749d..3819591a75 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -135,7 +135,7 @@ void IterativeMinMaxLinearEquationSolver::setUpViOperat // The trivial row grouping minmax operator makes sense over intervals. viOperatorTriv = std::make_shared>(); viOperatorTriv->setMatrixBackwards(*this->A); - if constexpr (!std::is_same_v) { + if constexpr (!storm::IsIntervalType) { // It might be that someone is using a minmaxlinearequationsolver with an advanced VI algorithm // but is just passing a DTMC over doubles. In this case we need to populate this VI operator. // It behaves exactly the same as the trivial row grouping operator, but it is currently hardcoded @@ -168,7 +168,7 @@ template void IterativeMinMaxLinearEquationSolver::extractScheduler(std::vector& x, std::vector const& b, OptimizationDirection const& dir, UncertaintyResolutionMode uncertaintyResolutionMode, bool updateX) const { - if (std::is_same_v && this->A->hasTrivialRowGrouping()) { + if (storm::IsIntervalType && this->A->hasTrivialRowGrouping()) { // Create robust scheduler index if it doesn't exist yet if (!this->robustSchedulerIndex) { this->robustSchedulerIndex = std::vector(x.size(), 0); @@ -201,7 +201,7 @@ void IterativeMinMaxLinearEquationSolver::extractSchedu setUpViOperator(); } if (viOperatorTriv) { - if constexpr (std::is_same() && std::is_same()) { + if constexpr (storm::IsIntervalType && storm::IsIntervalType) { storm::solver::helper::SchedulerTrackingHelper schedHelper(viOperatorTriv); schedHelper.computeScheduler(x, b, dir, *this->schedulerChoices, uncertaintyResolutionMode, updateX ? &x : nullptr, this->robustSchedulerIndex); } else { @@ -218,8 +218,8 @@ template bool IterativeMinMaxLinearEquationSolver::solveInducedEquationSystem( Environment const& env, std::unique_ptr>& linearEquationSolver, std::vector const& scheduler, std::vector& x, std::vector& subB, std::vector const& originalB, OptimizationDirection dir) const { - if constexpr (std::is_same_v) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We did not implement solving induced equation systems for interval-based models outside of robust VI."); // Implementing this requires linear equation systems with different value types and solution types (or some appropriate casting) @@ -251,7 +251,7 @@ bool IterativeMinMaxLinearEquationSolver::solveInducedE for (uint64_t i = 0; i < row.getNumberOfEntries(); i++, schedulerIterator++) { if (!utility::isZero(probLeft)) { auto const& entry = rowIter[*schedulerIterator]; - auto const diameter = entry.getValue().upper() - entry.getValue().lower(); + SolutionType const diameter = entry.getValue().upper() - entry.getValue().lower(); auto const value = utility::min(probLeft, diameter); tmp[*schedulerIterator] += value; probLeft -= value; @@ -334,7 +334,7 @@ template bool IterativeMinMaxLinearEquationSolver::performPolicyIteration( Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector&& initialPolicy) const { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We did not implement policy iteration for interval-based models."); return false; } else { @@ -460,7 +460,7 @@ MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver) { + if constexpr (storm::IsIntervalType) { STORM_LOG_ASSERT(!needsLinEqSolver, "Intervals should not require a linear equation solver."); // nothing to be done; } else if (needsLinEqSolver) { @@ -561,7 +561,7 @@ template bool IterativeMinMaxLinearEquationSolver::solveEquationsOptimisticValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We did not implement optimistic value iteration for interval-based models."); return false; } else { @@ -617,7 +617,7 @@ template bool IterativeMinMaxLinearEquationSolver::solveEquationsGuessingValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We did not implement guessing value iteration for interval-based models."); return false; } else { @@ -784,8 +784,8 @@ template bool IterativeMinMaxLinearEquationSolver::solveEquationsIntervalIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if constexpr (std::is_same_v) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We did not implement intervaliteration for interval-based models"); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We did not implement interval iteration for interval-based models"); return false; } else { setUpViOperator(); @@ -827,7 +827,7 @@ template bool IterativeMinMaxLinearEquationSolver::solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SoundVI does not handle interval-based models"); return false; } else { @@ -879,7 +879,7 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation template bool IterativeMinMaxLinearEquationSolver::solveEquationsViToPi(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "ViToPi does not handle interval-based models"); return false; } @@ -914,7 +914,7 @@ template bool IterativeMinMaxLinearEquationSolver::solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational search does not handle interval-based models"); return false; } else { @@ -986,6 +986,7 @@ void IterativeMinMaxLinearEquationSolver::clearCache() template class IterativeMinMaxLinearEquationSolver; template class IterativeMinMaxLinearEquationSolver; template class IterativeMinMaxLinearEquationSolver; +template class IterativeMinMaxLinearEquationSolver; } // namespace solver } // namespace storm diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp index 51d43b1bcd..3ad3d168d9 100644 --- a/src/storm/solver/LinearEquationSolver.cpp +++ b/src/storm/solver/LinearEquationSolver.cpp @@ -148,7 +148,7 @@ template std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env) const { EquationSolverType type = env.solver().getLinearEquationSolverType(); - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not implemented interval-based linear equation solvers"); } diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 81242b0296..5ee11d5e9a 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -252,19 +252,19 @@ std::unique_ptr> GeneralMinM result = std::make_unique>( std::make_unique>()); } else if (method == MinMaxMethod::Topological) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_ERROR("Topological method not implemented for ValueType==Interval."); } else { result = std::make_unique>(); } } else if (method == MinMaxMethod::LinearProgramming || method == MinMaxMethod::ViToLp) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_ERROR("LP method not implemented for ValueType==Interval."); } else { result = std::make_unique>(storm::utility::solver::getLpSolverFactory()); } } else if (method == MinMaxMethod::Acyclic) { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { STORM_LOG_ERROR("Acyclic method not implemented for ValueType==Interval"); } else { result = std::make_unique>(); @@ -322,4 +322,8 @@ template class GeneralMinMaxLinearEquationSolverFactory; template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolverFactory; template class GeneralMinMaxLinearEquationSolverFactory; + +template class MinMaxLinearEquationSolver; +template class MinMaxLinearEquationSolverFactory; +template class GeneralMinMaxLinearEquationSolverFactory; } // namespace storm::solver diff --git a/src/storm/solver/SolveGoal.cpp b/src/storm/solver/SolveGoal.cpp index c42b8a9d8a..90d00ceff8 100644 --- a/src/storm/solver/SolveGoal.cpp +++ b/src/storm/solver/SolveGoal.cpp @@ -147,6 +147,7 @@ template class SolveGoal; template class SolveGoal; template class SolveGoal; template class SolveGoal; +template class SolveGoal; } // namespace solver } // namespace storm diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 0d9fc4337d..079bf2f0c4 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -427,7 +427,7 @@ void StandardGameSolver::multiplyAndReduce(Environment const& env, Op storm::solver::Multiplier const& multiplier, std::vector& player2ReducedResult, std::vector& player1ReducedResult, std::vector* player1SchedulerChoices, std::vector* player2SchedulerChoices) const { - multiplier.multiplyAndReduce(env, player2Dir, x, b, player2ReducedResult, player2SchedulerChoices); + multiplier.multiplyAndReduce(env, player2Dir, x, b, player2ReducedResult, UncertaintyResolutionMode::Unset, player2SchedulerChoices); if (this->player1RepresentedByMatrix()) { // Player 1 represented by matrix. diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 7f35cbb08f..1f9736902e 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -43,5 +43,6 @@ void StandardMinMaxLinearEquationSolver::setMatrix(stor template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolver; +template class StandardMinMaxLinearEquationSolver; } // namespace storm::solver diff --git a/src/storm/solver/helper/SchedulerTrackingHelper.cpp b/src/storm/solver/helper/SchedulerTrackingHelper.cpp index 13e0ba5eaa..478866794e 100644 --- a/src/storm/solver/helper/SchedulerTrackingHelper.cpp +++ b/src/storm/solver/helper/SchedulerTrackingHelper.cpp @@ -108,7 +108,7 @@ bool SchedulerTrackingHelper::compu std::vector& schedulerStorage, UncertaintyResolutionMode uncertaintyResolutionMode, std::vector* operandOut, boost::optional> const& robustIndices) const { bool robustUncertainty = false; - if (storm::IsIntervalType) { + if constexpr (storm::IsIntervalType) { robustUncertainty = isUncertaintyResolvedRobust(uncertaintyResolutionMode, dir); } @@ -135,5 +135,7 @@ template class SchedulerTrackingHelper; template class SchedulerTrackingHelper; template class SchedulerTrackingHelper; template class SchedulerTrackingHelper; +template class SchedulerTrackingHelper; +template class SchedulerTrackingHelper; } // namespace storm::solver::helper diff --git a/src/storm/solver/helper/ValueIterationHelper.cpp b/src/storm/solver/helper/ValueIterationHelper.cpp index 586b6ae9ae..512a25b3db 100644 --- a/src/storm/solver/helper/ValueIterationHelper.cpp +++ b/src/storm/solver/helper/ValueIterationHelper.cpp @@ -108,7 +108,7 @@ SolverStatus ValueIterationHelper:: MultiplicationStyle mult, UncertaintyResolutionMode const& uncertaintyResolutionMode) const { bool robustUncertainty = false; - if (storm::IsIntervalType) { + if constexpr (storm::IsIntervalType) { robustUncertainty = isUncertaintyResolvedRobust(uncertaintyResolutionMode, Dir); } @@ -126,7 +126,7 @@ SolverStatus ValueIterationHelper:: std::function const& iterationCallback, MultiplicationStyle mult, UncertaintyResolutionMode const& uncertaintyResolutionMode) const { - if (storm::IsIntervalType) { + if constexpr (storm::IsIntervalType) { STORM_LOG_THROW(uncertaintyResolutionMode != UncertaintyResolutionMode::Unset, storm::exceptions::IllegalFunctionCallException, "Uncertainty resolution mode must be set for uncertain (interval) models."); STORM_LOG_THROW(dir.has_value() || (uncertaintyResolutionMode != UncertaintyResolutionMode::Robust && @@ -172,5 +172,7 @@ template class ValueIterationHelper; template class ValueIterationHelper; template class ValueIterationHelper; template class ValueIterationHelper; +template class ValueIterationHelper; +template class ValueIterationHelper; } // namespace storm::solver::helper diff --git a/src/storm/solver/helper/ValueIterationOperator.cpp b/src/storm/solver/helper/ValueIterationOperator.cpp index 4ab2674bf5..bd8a856f53 100644 --- a/src/storm/solver/helper/ValueIterationOperator.cpp +++ b/src/storm/solver/helper/ValueIterationOperator.cpp @@ -33,7 +33,7 @@ void ValueIterationOperator::setMat matrixColumns.reserve(matrix.getNonzeroEntryCount() + numRows + 1); // matrixColumns also contain indications for when a row(group) starts // hasOnlyConstants is only used for Interval matrices, currently only populated for iMCs - if constexpr (std::is_same::value) { + if constexpr (storm::IsIntervalType) { applyCache.hasOnlyConstants.clear(); applyCache.hasOnlyConstants.grow(matrix.getRowCount()); } @@ -53,7 +53,7 @@ void ValueIterationOperator::setMat matrixColumns.back() = StartOfRowGroupIndicator; // This is the start of the next row group } } else { - if constexpr (std::is_same::value) { + if constexpr (storm::IsIntervalType) { matrixColumns.push_back(StartOfRowIndicator); // Indicate start of first row for (auto rowIndex : indexRange(0, numRows)) { bool hasOnlyConstants = true; @@ -204,5 +204,7 @@ template class ValueIterationOperator; template class ValueIterationOperator; template class ValueIterationOperator; template class ValueIterationOperator; +template class ValueIterationOperator; +template class ValueIterationOperator; } // namespace storm::solver::helper diff --git a/src/storm/solver/helper/ValueIterationOperator.h b/src/storm/solver/helper/ValueIterationOperator.h index f14d976f6f..257f6c95fe 100644 --- a/src/storm/solver/helper/ValueIterationOperator.h +++ b/src/storm/solver/helper/ValueIterationOperator.h @@ -241,6 +241,15 @@ class ValueIterationOperator { return {(*offsets.first)[offsetIndex], offsets.second}; } + template + OpT robustInitializeRowRes(std::vector const&, OffT const& offsets, uint64_t offsetIndex) const { + if constexpr (RobustDirection == OptimizationDirection::Maximize) { + return offsets.upper(); + } else { + return offsets.lower(); + } + } + template OpT robustInitializeRowRes(std::vector const&, std::vector const& offsets, uint64_t offsetIndex) const { if constexpr (RobustDirection == OptimizationDirection::Maximize) { @@ -272,7 +281,7 @@ class ValueIterationOperator { template auto applyRow(std::vector::const_iterator& matrixColumnIt, typename std::vector::const_iterator& matrixValueIt, OperandType const& operand, OffsetType const& offsets, uint64_t offsetIndex) const { - if constexpr (std::is_same_v) { + if constexpr (storm::IsIntervalType) { return applyRowRobust(matrixColumnIt, matrixValueIt, operand, offsets, offsetIndex); } else { return applyRowStandard(matrixColumnIt, matrixValueIt, operand, offsets, offsetIndex); @@ -312,13 +321,13 @@ class ValueIterationOperator { auto applyRowRobust(std::vector::const_iterator& matrixColumnIt, typename std::vector::const_iterator& matrixValueIt, OperandType const& operand, OffsetType const& offsets, uint64_t offsetIndex) const { STORM_LOG_ASSERT(*matrixColumnIt >= StartOfRowIndicator, "VI Operator in invalid state."); - auto result{robustInitializeRowRes(operand, offsets, offsetIndex)}; + SolutionType result{robustInitializeRowRes(operand, offsets, offsetIndex)}; applyCache.robustOrder.clear(); if (applyCache.hasOnlyConstants.size() > 0 && applyCache.hasOnlyConstants.get(offsetIndex)) { for (++matrixColumnIt; *matrixColumnIt < StartOfRowIndicator; ++matrixColumnIt, ++matrixValueIt) { - auto const lower = matrixValueIt->lower(); + SolutionType const lower = matrixValueIt->lower(); if constexpr (isPair::value) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Value Iteration is not implemented with pairs and interval-models."); // Notice the unclear semantics here in terms of how to order things. @@ -332,7 +341,7 @@ class ValueIterationOperator { SolutionType remainingValue{storm::utility::one()}; uint64_t orderCounter = 0; for (++matrixColumnIt; *matrixColumnIt < StartOfRowIndicator; ++matrixColumnIt, ++matrixValueIt, ++orderCounter) { - auto const lower = matrixValueIt->lower(); + SolutionType const lower = matrixValueIt->lower(); if constexpr (isPair::value) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Value Iteration is not implemented with pairs and interval-models."); // Notice the unclear semantics here in terms of how to order things. @@ -340,8 +349,8 @@ class ValueIterationOperator { result += operand[*matrixColumnIt] * lower; } remainingValue -= lower; - auto const diameter = matrixValueIt->upper() - lower; - if (!storm::utility::isZero(diameter)) { + SolutionType const diameter = static_cast(-lower + matrixValueIt->upper()); + if (!storm::utility::isZero(diameter)) { applyCache.robustOrder.emplace_back(operand[*matrixColumnIt], std::make_pair(diameter, orderCounter)); } } @@ -353,7 +362,7 @@ class ValueIterationOperator { std::sort(applyCache.robustOrder.begin(), applyCache.robustOrder.end(), cmp); for (auto const& pair : applyCache.robustOrder) { - auto availableMass = std::min(pair.second.first, remainingValue); + SolutionType availableMass = std::min(pair.second.first, remainingValue); result += availableMass * pair.first; remainingValue -= availableMass; if (storm::utility::isZero(remainingValue)) { @@ -462,8 +471,14 @@ class ValueIterationOperator { storage::BitVector hasOnlyConstants; }; + template + struct ApplyCache { + mutable std::vector>> robustOrder; + storage::BitVector hasOnlyConstants; + }; + /*! - * Cache for robust value iteration, empty struct for other ValueTypes than storm::Interval. + * Cache for robust value iteration, empty struct for other ValueTypes than storm::Interval and storm::RationalInterval. */ ApplyCache applyCache; diff --git a/src/storm/solver/multiplier/Multiplier.cpp b/src/storm/solver/multiplier/Multiplier.cpp index e12fb09b4a..45acc9d578 100644 --- a/src/storm/solver/multiplier/Multiplier.cpp +++ b/src/storm/solver/multiplier/Multiplier.cpp @@ -1,4 +1,5 @@ #include "storm/solver/multiplier/Multiplier.h" +#include #include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -17,30 +18,34 @@ namespace storm { namespace solver { -template -Multiplier::Multiplier(storm::storage::SparseMatrix const& matrix) : matrix(matrix) { +template +Multiplier::Multiplier(storm::storage::SparseMatrix const& matrix) : matrix(matrix) { // Intentionally left empty. } -template -void Multiplier::clearCache() const { +template +void Multiplier::clearCache() const { cachedVector.reset(); } -template -void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, - std::vector const* b, std::vector& result, std::vector* choices) const { - multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices); +template +void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, + std::vector const* b, std::vector& result, + UncertaintyResolutionMode const& uncertaintyResolutionMode, + std::vector* choices) const { + multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, uncertaintyResolutionMode, choices); } -template -void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, - std::vector const* b, std::vector* choices, bool backwards) const { +template +void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, + std::vector const* b, std::vector* choices, + bool backwards) const { multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards); } -template -void Multiplier::repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const { +template +void Multiplier::repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, + uint64_t n) const { storm::utility::ProgressMeasurement progress("multiplications"); progress.setMaxCount(n); progress.startNewMeasurement(0); @@ -54,15 +59,16 @@ void Multiplier::repeatedMultiply(Environment const& env, std::vector } } -template -void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, - std::vector const* b, uint64_t n) const { +template +void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, + std::vector const* b, uint64_t n, + UncertaintyResolutionMode const& uncertaintyResolutionMode) const { storm::utility::ProgressMeasurement progress("multiplications"); progress.setMaxCount(n); progress.startNewMeasurement(0); for (uint64_t i = 0; i < n; ++i) { progress.updateProgress(i); - multiplyAndReduce(env, dir, x, b, x); + multiplyAndReduce(env, dir, x, b, x, uncertaintyResolutionMode); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications"); break; @@ -70,16 +76,18 @@ void Multiplier::repeatedMultiplyAndReduce(Environment const& env, Op } } -template -void Multiplier::repeatedMultiplyAndReduceWithFactor(Environment const& env, OptimizationDirection const& dir, std::vector& x, - std::vector const* b, uint64_t n, ValueType factor) const { +template +void Multiplier::repeatedMultiplyAndReduceWithFactor(Environment const& env, OptimizationDirection const& dir, + std::vector& x, std::vector const* b, uint64_t n, + SolutionType factor, + UncertaintyResolutionMode const& uncertaintyResolutionMode) const { storm::utility::ProgressMeasurement progress("multiplications"); progress.setMaxCount(n); progress.startNewMeasurement(0); for (uint64_t i = 0; i < n; ++i) { progress.updateProgress(i); - std::transform(x.begin(), x.end(), x.begin(), [factor](ValueType& c) { return c * factor; }); - multiplyAndReduce(env, dir, x, b, x); + std::transform(x.begin(), x.end(), x.begin(), [factor](SolutionType& c) { return c * factor; }); + multiplyAndReduce(env, dir, x, b, x, uncertaintyResolutionMode); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications"); break; @@ -87,15 +95,15 @@ void Multiplier::repeatedMultiplyAndReduceWithFactor(Environment cons } } -template -void Multiplier::repeatedMultiplyWithFactor(Environment const& env, std::vector& x, std::vector const* b, uint64_t n, - ValueType factor) const { +template +void Multiplier::repeatedMultiplyWithFactor(Environment const& env, std::vector& x, std::vector const* b, + uint64_t n, SolutionType factor) const { storm::utility::ProgressMeasurement progress("multiplications"); progress.setMaxCount(n); progress.startNewMeasurement(0); for (uint64_t i = 0; i < n; ++i) { progress.updateProgress(i); - std::transform(x.begin(), x.end(), x.begin(), [factor](ValueType& c) { return c * factor; }); + std::transform(x.begin(), x.end(), x.begin(), [factor](SolutionType& c) { return c * factor; }); multiply(env, x, b, x); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications"); @@ -104,39 +112,44 @@ void Multiplier::repeatedMultiplyWithFactor(Environment const& env, s } } -template - -std::vector& Multiplier::provideCachedVector(uint64_t size) const { +template +std::vector& Multiplier::provideCachedVector(uint64_t size) const { if (this->cachedVector) { this->cachedVector->resize(size); } else { - this->cachedVector = std::make_unique>(size); + this->cachedVector = std::make_unique>(size); } return *this->cachedVector; } -template -std::unique_ptr> MultiplierFactory::create(Environment const& env, storm::storage::SparseMatrix const& matrix) { +template +std::unique_ptr> MultiplierFactory::create(Environment const& env, + storm::storage::SparseMatrix const& matrix) { auto type = env.solver().multiplier().getType(); // Adjust the type if the ValueType is not supported - if (type == MultiplierType::ViOperator && (std::is_same_v || std::is_same_v)) { + if (type == MultiplierType::ViOperator && + (std::is_same_v || (storm::IsIntervalType && storm::IsIntervalType))) { STORM_LOG_INFO("Switching multiplier type from 'vioperator' to 'native' because the given ValueType is not supported by the VI Operator multiplier."); type = MultiplierType::Native; } switch (type) { case MultiplierType::ViOperator: - if constexpr (std::is_same_v || std::is_same_v) { + if constexpr (std::is_same_v || (storm::IsIntervalType && storm::IsIntervalType)) { throw storm::exceptions::NotImplementedException() << "VI Operator multiplier not supported with given value type."; } if (matrix.hasTrivialRowGrouping()) { - return std::make_unique>(matrix); + return std::make_unique>(matrix); } else { - return std::make_unique>(matrix); + return std::make_unique>(matrix); } case MultiplierType::Native: - return std::make_unique>(matrix); + if constexpr (std::is_same_v) { + return std::make_unique>(matrix); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Native multiplier not implemented for unequal ValueType and SolutionType."); + } } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType"); } @@ -149,6 +162,10 @@ template class Multiplier; template class MultiplierFactory; template class Multiplier; template class MultiplierFactory; +template class Multiplier; +template class MultiplierFactory; +template class Multiplier; +template class MultiplierFactory; } // namespace solver } // namespace storm diff --git a/src/storm/solver/multiplier/Multiplier.h b/src/storm/solver/multiplier/Multiplier.h index fe8e0f7d4a..b9c8e6a244 100644 --- a/src/storm/solver/multiplier/Multiplier.h +++ b/src/storm/solver/multiplier/Multiplier.h @@ -5,6 +5,7 @@ #include "storm/solver/MultiplicationStyle.h" #include "storm/solver/OptimizationDirection.h" +#include "storm/solver/UncertaintyResolutionMode.h" namespace storm { @@ -17,7 +18,7 @@ class SparseMatrix; namespace solver { -template +template class Multiplier { public: Multiplier(storm::storage::SparseMatrix const& matrix); @@ -39,7 +40,8 @@ class Multiplier { * @param result The target vector into which to write the multiplication result. Its length must be equal * to the number of rows of A. Can be the same as the x vector. */ - virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const = 0; + virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, + std::vector& result) const = 0; /*! * Performs a matrix-vector multiplication in gauss-seidel style. @@ -50,7 +52,7 @@ class Multiplier { * to the number of rows of A. * @param backwards if true, the iterations will be performed beginning from the last row and ending at the first row. */ - virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const = 0; + virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const = 0; /*! * Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups @@ -64,12 +66,15 @@ class Multiplier { * to the number of rows of A. * @param result The target vector into which to write the multiplication result. Its length must be equal * to the number of rows of A. Can be the same as the x vector. + * @param uncertaintyResolutionMode The mode according to which to resolve uncertainty in the reduction step. * @param choices If given, the choices made in the reduction process are written to this vector. */ - void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, - std::vector& result, std::vector* choices = nullptr) const; + void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, + std::vector& result, UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset, + std::vector* choices = nullptr) const; virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, - std::vector const& x, std::vector const* b, std::vector& result, + std::vector const& x, std::vector const* b, std::vector& result, + UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset, std::vector* choices = nullptr) const = 0; /*! @@ -87,10 +92,10 @@ class Multiplier { * @param choices If given, the choices made in the reduction process are written to this vector. * @param backwards if true, the iterations will be performed beginning from the last rowgroup and ending at the first rowgroup. */ - void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, + void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const; virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, - std::vector& x, std::vector const* b, std::vector* choices = nullptr, + std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const = 0; /*! @@ -104,7 +109,7 @@ class Multiplier { * to the number of rows of A. * @param n The number of times to perform the multiplication. */ - void repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const; + void repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const; /*! * Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups @@ -118,9 +123,10 @@ class Multiplier { * @param result The target vector into which to write the multiplication result. Its length must be equal * to the number of rows of A. * @param n The number of times to perform the multiplication. + * @param uncertaintyResolutionMode The mode according to which to resolve uncertainty in the reduction step. */ - void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, - uint64_t n) const; + void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, + uint64_t n, UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset) const; /*! * Performs repeated matrix-vector multiplication x' = A*(factor * x) + b. Vector x is scaled by factor in each iteration. * @@ -133,7 +139,8 @@ class Multiplier { * @param n The number of times to perform the multiplication. * @param factor The scalar to multiply with in each iteration. */ - void repeatedMultiplyWithFactor(Environment const& env, std::vector& x, std::vector const* b, uint64_t n, ValueType factor) const; + void repeatedMultiplyWithFactor(Environment const& env, std::vector& x, std::vector const* b, uint64_t n, + SolutionType factor) const; /*! * Performs repeated matrix-vector multiplication x' = A*(factor * x) + b, minimizes/maximizes over the row groups @@ -147,25 +154,27 @@ class Multiplier { * @param result The target vector into which to write the multiplication result. Its length must be equal * to the number of rows of A. * @param n The number of times to perform the multiplication. + * @param uncertaintyResolutionMode The mode according to which to resolve uncertainty in the reduction step. * @param factor The scalar to multiply with in each iteration. */ - void repeatedMultiplyAndReduceWithFactor(Environment const& env, OptimizationDirection const& dir, std::vector& x, - std::vector const* b, uint64_t n, ValueType factor) const; + void repeatedMultiplyAndReduceWithFactor(Environment const& env, OptimizationDirection const& dir, std::vector& x, + std::vector const* b, uint64_t n, SolutionType factor, + UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset) const; protected: - std::vector& provideCachedVector(uint64_t size) const; + std::vector& provideCachedVector(uint64_t size) const; - mutable std::unique_ptr> cachedVector; + mutable std::unique_ptr> cachedVector; storm::storage::SparseMatrix const& matrix; }; -template +template class MultiplierFactory { public: MultiplierFactory() = default; ~MultiplierFactory() = default; - std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix); + std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix); }; } // namespace solver diff --git a/src/storm/solver/multiplier/NativeMultiplier.cpp b/src/storm/solver/multiplier/NativeMultiplier.cpp index 876f7eea6e..50b41b559b 100644 --- a/src/storm/solver/multiplier/NativeMultiplier.cpp +++ b/src/storm/solver/multiplier/NativeMultiplier.cpp @@ -4,6 +4,8 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/storage/SparseMatrix.h" #include "storm/utility/macros.h" @@ -41,7 +43,10 @@ void NativeMultiplier::multiplyGaussSeidel(Environment const& env, st template void NativeMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, - std::vector* choices) const { + UncertaintyResolutionMode const& uncertaintyResolutionMode, std::vector* choices) const { + STORM_LOG_THROW(uncertaintyResolutionMode == UncertaintyResolutionMode::Unset, storm::exceptions::NotSupportedException, + "Uncertainty resolution modes other than 'Unset' are not supported by the native multiplier."); + std::vector* target = &result; if (&x == &result) { target = &this->provideCachedVector(x.size()); diff --git a/src/storm/solver/multiplier/NativeMultiplier.h b/src/storm/solver/multiplier/NativeMultiplier.h index ad722fe89c..fbecd2e861 100644 --- a/src/storm/solver/multiplier/NativeMultiplier.h +++ b/src/storm/solver/multiplier/NativeMultiplier.h @@ -23,6 +23,7 @@ class NativeMultiplier : public Multiplier { virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const override; virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, + UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset, std::vector* choices = nullptr) const override; virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, diff --git a/src/storm/solver/multiplier/ViOperatorMultiplier.cpp b/src/storm/solver/multiplier/ViOperatorMultiplier.cpp index fce6106637..59af83eb62 100644 --- a/src/storm/solver/multiplier/ViOperatorMultiplier.cpp +++ b/src/storm/solver/multiplier/ViOperatorMultiplier.cpp @@ -1,7 +1,9 @@ #include "ViOperatorMultiplier.h" +#include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/solver/OptimizationDirection.h" #include "storm/solver/helper/ValueIterationOperator.h" #include "storm/storage/SparseMatrix.h" #include "storm/utility/Extremum.h" @@ -142,14 +144,15 @@ class PlainMultiplicationBackend { } // namespace detail -template -ViOperatorMultiplier::ViOperatorMultiplier(storm::storage::SparseMatrix const& matrix) - : Multiplier(matrix) { +template +ViOperatorMultiplier::ViOperatorMultiplier(storm::storage::SparseMatrix const& matrix) + : Multiplier(matrix) { // Intentionally left empty. } -template -typename ViOperatorMultiplier::ViOpT& ViOperatorMultiplier::initialize() const { +template +typename ViOperatorMultiplier::ViOpT& +ViOperatorMultiplier::initialize() const { if (!viOperatorFwd) { return initialize(false); // default to backward operator } else { @@ -157,8 +160,9 @@ typename ViOperatorMultiplier::ViOpT& ViOperatorM } } -template -typename ViOperatorMultiplier::ViOpT& ViOperatorMultiplier::initialize(bool backwards) const { +template +typename ViOperatorMultiplier::ViOpT& +ViOperatorMultiplier::initialize(bool backwards) const { auto& viOp = backwards ? viOperatorBwd : viOperatorFwd; if (!viOp) { viOp = std::make_unique(); @@ -171,9 +175,9 @@ typename ViOperatorMultiplier::ViOpT& ViOperatorM return *viOp; } -template -void ViOperatorMultiplier::multiply(Environment const& env, std::vector const& x, std::vector const* b, - std::vector& result) const { +template +void ViOperatorMultiplier::multiply(Environment const& env, std::vector const& x, + std::vector const* b, std::vector& result) const { if (&result == &x) { auto& tmpResult = this->provideCachedVector(x.size()); multiply(env, x, b, tmpResult); @@ -181,7 +185,7 @@ void ViOperatorMultiplier::multiply(Environment c return; } auto const& viOp = initialize(); - detail::PlainMultiplicationBackend backend(result); + detail::PlainMultiplicationBackend backend(result); // Below, we just add 'result' as a dummy argument to the apply method. // The backend already takes care of filling the result vector while processing the rows. if (b) { @@ -191,12 +195,12 @@ void ViOperatorMultiplier::multiply(Environment c } } -template -void ViOperatorMultiplier::multiplyGaussSeidel(Environment const& /*env*/, std::vector& x, - std::vector const* b, bool backwards) const { +template +void ViOperatorMultiplier::multiplyGaussSeidel(Environment const& /*env*/, std::vector& x, + std::vector const* b, bool backwards) const { STORM_LOG_THROW(TrivialRowGrouping, storm::exceptions::NotSupportedException, "This multiplier does not support multiplications without reduction when invoked with non-trivial row groups"); - detail::MultiplierBackend backend; + detail::MultiplierBackend backend; auto const& viOp = initialize(backwards); if (b) { viOp.applyInPlace(x, *b, backend); @@ -205,51 +209,69 @@ void ViOperatorMultiplier::multiplyGaussSeidel(En } } -template -void ViOperatorMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, - std::vector const& rowGroupIndices, std::vector const& x, - std::vector const* b, std::vector& result, - std::vector* choices) const { +template +void ViOperatorMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, + std::vector const& rowGroupIndices, + std::vector const& x, std::vector const* b, + std::vector& result, + UncertaintyResolutionMode const& uncertaintyResolutionMode, + std::vector* choices) const { if (&result == &x) { auto& tmpResult = this->provideCachedVector(x.size()); - multiplyAndReduce(env, dir, rowGroupIndices, x, b, tmpResult, choices); + multiplyAndReduce(env, dir, rowGroupIndices, x, b, tmpResult, uncertaintyResolutionMode, choices); std::swap(result, tmpResult); return; } STORM_LOG_THROW(&rowGroupIndices == &this->matrix.getRowGroupIndices(), storm::exceptions::NotSupportedException, "The row group indices must be the same as the ones stored in the matrix of this multiplier"); auto const& viOp = initialize(); - auto apply = [&](BT& backend) { - if (b) { - viOp.apply(x, result, *b, backend); + + auto applyRobustDirection = [&](BT& backend, OffsetType const& offset) { + bool robustUncertainty = false; + if constexpr (storm::IsIntervalType) { + robustUncertainty = isUncertaintyResolvedRobust(uncertaintyResolutionMode, dir); + } + + if (robustUncertainty) { + viOp.template applyRobust(x, result, offset, backend); } else { - viOp.apply(x, result, storm::utility::zero(), backend); + viOp.template applyRobust(x, result, offset, backend); } }; - if (storm::solver::minimize(dir)) { - if (choices) { - detail::MultiplierBackend backend(*choices, this->matrix.getRowGroupIndices()); - apply(backend); + + auto applyBackend = [&](OffsetType const& offset) { + if (storm::solver::minimize(dir)) { + if (choices) { + detail::MultiplierBackend backend(*choices, + this->matrix.getRowGroupIndices()); + applyRobustDirection.template operator()(backend, offset); + } else { + detail::MultiplierBackend backend; + applyRobustDirection.template operator()(backend, offset); + } } else { - detail::MultiplierBackend backend; - apply(backend); + if (choices) { + detail::MultiplierBackend backend(*choices, + this->matrix.getRowGroupIndices()); + applyRobustDirection.template operator()(backend, offset); + } else { + detail::MultiplierBackend backend; + applyRobustDirection.template operator()(backend, offset); + } } + }; + + if (b) { + applyBackend(*b); } else { - if (choices) { - detail::MultiplierBackend backend(*choices, this->matrix.getRowGroupIndices()); - apply(backend); - } else { - detail::MultiplierBackend backend; - apply(backend); - } + applyBackend(storm::utility::zero()); } } -template -void ViOperatorMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, - std::vector const& rowGroupIndices, std::vector& x, - std::vector const* b, std::vector* choices, - bool backwards) const { +template +void ViOperatorMultiplier::multiplyAndReduceGaussSeidel( + Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, + std::vector const* b, std::vector* choices, bool backwards) const { STORM_LOG_THROW(&rowGroupIndices == &this->matrix.getRowGroupIndices(), storm::exceptions::NotSupportedException, "The row group indices must be the same as the ones stored in the matrix of this multiplier"); auto const& viOp = initialize(backwards); @@ -262,28 +284,28 @@ void ViOperatorMultiplier::multiplyAndReduceGauss }; if (storm::solver::minimize(dir)) { if (choices) { - detail::MultiplierBackend backend(*choices, this->matrix.getRowGroupIndices()); + detail::MultiplierBackend backend(*choices, this->matrix.getRowGroupIndices()); apply(backend); } else { - detail::MultiplierBackend backend; + detail::MultiplierBackend backend; apply(backend); } } else { if (choices) { - detail::MultiplierBackend backend(*choices, this->matrix.getRowGroupIndices()); + detail::MultiplierBackend backend(*choices, this->matrix.getRowGroupIndices()); apply(backend); } else { - detail::MultiplierBackend backend; + detail::MultiplierBackend backend; apply(backend); } } } -template -void ViOperatorMultiplier::clearCache() const { +template +void ViOperatorMultiplier::clearCache() const { viOperatorBwd.reset(); viOperatorFwd.reset(); - Multiplier::clearCache(); + Multiplier::clearCache(); }; template class ViOperatorMultiplier; @@ -292,4 +314,10 @@ template class ViOperatorMultiplier; template class ViOperatorMultiplier; template class ViOperatorMultiplier; +template class ViOperatorMultiplier; +template class ViOperatorMultiplier; + +template class ViOperatorMultiplier; +template class ViOperatorMultiplier; + } // namespace storm::solver diff --git a/src/storm/solver/multiplier/ViOperatorMultiplier.h b/src/storm/solver/multiplier/ViOperatorMultiplier.h index 209ff9ee01..983e02e573 100644 --- a/src/storm/solver/multiplier/ViOperatorMultiplier.h +++ b/src/storm/solver/multiplier/ViOperatorMultiplier.h @@ -14,25 +14,27 @@ class SparseMatrix; namespace solver { -template -class ViOperatorMultiplier : public Multiplier { +template +class ViOperatorMultiplier : public Multiplier { public: ViOperatorMultiplier(storm::storage::SparseMatrix const& matrix); virtual ~ViOperatorMultiplier() = default; - virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, - std::vector& result) const override; - virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const override; + virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, + std::vector& result) const override; + virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, + bool backwards = true) const override; virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, - std::vector const& x, std::vector const* b, std::vector& result, + std::vector const& x, std::vector const* b, std::vector& result, + UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset, std::vector* choices = nullptr) const override; virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, - std::vector& x, std::vector const* b, std::vector* choices = nullptr, + std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const override; virtual void clearCache() const override; private: - using ViOpT = storm::solver::helper::ValueIterationOperator; + using ViOpT = storm::solver::helper::ValueIterationOperator; ViOpT& initialize() const; ViOpT& initialize(bool backwards) const; diff --git a/src/storm/storage/Distribution.cpp b/src/storm/storage/Distribution.cpp index 8ed053f11e..77b771e9f3 100644 --- a/src/storm/storage/Distribution.cpp +++ b/src/storm/storage/Distribution.cpp @@ -230,5 +230,10 @@ template std::ostream& operator<<(std::ostream& out, Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); +template class Distribution; +template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); +template class Distribution; +template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); + } // namespace storage } // namespace storm diff --git a/src/storm/storage/MaximalEndComponentDecomposition.cpp b/src/storm/storage/MaximalEndComponentDecomposition.cpp index 1df4402f1d..6e7763f048 100644 --- a/src/storm/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storm/storage/MaximalEndComponentDecomposition.cpp @@ -252,6 +252,10 @@ template class MaximalEndComponentDecomposition; template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition( storm::models::sparse::NondeterministicModel const& model); +template class MaximalEndComponentDecomposition; +template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition( + storm::models::sparse::NondeterministicModel const& model); + template class MaximalEndComponentDecomposition; template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition( storm::models::sparse::NondeterministicModel const& model); diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index a5db7a903c..1dacf8d86d 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -391,6 +391,7 @@ template class Scheduler; template class Scheduler; template class Scheduler; template class Scheduler; +template class Scheduler; } // namespace storage } // namespace storm diff --git a/src/storm/storage/SchedulerChoice.cpp b/src/storm/storage/SchedulerChoice.cpp index 3c89c96efc..668052c88b 100644 --- a/src/storm/storage/SchedulerChoice.cpp +++ b/src/storm/storage/SchedulerChoice.cpp @@ -75,6 +75,8 @@ template class SchedulerChoice; template std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); template class SchedulerChoice; template std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); +template class SchedulerChoice; +template std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); } // namespace storage } // namespace storm diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 249411c247..e2808688c8 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -672,15 +672,20 @@ typename SparseMatrix::index_type SparseMatrix::getEntryCo template typename SparseMatrix::index_type SparseMatrix::getRowGroupEntryCount(index_type const group) const { - index_type result = 0; if (!this->hasTrivialRowGrouping()) { + index_type result = 0; for (auto row : this->getRowGroupIndices(group)) { result += (this->rowIndications[row + 1] - this->rowIndications[row]); } + return result; } else { - result += (this->rowIndications[group + 1] - this->rowIndications[group]); + return (this->rowIndications[group + 1] - this->rowIndications[group]); } - return result; +} + +template +typename SparseMatrix::index_type SparseMatrix::getRowEntryCount(index_type const row) const { + return (this->rowIndications[row + 1] - this->rowIndications[row]); } template @@ -2582,5 +2587,19 @@ template bool SparseMatrix::isSubmatrixOf(SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; +// Rational Intervals +template std::vector SparseMatrix::getPointwiseProductRowSumVector( + storm::storage::SparseMatrix const& otherMatrix) const; +template class MatrixEntry::index_type, RationalInterval>; +template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, RationalInterval> const& entry); +template class SparseMatrixBuilder; +template class SparseMatrix; +template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); +template std::vector SparseMatrix::getPointwiseProductRowSumVector( + storm::storage::SparseMatrix const& otherMatrix) const; +template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + +template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + } // namespace storage } // namespace storm diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 6dc7a725c5..a10511faa0 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -532,6 +532,13 @@ class SparseMatrix { */ index_type getRowGroupEntryCount(index_type const group) const; + /*! + * Returns the number of entries in the given row of the matrix. + * @param row Which row + * @return Number of entries + */ + index_type getRowEntryCount(index_type const row) const; + /*! * Returns the cached number of nonzero entries in the matrix. * diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp index 48808a2448..507339d3e7 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp @@ -343,5 +343,6 @@ template class StronglyConnectedComponentDecomposition; template class StronglyConnectedComponentDecomposition; template class StronglyConnectedComponentDecomposition; template class StronglyConnectedComponentDecomposition; +template class StronglyConnectedComponentDecomposition; } // namespace storm::storage diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index 7f2d19b3c0..3de2e01489 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -135,9 +135,11 @@ MemoryStructure MemoryStructureBuilder::buildTrivial template class MemoryStructureBuilder; template class MemoryStructureBuilder>; +template class MemoryStructureBuilder>; template class MemoryStructureBuilder; template class MemoryStructureBuilder; template class MemoryStructureBuilder; +template class MemoryStructureBuilder; } // namespace storage } // namespace storm diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index fbb85aa97d..6bcea8b21a 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -571,9 +571,11 @@ SparseModelMemoryProductReverseData SparseModelMemoryProduct; template class SparseModelMemoryProduct>; +template class SparseModelMemoryProduct>; template class SparseModelMemoryProduct; template class SparseModelMemoryProduct; template class SparseModelMemoryProduct; +template class SparseModelMemoryProduct; } // namespace storage } // namespace storm diff --git a/src/storm/transformer/AddUncertainty.cpp b/src/storm/transformer/AddUncertainty.cpp index 64713ccfa1..e750f34089 100644 --- a/src/storm/transformer/AddUncertainty.cpp +++ b/src/storm/transformer/AddUncertainty.cpp @@ -8,6 +8,7 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/storage/SparseMatrix.h" +#include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -17,35 +18,42 @@ template AddUncertainty::AddUncertainty(std::shared_ptr> const& originalModel) : origModel(originalModel) {} template -std::shared_ptr> AddUncertainty::transform(double additiveUncertainty, double minimalTransitionProbability) { +std::shared_ptr::IntervalType>> AddUncertainty::transform( + ValueType additiveUncertainty, ValueType minimalTransitionProbability, std::optional maxSuccessors) { // we first build the matrix and later copy the row grouping. auto newMatrixBuilder = - storage::SparseMatrixBuilder(origModel->getTransitionMatrix().getRowCount(), origModel->getTransitionMatrix().getColumnCount(), - origModel->getTransitionMatrix().getNonzeroEntryCount(), true, false); + storage::SparseMatrixBuilder(origModel->getTransitionMatrix().getRowCount(), origModel->getTransitionMatrix().getColumnCount(), + origModel->getTransitionMatrix().getNonzeroEntryCount(), true, false); // Build transition matrix (without row grouping) for (uint64_t rowIndex = 0; rowIndex < origModel->getTransitionMatrix().getRowCount(); ++rowIndex) { - for (auto const& entry : origModel->getTransitionMatrix().getRow(rowIndex)) { - newMatrixBuilder.addNextValue(rowIndex, entry.getColumn(), addUncertainty(entry.getValue(), additiveUncertainty, minimalTransitionProbability)); + if (!maxSuccessors.has_value() || origModel->getTransitionMatrix().getRowEntryCount(rowIndex) <= maxSuccessors.value()) { + for (auto const& entry : origModel->getTransitionMatrix().getRow(rowIndex)) { + newMatrixBuilder.addNextValue(rowIndex, entry.getColumn(), addUncertainty(entry.getValue(), additiveUncertainty, minimalTransitionProbability)); + } + } else { + for (auto const& entry : origModel->getTransitionMatrix().getRow(rowIndex)) { + newMatrixBuilder.addNextValue(rowIndex, entry.getColumn(), storm::utility::convertNumber(entry.getValue())); + } } } - storm::storage::sparse::ModelComponents modelComponents(newMatrixBuilder.build(), origModel->getStateLabeling()); + storm::storage::sparse::ModelComponents modelComponents(newMatrixBuilder.build(), origModel->getStateLabeling()); if (!origModel->getTransitionMatrix().hasTrivialRowGrouping()) { modelComponents.transitionMatrix.setRowGroupIndices(origModel->getTransitionMatrix().getRowGroupIndices()); } // Change value type of standard reward model. - std::unordered_map> newRewardModels; + std::unordered_map> newRewardModels; for (auto const& rewModel : origModel->getRewardModels()) { auto const& oldRewModel = rewModel.second; - std::optional> stateRewards; - std::optional> stateActionRewards; + std::optional> stateRewards; + std::optional> stateActionRewards; if (oldRewModel.hasStateRewards()) { - stateRewards = utility::vector::convertNumericVector(oldRewModel.getStateRewardVector()); + stateRewards = utility::vector::convertNumericVector(oldRewModel.getStateRewardVector()); } if (oldRewModel.hasStateActionRewards()) { - stateActionRewards = utility::vector::convertNumericVector(oldRewModel.getStateActionRewardVector()); + stateActionRewards = utility::vector::convertNumericVector(oldRewModel.getStateActionRewardVector()); } STORM_LOG_THROW(!oldRewModel.hasTransitionRewards(), exceptions::NotImplementedException, "Transition rewards are not supported."); - models::sparse::StandardRewardModel newRewModel(std::move(stateRewards), std::move(stateActionRewards)); + models::sparse::StandardRewardModel newRewModel(std::move(stateRewards), std::move(stateActionRewards)); newRewardModels.emplace(rewModel.first, std::move(newRewModel)); } @@ -57,27 +65,28 @@ std::shared_ptr> AddUncertaintygetType()) { case storm::models::ModelType::Dtmc: - return std::make_shared>(std::move(modelComponents)); + return std::make_shared>(std::move(modelComponents)); case storm::models::ModelType::Mdp: - return std::make_shared>(std::move(modelComponents)); + return std::make_shared>(std::move(modelComponents)); default: STORM_LOG_THROW(false, exceptions::NotImplementedException, "Only DTMC and MDP model types are currently supported."); } } template -storm::Interval AddUncertainty::addUncertainty(ValueType const& vt, double additiveUncertainty, double minimalValue) { +typename AddUncertainty::IntervalType AddUncertainty::addUncertainty(ValueType const& vt, ValueType additiveUncertainty, + ValueType minimalValue) { if (utility::isOne(vt)) { - return storm::Interval(1.0, 1.0); + return IntervalType(storm::utility::one(), storm::utility::one()); } - double center = storm::utility::convertNumber(vt); - STORM_LOG_THROW(center >= minimalValue, storm::exceptions::InvalidArgumentException, "Transition probability is smaller than minimal value"); - double lowerBound = std::max(center - additiveUncertainty, minimalValue); - double upperBound = std::min(center + additiveUncertainty, 1.0 - minimalValue); - STORM_LOG_ASSERT(lowerBound > 0, "Lower bound must be strictly above zero."); - STORM_LOG_ASSERT(upperBound < 1, "Upper bound must be strictly below one."); - return storm::Interval(lowerBound, upperBound); + STORM_LOG_THROW(vt >= minimalValue, storm::exceptions::InvalidArgumentException, "Transition probability is smaller than minimal value"); + ValueType const lowerBound = storm::utility::max(vt - additiveUncertainty, minimalValue); + ValueType const upperBound = storm::utility::min(vt + additiveUncertainty, storm::utility::one() - minimalValue); + STORM_LOG_ASSERT(storm::utility::isPositive(lowerBound), "Lower bound must be strictly above zero."); + STORM_LOG_ASSERT(upperBound < storm::utility::one(), "Upper bound must be strictly below one."); + return IntervalType(lowerBound, upperBound); } template class AddUncertainty; +template class AddUncertainty; } // namespace storm::transformer \ No newline at end of file diff --git a/src/storm/transformer/AddUncertainty.h b/src/storm/transformer/AddUncertainty.h index f31088c1ca..1ff2d35995 100644 --- a/src/storm/transformer/AddUncertainty.h +++ b/src/storm/transformer/AddUncertainty.h @@ -1,7 +1,11 @@ #pragma once +#include + #include "storm/adapters/IntervalForward.h" +#include "storm/adapters/RationalNumberForward.h" #include "storm/models/sparse/Model.h" +#include "storm/utility/constants.h" namespace storm::transformer { @@ -10,16 +14,24 @@ namespace storm::transformer { * We currently support only one type of self-defined uncertainty, although additional types of uncertainty are imaginable. * The transformer does maintain reward models, state labels, state valuations, choice labels and choice origins. * - * @tparam ValueType + * When ValueType is storm::RationalNumber the output model uses storm::RationalInterval (exact arithmetic). + * For all other ValueTypes (e.g. double) the output uses storm::Interval (double-precision). + * + * @tparam ValueType The value type of the input model. */ template class AddUncertainty { public: + using IntervalType = std::conditional_t, storm::RationalInterval, storm::Interval>; + static_assert(std::is_same_v>, "Expected ValueType to match the interval base type."); + AddUncertainty(std::shared_ptr> const& originalModel); - std::shared_ptr> transform(double additiveUncertainty, double minimalValue = 0.0001); + std::shared_ptr> transform(ValueType additiveUncertainty, + ValueType minimalValue = storm::utility::convertNumber(0.0001), + std::optional maxSuccessors = {}); private: - storm::Interval addUncertainty(ValueType const& vt, double additiveUncertainty, double minimalValue); + IntervalType addUncertainty(ValueType const& vt, ValueType additiveUncertainty, ValueType minimalValue); std::shared_ptr> origModel; }; diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index cbc6f8539a..c19983994e 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -225,6 +225,10 @@ template SubsystemBuilderReturnType> const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates = true, SubsystemBuilderOptions options = SubsystemBuilderOptions()); +template SubsystemBuilderReturnType> buildSubsystem( + storm::models::sparse::Model> const& originalModel, + storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates = true, + SubsystemBuilderOptions options = SubsystemBuilderOptions()); template SubsystemBuilderReturnType buildSubsystem(storm::models::sparse::Model const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates = true, @@ -238,6 +242,11 @@ template SubsystemBuilderReturnType buildSubsystem(storm::model storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates = true, SubsystemBuilderOptions options = SubsystemBuilderOptions()); +template SubsystemBuilderReturnType buildSubsystem(storm::models::sparse::Model const& originalModel, + storm::storage::BitVector const& subsystemStates, + storm::storage::BitVector const& subsystemActions, + bool keepUnreachableStates = true, + SubsystemBuilderOptions options = SubsystemBuilderOptions()); } // namespace transformer } // namespace storm diff --git a/src/storm/utility/ConstantsComparator.cpp b/src/storm/utility/ConstantsComparator.cpp index 5513626567..7a80f4b17a 100644 --- a/src/storm/utility/ConstantsComparator.cpp +++ b/src/storm/utility/ConstantsComparator.cpp @@ -65,5 +65,6 @@ template class ConstantsComparator; template class ConstantsComparator; template class ConstantsComparator; +template class ConstantsComparator; } // namespace utility } // namespace storm diff --git a/src/storm/utility/NumberTraits.h b/src/storm/utility/NumberTraits.h index 0ef102199b..23cb9a6036 100644 --- a/src/storm/utility/NumberTraits.h +++ b/src/storm/utility/NumberTraits.h @@ -1,5 +1,6 @@ #pragma once +#include "storm/adapters/IntervalForward.h" #include "storm/adapters/RationalFunctionForward.h" #include "storm/adapters/RationalNumberForward.h" @@ -40,6 +41,18 @@ struct NumberTraits { }; #endif +template<> +struct NumberTraits { + static const bool SupportsExponential = true; + static const bool IsExact = false; +}; + +template<> +struct NumberTraits { + static const bool SupportsExponential = true; + static const bool IsExact = true; +}; + template<> struct NumberTraits { static const bool SupportsExponential = false; diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp index 0e67de3fb8..1a19e27316 100644 --- a/src/storm/utility/builder.cpp +++ b/src/storm/utility/builder.cpp @@ -43,12 +43,18 @@ template std::shared_ptr> buildModelFromCom template std::shared_ptr>> buildModelFromComponents( storm::models::ModelType modelType, storm::storage::sparse::ModelComponents>&& components); +template std::shared_ptr>> +buildModelFromComponents( + storm::models::ModelType modelType, + storm::storage::sparse::ModelComponents>&& components); template std::shared_ptr> buildModelFromComponents( storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); template std::shared_ptr> buildModelFromComponents( storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); template std::shared_ptr> buildModelFromComponents( storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); +template std::shared_ptr> buildModelFromComponents( + storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); } // namespace builder } // namespace utility diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 963d4981d4..aafd3d489f 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -836,6 +836,11 @@ bool isConstant(storm::Interval const& a) { return a.isPointInterval(); } +template<> +bool isConstant(storm::RationalInterval const& a) { + return a.isPointInterval(); +} + template<> bool isInfinity(storm::RationalFunction const& a) { // FIXME: this should be treated more properly. @@ -1036,6 +1041,16 @@ storm::Interval convertNumber(uint64_t const& number) { return storm::Interval(convertNumber(number)); } +template<> +storm::RationalInterval convertNumber(double const& number) { + return storm::RationalInterval(convertNumber(number)); +} + +template<> +storm::RationalInterval convertNumber(uint64_t const& number) { + return storm::RationalInterval(convertNumber(number)); +} + #if defined(STORM_HAVE_GMP) template<> storm::Interval convertNumber(storm::GmpRationalNumber const& n) { @@ -1047,6 +1062,17 @@ storm::GmpRationalNumber convertNumber(storm::Interval const& number) { STORM_LOG_ASSERT(number.isPointInterval(), "Interval must be a point interval to convert"); return convertNumber(number.lower()); } + +template<> +storm::RationalInterval convertNumber(storm::GmpRationalNumber const& n) { + return storm::RationalInterval(convertNumber(n)); +} + +template<> +storm::GmpRationalNumber convertNumber(storm::RationalInterval const& number) { + STORM_LOG_ASSERT(number.isPointInterval(), "Interval must be a point interval to convert"); + return convertNumber(number.lower()); +} #endif #if defined(STORM_HAVE_CLN) @@ -1060,6 +1086,17 @@ storm::ClnRationalNumber convertNumber(storm::Interval const& number) { STORM_LOG_ASSERT(number.isPointInterval(), "Interval must be a point interval to convert"); return convertNumber(number.lower()); } + +template<> +storm::RationalInterval convertNumber(storm::ClnRationalNumber const& n) { + return storm::RationalInterval(convertNumber(n)); +} + +template<> +storm::ClnRationalNumber convertNumber(storm::RationalInterval const& number) { + STORM_LOG_ASSERT(number.isPointInterval(), "Interval must be a point interval to convert"); + return convertNumber(number.lower()); +} #endif template<> @@ -1068,6 +1105,12 @@ double convertNumber(storm::Interval const& number) { return number.lower(); } +template<> +double convertNumber(storm::RationalInterval const& number) { + STORM_LOG_ASSERT(number.isPointInterval(), "Rational interval must be a point interval to convert"); + return convertNumber(number.lower()); +} + template<> storm::Interval abs(storm::Interval const& interval) { return interval.abs(); @@ -1080,6 +1123,18 @@ bool isApproxEqual(storm::Interval const& a, storm::Interval const& b, storm::In isApproxEqual(a.upper(), b.upper(), precision.center(), relative); } +template<> +bool isApproxEqual(storm::RationalInterval const& a, storm::RationalInterval const& b, storm::RationalInterval const& precision, bool relative) { + STORM_LOG_ASSERT(precision.isPointInterval(), "Precision must be a point interval"); + return isApproxEqual(a.lower(), b.lower(), precision.center(), relative) && + isApproxEqual(a.upper(), b.upper(), precision.center(), relative); +} + +template<> +storm::RationalInterval abs(storm::RationalInterval const& interval) { + return interval.abs(); +} + // Explicit instantiations. // double @@ -1250,5 +1305,17 @@ template Interval convertNumber(Interval const&); template std::string to_string(storm::Interval const& value); +// Instantiations for intervals. +template RationalInterval one(); +template RationalInterval zero(); +template bool isOne(RationalInterval const& value); +template bool isZero(RationalInterval const& value); +template bool isInfinity(RationalInterval const& value); +template bool isAlmostZero(RationalInterval const& value); +template bool isNonNegative(RationalInterval const& value); +template bool isPositive(RationalInterval const& value); +template bool isBetween(RationalInterval const&, RationalInterval const&, RationalInterval const& value, bool); + +template std::string to_string(storm::RationalInterval const& value); } // namespace utility } // namespace storm diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index e407834ecf..8964fde8ab 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1962,6 +1962,10 @@ template storm::storage::BitVector performProb0E( template storm::storage::BitVector performProb0E( storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +template storm::storage::BitVector performProb0E( + storm::models::sparse::NondeterministicModel> const& model, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, @@ -1973,6 +1977,10 @@ template storm::storage::BitVector performProb1A( template storm::storage::BitVector performProb1A( storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +template storm::storage::BitVector performProb1A( + storm::models::sparse::NondeterministicModel> const& model, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb1A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, @@ -2264,6 +2272,143 @@ template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates); // End storm::interval +// Instantiations for storm::Rationalinterval + +template storm::storage::BitVector getReachableOneStep(storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::BitVector const& initialStates); + +template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, + storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps, + boost::optional const& choiceFilter); + +template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + +template bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, + boost::optional const& subsystem); + +template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + +template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::BitVector const& initialStates, boost::optional const& subsystem); + +template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + bool useStepBound = false, uint_fast64_t maximalSteps = 0); + +template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + storm::storage::BitVector const& statesWithProbabilityGreater0); + +template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + +template std::pair performProb01( + storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); + +template std::pair performProb01( + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); + +template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + storm::storage::Scheduler& scheduler, + boost::optional const& rowFilter); + +template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::Scheduler& scheduler); + +template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::Scheduler& scheduler); + +template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + storm::storage::Scheduler& scheduler, + boost::optional const& rowFilter = boost::none); + +template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + bool useStepBound = false, uint_fast64_t maximalSteps = 0); + +template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + +template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, + std::vector const& nondeterministicChoiceIndices, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + boost::optional const& choiceConstraint = boost::none); + +template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + +template std::pair performProb01Max( + storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); + +template std::pair performProb01Max( + storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); + +template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, + std::vector const& nondeterministicChoiceIndices, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + bool useStepBound = false, uint_fast64_t maximalSteps = 0, + boost::optional const& choiceConstraint = boost::none); + +template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + +template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, + std::vector const& nondeterministicChoiceIndices, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + +template storm::storage::BitVector performProb1A(storm::storage::SparseMatrix const& transitionMatrix, + std::vector const& nondeterministicChoiceIndices, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + +template std::pair performProb01Min( + storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); + +template std::pair performProb01Min( + storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); + +template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, + std::vector const& player1RowGrouping, + storm::storage::SparseMatrix const& player1BackwardTransitions, + std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair); + +template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, + std::vector const& player1RowGrouping, + storm::storage::SparseMatrix const& player1BackwardTransitions, + std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair, + boost::optional const& player1Candidates); + +template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, + std::vector const& firstStates); +// End storm::Rationalinterval template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, diff --git a/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp index 2cb9f531a3..9c2b0f4f7b 100644 --- a/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp @@ -1,5 +1,6 @@ #include "storm-config.h" #include "storm/adapters/IntervalForward.h" +#include "storm/adapters/RationalNumberForward.h" #include "test/storm_gtest.h" #include "storm-parsers/api/model_descriptions.h" @@ -14,6 +15,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/transformer/AddUncertainty.h" +#include "storm/utility/constants.h" std::unique_ptr getInitialStateFilter( std::shared_ptr> const& model) { @@ -153,6 +155,133 @@ void checkModelForQualitativeResult(std::string const& path, std::string const& } } +std::unique_ptr getInitialStateFilter( + std::shared_ptr> const& model) { + return std::make_unique>(model->getInitialStates()); +} + +storm::RationalNumber getQuantitativeResultAtInitialState(std::shared_ptr> const& model, + std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); +} + +std::unique_ptr getInitialStateFilter( + std::shared_ptr> const& model) { + return std::make_unique>(model->getInitialStates()); +} + +storm::RationalNumber getQuantitativeResultAtInitialState(std::shared_ptr> const& model, + std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); +} + +void expectThrowRational(std::string const& path, std::string const& formulaString, + std::optional uncertaintyResolutionMode = std::nullopt) { + std::shared_ptr> modelPtr = storm::parser::parseDirectEncodingModel(path); + + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); + + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + + std::shared_ptr> dtmc = modelPtr->as>(); + ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType()); + auto task = storm::modelchecker::CheckTask(*formulas[0]); + if (uncertaintyResolutionMode.has_value()) { + task.setUncertaintyResolutionMode(uncertaintyResolutionMode.value()); + } + + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(*dtmc); + STORM_SILENT_EXPECT_THROW(checker.check(env, task), storm::exceptions::BaseException); +} + +void checkExplicitModelForQuantitativeResultRational(std::string const& path, std::string const& formulaString, storm::RationalNumber min, + storm::RationalNumber max) { + std::shared_ptr> modelPtr = storm::parser::parseDirectEncodingModel(path); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + + std::shared_ptr> dtmc = modelPtr->as>(); + ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType()); + auto taskMax = storm::modelchecker::CheckTask(*formulas[0]); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize); + + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(*dtmc); + auto resultMax = checker.check(env, taskMax); + EXPECT_EQ(max, getQuantitativeResultAtInitialState(dtmc, resultMax)); + + auto taskMin = storm::modelchecker::CheckTask(*formulas[1]); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + + auto resultMin = checker.check(env, taskMin); + EXPECT_EQ(min, getQuantitativeResultAtInitialState(dtmc, resultMin)); +} + +void checkPrismModelForQuantitativeResultRational(std::string const& path, std::string const& formulaString, storm::RationalNumber min, + storm::RationalNumber max) { + storm::prism::Program program = storm::api::parseProgram(path); + program = storm::utility::prism::preprocess(program, ""); + + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); + std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); + + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + + std::shared_ptr> dtmc = modelPtr->as>(); + ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType()); + auto taskMax = storm::modelchecker::CheckTask(*formulas[0]); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize); + + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(*dtmc); + auto resultMax = checker.check(env, taskMax); + EXPECT_EQ(max, getQuantitativeResultAtInitialState(dtmc, resultMax)); + + auto taskMin = storm::modelchecker::CheckTask(*formulas[1]); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + + auto resultMin = checker.check(env, taskMin); + EXPECT_EQ(min, getQuantitativeResultAtInitialState(dtmc, resultMin)); +} + +void makeUncertainAndCheckRational(std::string const& path, std::string const& formulaString, storm::RationalNumber amountOfUncertainty) { + storm::prism::Program program = storm::api::parseProgram(path); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = + storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program)); + std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); + auto dtmc = modelPtr->as>(); + + storm::Environment env; + auto taskCertain = storm::modelchecker::CheckTask(*formulas[0]); + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(*dtmc); + auto exresult = checker.check(env, taskCertain); + storm::RationalNumber certainValue = getQuantitativeResultAtInitialState(modelPtr, exresult); + + storm::Environment envIntervals; + envIntervals.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + auto transformer = storm::transformer::AddUncertainty(modelPtr); + auto idtmc = transformer.transform(amountOfUncertainty)->as>(); + auto ichecker = storm::modelchecker::SparseDtmcPrctlModelChecker>(*idtmc); + + auto taskMin = storm::modelchecker::CheckTask(*formulas[0]); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + auto iresultMin = ichecker.check(envIntervals, taskMin); + storm::RationalNumber minValue = getQuantitativeResultAtInitialState(idtmc, iresultMin); + EXPECT_LE(minValue, certainValue); + + auto taskMax = storm::modelchecker::CheckTask(*formulas[0]); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize); + auto iresultMax = ichecker.check(envIntervals, taskMax); + storm::RationalNumber maxValue = getQuantitativeResultAtInitialState(idtmc, iresultMax); + EXPECT_LE(certainValue, maxValue); +} + TEST(RobustDtmcModelCheckerTest, Tiny01ReachMaxMinProbs) { // Maximal Reachability probabilities using explicit format. checkExplicitModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-01.drn", "P=? [ F \"target\"];P=? [ F \"target\"]", 0.3, 0.5); @@ -228,3 +357,83 @@ TEST(RobustDtmcModelCheckerTest, TinyO2Propositional) { checkModelForQualitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-02.drn", "\"target\";!\"target\"", expectedResults); } + +// ---- RationalInterval tests (exact arithmetic) ---- + +TEST(RobustRationalDtmcModelCheckerTest, Tiny01ReachMaxMinProbs) { + checkExplicitModelForQuantitativeResultRational(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-01.drn", "P=? [ F \"target\"];P=? [ F \"target\"]", + storm::RationalNumber("3/10"), storm::RationalNumber("1/2")); +} + +TEST(RobustRationalDtmcModelCheckerTest, Tiny01MaxReachProbNoUncertaintyResolutionMode) { + expectThrowRational(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-01.drn", "P=? [ F \"target\"];", + std::make_optional(storm::UncertaintyResolutionMode::Unset)); +} + +TEST(RobustRationalDtmcModelCheckerTest, Tiny01MaxReachProbNoOptimizationDirectionButRobust) { + expectThrowRational(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-01.drn", "P=? [ F \"target\"];", + std::make_optional(storm::UncertaintyResolutionMode::Robust)); +} + +TEST(RobustRationalDtmcModelCheckerTest, Tiny02GloballyMaxMinProbs) { + expectThrowRational(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-02.drn", "P=? [ G \"target\"];P=? [ G \"target\"]"); +} + +TEST(RobustRationalDtmcModelCheckerTest, DieIntervalsMaxMin) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + checkPrismModelForQuantitativeResultRational(STORM_TEST_RESOURCES_DIR "/idtmc/die-intervals.pm", "P=? [ F \"one\"];P=? [ F \"one\"]", + storm::RationalNumber("4483008223/94143178827"), storm::RationalNumber("35864065784/94143178827")); +} + +TEST(RobustRationalDtmcModelCheckerTest, BrpIntervalsMaxMin) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + checkPrismModelForQuantitativeResultRational( + STORM_TEST_RESOURCES_DIR "/idtmc/brp-32-2-intervals.pm", "P=? [ F \"error\" ];P=? [ F \"error\" ]", + // The number is to large to be represented as a literal, so we construct it from strings. + storm::RationalNumber("10238464074071514998168131748974289312176706851339248682605279417683104172439385084862067764341447739354976890683145110072150529" + "29484271217452553595194641992099205093706027267658909966207049695357884534755950707204946503657943965652247014748702342577938440" + "579441829932769922685028147340905022682454110960938051" + "/" + "40000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + "00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + "000000000000000000000000000000000000000000000000000000000000000"), + storm::RationalNumber("73421101667166357614487085157865792442422423664718103404519649530149236548299533815461648662459394997073289369183682645650367121" + "4626220291672876565353557862092334897" + "/" + "86736173798840354720596224069595336914062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + "0000000000000000000000000000000000000000")); +} + +TEST(RobustRationalDtmcModelCheckerTest, DieIntervalsMaxMinRewards) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + checkPrismModelForQuantitativeResultRational(STORM_TEST_RESOURCES_DIR "/idtmc/die-intervals.pm", "R=? [ F \"done\"];R=? [ F \"done\"]", + storm::RationalNumber("15544649/4782969"), storm::RationalNumber("76715008330675523/16677181699666569")); +} + +TEST(RobustRationalDtmcModelCheckerTest, Tiny03MaxMinRewards) { + checkExplicitModelForQuantitativeResultRational(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-03.drn", "R=? [ F \"target\"];R=? [ F \"target\"]", + storm::RationalNumber("13/2"), storm::RationalNumber("17/2")); +} + +TEST(RobustRationalDtmcModelCheckerTest, Tiny03RewardsNoUncertaintyResolutionMode) { + expectThrowRational(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-03.drn", "R=? [ F \"target\"]", storm::UncertaintyResolutionMode::Unset); +} + +TEST(RobustRationalDtmcModelCheckerTest, Tiny04MaxMinRewards) { + checkExplicitModelForQuantitativeResultRational(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-04.drn", "R=? [ F \"target\"];R=? [ F \"target\"]", + storm::utility::infinity(), storm::utility::infinity()); +} + +TEST(RobustRationalDtmcModelCheckerTest, AddUncertaintyBrpMax) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + makeUncertainAndCheckRational(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm", "P=? [ F \"target\"]", storm::RationalNumber("1/10")); + makeUncertainAndCheckRational(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm", "P=? [ F \"target\"]", storm::RationalNumber("1/20")); +} diff --git a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp index d49c63f129..8756b7f1d2 100644 --- a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp @@ -1,4 +1,6 @@ #include "storm-config.h" +#include "storm/adapters/RationalNumberForward.h" +#include "storm/exceptions/NotImplementedException.h" #include "test/storm_gtest.h" #include "storm-parsers/api/model_descriptions.h" @@ -25,6 +27,23 @@ std::unique_ptr getInitialStateFilt return std::make_unique>(model->getInitialStates()); } +std::unique_ptr getInitialStateFilter( + std::shared_ptr> const& model) { + return std::make_unique>(model->getInitialStates()); +} + +storm::RationalNumber getQuantitativeResultAtInitialState(std::shared_ptr> const& model, + std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); +} + +std::unique_ptr getInitialStateFilter( + std::shared_ptr> const& model) { + return std::make_unique>(model->getInitialStates()); +} + double getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { auto filter = getInitialStateFilter(model); @@ -39,6 +58,13 @@ double getQuantitativeResultAtInitialState(std::shared_ptrasQuantitativeCheckResult().getMin(); } +storm::RationalNumber getQuantitativeResultAtInitialState(std::shared_ptr> const& model, + std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); +} + void expectThrow(std::string const& path, std::string const& formulaString) { std::shared_ptr> modelPtr = storm::parser::parseDirectEncodingModel(path); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); @@ -51,7 +77,7 @@ void expectThrow(std::string const& path, std::string const& formulaString) { auto task = storm::modelchecker::CheckTask(*formulas[0]); auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); - STORM_SILENT_EXPECT_THROW(checker.check(env, task), storm::exceptions::InvalidArgumentException); + STORM_SILENT_EXPECT_THROW(checker.check(env, task), storm::exceptions::NotImplementedException); } void checkModel(std::string const& path, std::string const& formulaString, double maxmin, double maxmax, double minmax, double minmin, bool produceScheduler) { @@ -124,6 +150,38 @@ void checkPrismModelForQuantitativeResult(std::string const& path, std::string c EXPECT_NEAR(maxmax, getQuantitativeResultAtInitialState(mdp, resultMaxMax), 0.0001); } +void checkModelRational(std::string const& path, std::string const& formulaString, storm::RationalNumber maxmin, storm::RationalNumber maxmax, + storm::RationalNumber minmax, storm::RationalNumber minmin, bool produceScheduler) { + std::shared_ptr> modelPtr = storm::parser::parseDirectEncodingModel(path); + + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + + std::shared_ptr> mdp = modelPtr->as>(); + ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType()); + auto taskMax = storm::modelchecker::CheckTask(*formulas[0]); + taskMax.setProduceSchedulers(produceScheduler); + + auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust); + auto resultMax = checker.check(env, taskMax); + EXPECT_EQ(maxmin, getQuantitativeResultAtInitialState(mdp, resultMax)); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative); + auto resultMaxNonRobust = checker.check(env, taskMax); + EXPECT_EQ(maxmax, getQuantitativeResultAtInitialState(mdp, resultMaxNonRobust)); + + auto taskMin = storm::modelchecker::CheckTask(*formulas[1]); + taskMin.setProduceSchedulers(produceScheduler); + + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust); + auto resultMin = checker.check(env, taskMin); + EXPECT_EQ(minmax, getQuantitativeResultAtInitialState(mdp, resultMin)); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative); + auto resultMinNonRobust = checker.check(env, taskMin); + EXPECT_EQ(minmin, getQuantitativeResultAtInitialState(mdp, resultMinNonRobust)); +} + TEST(RobustMdpModelCheckerTest, RobotMinMaxTest) { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; @@ -168,16 +226,54 @@ void makeUncertainAndCheck(std::string const& path, std::string const& formulaSt EXPECT_LE(certainValue, maxValue); } +void makeUncertainAndCheckRational(std::string const& path, std::string const& formulaString, storm::RationalNumber amountOfUncertainty) { + storm::prism::Program program = storm::api::parseProgram(path); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = + storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program)); + std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); + auto mdp = modelPtr->as>(); + + ASSERT_TRUE(formulas[0]->isProbabilityOperatorFormula()); + ASSERT_TRUE(formulas[0]->asProbabilityOperatorFormula().getOptimalityType() == storm::solver::OptimizationDirection::Maximize); + + storm::Environment env; + auto taskCertain = storm::modelchecker::CheckTask(*formulas[0]); + auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); + auto exresult = checker.check(env, taskCertain); + storm::RationalNumber certainValue = getQuantitativeResultAtInitialState(modelPtr, exresult); + + storm::Environment envIntervals; + envIntervals.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + auto transformer = storm::transformer::AddUncertainty(modelPtr); + auto imdp = transformer.transform(amountOfUncertainty)->as>(); + auto ichecker = storm::modelchecker::SparseMdpPrctlModelChecker>(*imdp); + + auto taskMin = storm::modelchecker::CheckTask(*formulas[0]); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + auto iresultMin = ichecker.check(envIntervals, taskMin); + storm::RationalNumber minValue = getQuantitativeResultAtInitialState(imdp, iresultMin); + EXPECT_LE(minValue, certainValue); + + auto taskMax = storm::modelchecker::CheckTask(*formulas[0]); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize); + auto iresultMax = ichecker.check(envIntervals, taskMax); + storm::RationalNumber maxValue = getQuantitativeResultAtInitialState(imdp, iresultMax); + EXPECT_LE(certainValue, maxValue); +} + +// TODO: Add next properties + TEST(RobustMDPModelCheckingTest, Tiny01maxmin) { checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-01.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", 0.4, 0.5, 0.5, 0.4, false); } TEST(RobustMDPModelCheckingTest, Tiny03maxmin) { - checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", 0.4, 0.5, 0.5, 0.4, true); + checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", 0.4, 0.6, 0.5, 0.3, true); } TEST(RobustMDPModelCheckingTest, BoundedTiny03maxmin) { - expectThrow(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F<=3 \"target\"]"); + checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F<=3 \"target\"];Pmin=? [ F<=3 \"target\"]", 0.4, 0.6, 0.5, 0.3, true); } TEST(RobustMDPModelCheckingTest, Tiny04maxmin) { @@ -192,6 +288,34 @@ TEST(RobustMDPModelCheckingTest, Tiny04maxmin_rewards) { expectThrow(STORM_TEST_RESOURCES_DIR "/imdp/tiny-04.drn", "Rmin=? [ F \"target\"]"); } +// ---- RationalInterval tests (exact arithmetic) ---- + +TEST(RobustRationalMDPModelCheckingTest, Tiny01maxmin) { + checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-01.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber("2/5"), + storm::RationalNumber("1/2"), storm::RationalNumber("1/2"), storm::RationalNumber("2/5"), false); +} + +TEST(RobustRationalMDPModelCheckingTest, Tiny03maxmin) { + checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber("2/5"), + storm::RationalNumber("3/5"), storm::RationalNumber("1/2"), storm::RationalNumber("3/10"), true); +} + +TEST(RobustRationalMDPModelCheckingTest, BoundedTiny03maxmin) { + checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F<=3 \"target\"];Pmin=? [ F<=3 \"target\"]", storm::RationalNumber("2/5"), + storm::RationalNumber("3/5"), storm::RationalNumber("1/2"), storm::RationalNumber("3/10"), true); +} + +TEST(RobustRationalMDPModelCheckingTest, Tiny04maxmin) { + // Fill in exact rational values once test output is known. + checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-04.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber(1), + storm::RationalNumber(1), storm::RationalNumber("42857140807299/100000000000000"), storm::RationalNumber("21/50"), false); +} + +TEST(RobustRationalMDPModelCheckingTest, Tiny05maxmin) { + checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-05.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber("3/10"), + storm::RationalNumber("2/5"), storm::RationalNumber("2/5"), storm::RationalNumber("3/10"), false); +} + TEST(RobustMDPModelCheckingTest, AddUncertaintyCoin22max) { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; @@ -199,3 +323,11 @@ TEST(RobustMDPModelCheckingTest, AddUncertaintyCoin22max) { makeUncertainAndCheck(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", 0.1); makeUncertainAndCheck(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", 0.2); } + +TEST(RobustRationalMDPModelCheckingTest, AddUncertaintyCoin22max) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + makeUncertainAndCheckRational(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", storm::RationalNumber("1/10")); + makeUncertainAndCheckRational(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", storm::RationalNumber("1/5")); +} diff --git a/src/test/storm/solver/MultiplierTest.cpp b/src/test/storm/solver/MultiplierTest.cpp index 693ad44f05..1933065ce5 100644 --- a/src/test/storm/solver/MultiplierTest.cpp +++ b/src/test/storm/solver/MultiplierTest.cpp @@ -123,4 +123,6 @@ TYPED_TEST(MultiplierTest, repeatedMultiplyAndReduceTest) { EXPECT_NEAR(x[0], this->parseNumber("0.923808265834023387639"), this->precision()); } +// TODO: Write test using the uncertainty resolution mode when more modes than 'Unset' are supported by the native multiplier. + } // namespace \ No newline at end of file diff --git a/src/test/storm/transformer/AddUncertaintyTest.cpp b/src/test/storm/transformer/AddUncertaintyTest.cpp index 1911aba39d..d35b4d38ee 100644 --- a/src/test/storm/transformer/AddUncertaintyTest.cpp +++ b/src/test/storm/transformer/AddUncertaintyTest.cpp @@ -3,6 +3,7 @@ #include "storm-parsers/api/storm-parsers.h" #include "storm-parsers/parser/PrismParser.h" +#include "storm/adapters/RationalNumberForward.h" #include "storm/api/storm.h" #include "storm/transformer/AddUncertainty.h" @@ -37,3 +38,35 @@ TEST(AddUncertaintyTransformerTest, Coin22Test) { EXPECT_EQ(uncertainModel->getNumberOfTransitions(), model->getNumberOfTransitions()); EXPECT_TRUE(uncertainModel->hasUncertainty()); } + +TEST(AddUncertaintyTransformerTest, BrpTestRational) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); + std::string formulasString = "P=? [ F \"target\"]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); + auto model = storm::api::buildSparseModel(program, formulas); + + auto transformer = storm::transformer::AddUncertainty(model); + auto uncertainModel = transformer.transform(storm::RationalNumber("1/100")); + EXPECT_EQ(uncertainModel->getNumberOfStates(), model->getNumberOfStates()); + EXPECT_EQ(uncertainModel->getNumberOfTransitions(), model->getNumberOfTransitions()); + EXPECT_TRUE(uncertainModel->hasUncertainty()); +} + +TEST(AddUncertaintyTransformerTest, Coin22TestRational) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); + std::string formulasString = "Pmax=? [ F \"all_coins_equal_1\"]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); + auto model = storm::api::buildSparseModel(program, formulas); + + auto transformer = storm::transformer::AddUncertainty(model); + auto uncertainModel = transformer.transform(storm::RationalNumber("1/100")); + EXPECT_EQ(uncertainModel->getNumberOfStates(), model->getNumberOfStates()); + EXPECT_EQ(uncertainModel->getNumberOfTransitions(), model->getNumberOfTransitions()); + EXPECT_TRUE(uncertainModel->hasUncertainty()); +}