diff --git a/resources/examples/testfiles/idtmc/brp-32-2-intervals.pm b/resources/examples/testfiles/idtmc/brp-32-2-intervals.pm new file mode 100644 index 0000000000..7e79374252 --- /dev/null +++ b/resources/examples/testfiles/idtmc/brp-32-2-intervals.pm @@ -0,0 +1,145 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 +// DTMC with interval probabilities for channels (Storm IMDP/IDTMC extension) + +dtmc + +// number of chunks +const int N = 32; +// maximum number of retransmissions +const int MAX = 2; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=true); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=true); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +module checker // prevents more than one frame being set + + T : bool; + + [NewFile] (T=false) -> (T'=true); + +endmodule + +// ------------------------------------------------------------------ +// Channels with interval probabilities (IMDP-style ranges) +// These match the spirit of the DRN ranges like [0.98,1] and [0.0001,0.02] +// ------------------------------------------------------------------ + +module channelK + + k : [0..2]; + + // idle -- message transfer may succeed or be lost + // (success prob in [0.98, 1], loss prob in [0.0001, 0.02]) + [aF] (k=0) -> [0.98, 1] : (k'=1) + [0.0001, 0.02] : (k'=2); + + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle -- ack transfer may succeed or be lost + // (success prob in [0.99, 1], loss prob in [0.0001, 0.01]) + [aA] (l=0) -> [0.99, 1] : (l'=1) + [0.0001, 0.01] : (l'=2); + + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + +rewards + [aF] i=1 : 1; +endrewards + +label "error" = s=5; diff --git a/resources/examples/testfiles/idtmc/die-intervals.pm b/resources/examples/testfiles/idtmc/die-intervals.pm new file mode 100644 index 0000000000..a1a6ffe809 --- /dev/null +++ b/resources/examples/testfiles/idtmc/die-intervals.pm @@ -0,0 +1,29 @@ +// Knuth's model of a fair die using unfair coins, where the bias is controlled by nature. +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> [1/3, 2/3] : (s'=1) + [1/3, 2/3] : (s'=2); + [] s=1 -> [1/3, 2/3] : (s'=3) + [1/3, 2/3] : (s'=4); + [] s=2 -> [1/3, 2/3] : (s'=5) + [1/3, 2/3] : (s'=6); + [] s=3 -> [1/3, 2/3] : (s'=1) + [1/3, 2/3] : (s'=7) & (d'=1); + [] s=4 -> [1/3, 2/3] : (s'=7) & (d'=2) + [1/3, 2/3] : (s'=7) & (d'=3); + [] s=5 -> [1/3, 2/3] : (s'=7) & (d'=4) + [1/3, 2/3] : (s'=7) & (d'=5); + [] s=6 -> [1/3, 2/3] : (s'=2) + [1/3, 2/3] : (s'=7) & (d'=6); + [] s=7 -> 1: (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards + +label "one" = s=7&d=1; +label "two" = s=7&d=2; +label "three" = s=7&d=3; +label "done" = s=7; diff --git a/resources/examples/testfiles/idtmc/tiny-01.drn b/resources/examples/testfiles/idtmc/tiny-01.drn new file mode 100644 index 0000000000..9fbc94c2d9 --- /dev/null +++ b/resources/examples/testfiles/idtmc/tiny-01.drn @@ -0,0 +1,20 @@ +@type: DTMC +@parameters + +@reward_models + +@nr_states +3 +@nr_choices +3 +@model +state 0 init + action 0 + 1 : [0.3, 0.5] + 2 : [0.5, 0.7] +state 1 target + action 0 + 1 : [1, 1] +state 2 + action 0 + 2 : [1, 1] \ No newline at end of file diff --git a/resources/examples/testfiles/idtmc/tiny-02.drn b/resources/examples/testfiles/idtmc/tiny-02.drn new file mode 100644 index 0000000000..d93e556887 --- /dev/null +++ b/resources/examples/testfiles/idtmc/tiny-02.drn @@ -0,0 +1,20 @@ +@type: DTMC +@parameters + +@reward_models + +@nr_states +3 +@nr_choices +3 +@model +state 0 init target + action 0 + 1 : [0.3, 0.5] + 2 : [0.5, 0.7] +state 1 + action 0 + 1 : [1, 1] +state 2 target + action 0 + 2 : [1, 1] \ No newline at end of file diff --git a/resources/examples/testfiles/idtmc/tiny-03.drn b/resources/examples/testfiles/idtmc/tiny-03.drn new file mode 100644 index 0000000000..ee4aa53f13 --- /dev/null +++ b/resources/examples/testfiles/idtmc/tiny-03.drn @@ -0,0 +1,23 @@ +@type: DTMC +@parameters + +@reward_models +cost +@nr_states +4 +@nr_choices +4 +@model +state 0 init [0] + action 0 + 1 : [0.3, 0.7] + 2 : [0.3, 0.7] +state 1 [5] + action 0 + 3 : [1, 1] +state 2 [10] + action 0 + 3 : [1, 1] +state 3 target [0] + action 0 + 3 : [1, 1] \ No newline at end of file diff --git a/resources/examples/testfiles/idtmc/tiny-04.drn b/resources/examples/testfiles/idtmc/tiny-04.drn new file mode 100644 index 0000000000..58b8308b0a --- /dev/null +++ b/resources/examples/testfiles/idtmc/tiny-04.drn @@ -0,0 +1,26 @@ +@type: DTMC +@parameters + +@reward_models +cost +@nr_states +5 +@nr_choices +5 +@model +state 0 init [0] + action 0 + 1 : [0.3, 0.7] + 2 : [0.3, 0.7] +state 1 [5] + action 0 + 3 : [1, 1] +state 2 [10] + action 0 + 4 : [1, 1] +state 3 target [0] + action 0 + 3 : [1, 1] +state 4 [1] + action 0 + 4 : [1, 1] \ No newline at end of file diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 06d41ac28d..b78f201df3 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -1295,8 +1295,18 @@ void verifyModel(std::shared_ptr> const& auto const& ioSettings = storm::settings::getModule(); auto verificationCallback = [&sparseModel, &ioSettings, &mpi](std::shared_ptr const& formula, std::shared_ptr const& states) { + auto createTask = [&ioSettings](auto const& f, bool onlyInitialStates) { + (void)ioSettings; // suppress unused lambda capture warning. [[maybe_unused]] doesn't work for lambda captures. + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(ioSettings.isUncertaintyResolutionModeSet(), storm::exceptions::InvalidSettingsException, + "Uncertainty resolution mode required for uncertain (interval) models."); + return storm::api::createTask(f, storm::solver::convert(ioSettings.getUncertaintyResolutionMode()), onlyInitialStates); + } else { + return storm::api::createTask(f, onlyInitialStates); + } + }; bool filterForInitialStates = states->isInitialFormula(); - auto task = storm::api::createTask(formula, filterForInitialStates); + auto task = createTask(formula, states->isInitialFormula()); if (ioSettings.isExportSchedulerSet()) { task.setProduceSchedulers(true); } @@ -1306,7 +1316,7 @@ void verifyModel(std::shared_ptr> const& if (filterForInitialStates) { filter = std::make_unique(sparseModel->getInitialStates()); } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true' - filter = storm::api::verifyWithSparseEngine(mpi.env, sparseModel, storm::api::createTask(states, false)); + filter = storm::api::verifyWithSparseEngine(mpi.env, sparseModel, createTask(states, false)); } if (result && filter) { result->filter(filter->asQualitativeCheckResult()); @@ -1337,12 +1347,9 @@ void verifyModel(std::shared_ptr> const& "--buildchoicelab or --buildchoiceorig."); } if (result->isExplicitQuantitativeCheckResult()) { - if constexpr (storm::IsIntervalType) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export for interval models is not supported."); - } else { - storm::api::exportScheduler(sparseModel, result->template asExplicitQuantitativeCheckResult().getScheduler(), - schedulerExportPath.string()); - } + storm::api::exportScheduler(sparseModel, + result->template asExplicitQuantitativeCheckResult>().getScheduler(), + schedulerExportPath.string()); } else if (result->isExplicitParetoCurveCheckResult()) { if constexpr (std::is_same_v || storm::IsIntervalType) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export for models of this value type is not supported."); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 122920d304..9d4b9f4e82 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -26,6 +26,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/models/sparse/Dtmc.h" #include "storm/solver/OptimizationDirection.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/solver/multiplier/Multiplier.h" #include "storm/storage/BitVector.h" #include "storm/utility/constants.h" @@ -437,7 +438,7 @@ std::vector SparseDtmcParameterLiftingModelCheckersetHasUniqueSolution(); solver->setHasNoEndComponents(); // Uncertainty is not robust (=adversarial) - solver->setUncertaintyIsRobust(false); + solver->setUncertaintyResolutionMode(UncertaintyResolutionMode::Cooperative); if (lowerResultBound) solver->setLowerBound(lowerResultBound.value()); if (upperResultBound) { diff --git a/src/storm/api/export.h b/src/storm/api/export.h index c24ea4ce33..9e5feaae88 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -62,8 +62,8 @@ void exportSymbolicModelAsDot(std::shared_ptrwriteDotToFile(filename); } -template -void exportScheduler(std::shared_ptr> const& model, storm::storage::Scheduler const& scheduler, +template +void exportScheduler(std::shared_ptr> const& model, storm::storage::Scheduler const& scheduler, std::string const& filename) { std::ofstream stream; storm::io::openFile(filename, stream); diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index ee166a638f..a5b31933db 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -30,6 +30,7 @@ #include "storm/settings/modules/AbstractionSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/IOSettings.h" #include "storm/storage/SymbolicModelDescription.h" @@ -41,11 +42,22 @@ namespace storm { namespace api { template + requires(!storm::IsIntervalType) storm::modelchecker::CheckTask createTask(std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); } +template + requires(storm::IsIntervalType) +storm::modelchecker::CheckTask createTask(std::shared_ptr const& formula, + storm::UncertaintyResolutionMode uncertaintyResolution, + bool onlyInitialStatesRelevant = false) { + storm::modelchecker::CheckTask checkTask(*formula, onlyInitialStatesRelevant); + checkTask.setUncertaintyResolutionMode(uncertaintyResolution); + return checkTask; +} + // // Verifying with Exploration engine // @@ -93,24 +105,27 @@ template std::unique_ptr verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { - if constexpr (storm::IsIntervalType) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify interval DTMCs."); + std::unique_ptr result; + if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && + storm::settings::getModule().isUseDedicatedModelCheckerSet()) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "We do not yet support using the elimination checker with intervals models."); + } + auto newTask = task.template convertValueType< + typename storm::modelchecker::SparseDtmcEliminationModelChecker>::SolutionType>(); + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(newTask)) { + result = modelchecker.check(env, newTask); + } } else { - std::unique_ptr result; - if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && - storm::settings::getModule().isUseDedicatedModelCheckerSet()) { - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(env, task); - } - } else { - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(env, task); - } + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + auto newTask = + task.template convertValueType>::SolutionType>(); + if (modelchecker.canHandle(newTask)) { + result = modelchecker.check(env, newTask); } - return result; } + return result; } template diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index fae679a6d4..04cc3cce72 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -489,6 +489,7 @@ template class AbstractModelChecker>; template class AbstractModelChecker>; +template class AbstractModelChecker>; // DD template class AbstractModelChecker>; diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 93c9ccfadc..16cd6ca63a 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -7,10 +7,11 @@ #include "storm/logic/Formulas.h" #include "storm/utility/constants.h" +#include "storm/adapters/IntervalForward.h" #include "storm/logic/ComparisonType.h" #include "storm/logic/PlayerCoalition.h" #include "storm/modelchecker/hints/ModelCheckerHint.h" -#include "storm/solver/OptimizationDirection.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/exceptions/InvalidOperationException.h" @@ -35,11 +36,12 @@ class CheckTask { /*! * Creates a task object with the default options for the given formula. */ - CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula), hint(new ModelCheckerHint()) { + CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false, UncertaintyResolutionMode = UncertaintyResolutionMode::Unset) + : formula(formula), hint(new ModelCheckerHint()) { this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; this->produceSchedulers = false; this->qualitative = false; - this->robustUncertainty = true; + this->uncertaintyResolutionMode = UncertaintyResolutionMode::Unset; updateOperatorInformation(); } @@ -52,7 +54,7 @@ class CheckTask { CheckTask substituteFormula(NewFormulaType const& newFormula) const { CheckTask result(newFormula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint, - this->robustUncertainty); + this->uncertaintyResolutionMode); result.updateOperatorInformation(); return result; } @@ -131,7 +133,7 @@ class CheckTask { CheckTask convertValueType() const { return CheckTask(this->formula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint, - this->robustUncertainty); + this->uncertaintyResolutionMode); } /*! @@ -299,18 +301,31 @@ class CheckTask { } /*! - * Conversion operator that strips the type of the formula. + * Retrieves the mode which decides how the uncertainty will be resolved. */ - operator CheckTask() const { - return this->template substituteFormula(this->getFormula()); + UncertaintyResolutionMode getUncertaintyResolutionMode() const { + return uncertaintyResolutionMode; + } + + /*! + * Sets the mode which decides how the uncertainty will be resolved. + */ + void setUncertaintyResolutionMode(UncertaintyResolutionMode uncertaintyResolutionMode) { + this->uncertaintyResolutionMode = uncertaintyResolutionMode; } - bool getRobustUncertainty() const { - return robustUncertainty; + /*! + * Returns whether the mode, which decides how the uncertainty will be resolved, is set. + */ + bool isUncertaintyResolutionModeSet() const { + return isSet(this->uncertaintyResolutionMode); } - void setRobustUncertainty(bool robust = true) { - robustUncertainty = robust; + /*! + * Conversion operator that strips the type of the formula. + */ + operator CheckTask() const { + return this->template substituteFormula(this->getFormula()); } private: @@ -332,7 +347,7 @@ class CheckTask { CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional playerCoalition, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr const& hint, - bool robust) + UncertaintyResolutionMode uncertaintyResolutionMode) : formula(formula), optimizationDirection(optimizationDirection), playerCoalition(playerCoalition), @@ -342,7 +357,7 @@ class CheckTask { qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint), - robustUncertainty(robust) { + uncertaintyResolutionMode(uncertaintyResolutionMode) { // Intentionally left empty. } @@ -374,8 +389,8 @@ class CheckTask { // A hint that might contain information that speeds up the modelchecking process (if supported by the model checker) std::shared_ptr hint; - /// Whether uncertainty should be resolved robust (standard) or angelically. - bool robustUncertainty; + // Whether uncertainty should be resolved be minimizing, maximizing, acting robust or cooperative. + UncertaintyResolutionMode uncertaintyResolutionMode; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/helper/DiscountingHelper.cpp b/src/storm/modelchecker/helper/DiscountingHelper.cpp index 7cbd1e7d37..3b1e437bf4 100644 --- a/src/storm/modelchecker/helper/DiscountingHelper.cpp +++ b/src/storm/modelchecker/helper/DiscountingHelper.cpp @@ -63,7 +63,7 @@ bool DiscountingHelper::solveWithDiscountedValueI // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir.value(), true); + this->extractScheduler(x, b, dir.value(), UncertaintyResolutionMode::Robust); } return status == solver::SolverStatus::Converged || status == solver::SolverStatus::TerminatedEarly; } @@ -87,15 +87,17 @@ bool DiscountingHelper::hasScheduler() const { template<> void DiscountingHelper::extractScheduler(std::vector& x, std::vector const& b, OptimizationDirection const& dir, - bool robust) const {} + UncertaintyResolutionMode uncertaintyResolutionMode) const {} template<> void DiscountingHelper::extractScheduler(std::vector& x, std::vector const& b, - OptimizationDirection const& dir, bool robust) const {} + OptimizationDirection const& dir, + UncertaintyResolutionMode uncertaintyResolutionMode) const {} template void DiscountingHelper::extractScheduler(std::vector& x, std::vector const& b, - OptimizationDirection const& dir, bool robust) const { + OptimizationDirection const& dir, + UncertaintyResolutionMode uncertaintyResolutionMode) const { // Make sure that storage for scheduler choices is available if (!this->schedulerChoices) { this->schedulerChoices = std::vector(x.size(), 0); @@ -108,7 +110,7 @@ void DiscountingHelper::extractScheduler(std::vec setUpViOperator(); } storm::solver::helper::SchedulerTrackingHelper schedHelper(viOperator); - schedHelper.computeScheduler(x, b, dir, *this->schedulerChoices, robust, nullptr); + schedHelper.computeScheduler(x, b, dir, *this->schedulerChoices, uncertaintyResolutionMode, nullptr); } template diff --git a/src/storm/modelchecker/helper/DiscountingHelper.h b/src/storm/modelchecker/helper/DiscountingHelper.h index c02352a19c..1a1e75c121 100644 --- a/src/storm/modelchecker/helper/DiscountingHelper.h +++ b/src/storm/modelchecker/helper/DiscountingHelper.h @@ -37,7 +37,8 @@ class DiscountingHelper : public SingleValueModelCheckerHelper& x, std::vector const& b, OptimizationDirection const& dir, bool robust) const; + void extractScheduler(std::vector& x, std::vector const& b, OptimizationDirection const& dir, + UncertaintyResolutionMode uncertaintyResolutionMode) const; mutable std::shared_ptr> viOperator; mutable std::unique_ptr> auxiliaryRowGroupVector; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 0da5f8dfbe..7ee772bf0c 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -32,38 +32,48 @@ SparseDtmcPrctlModelChecker::SparseDtmcPrctlModelChecker(Sp } template -bool SparseDtmcPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, +bool SparseDtmcPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctlstar() - .setLongRunAverageRewardFormulasAllowed(true) - .setLongRunAverageProbabilitiesAllowed(true) - .setConditionalProbabilityFormulasAllowed(true) - .setConditionalRewardFormulasAllowed(true) - .setTotalRewardFormulasAllowed(true) - .setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true) - .setRewardBoundedUntilFormulasAllowed(true) - .setRewardBoundedCumulativeRewardFormulasAllowed(true) - .setMultiDimensionalBoundedUntilFormulasAllowed(true) - .setMultiDimensionalCumulativeRewardFormulasAllowed(true) - .setTimeOperatorsAllowed(true) - .setReachbilityTimeFormulasAllowed(true) - .setRewardAccumulationAllowed(true) - .setHOAPathFormulasAllowed(true) - .setDiscountedTotalRewardFormulasAllowed(true) - .setDiscountedCumulativeRewardFormulasAllowed(true))) { - return true; - } else if (checkTask.isOnlyInitialStatesRelevantSet() && formula.isInFragment(storm::logic::quantiles())) { - if (requiresSingleInitialState) { - *requiresSingleInitialState = true; + if constexpr (storm::IsIntervalType) { + if (formula.isInFragment(storm::logic::propositional())) { + return true; + } + if (formula.isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setRewardOperatorsAllowed(true))) { + return true; + } + } else { + if (formula.isInFragment(storm::logic::prctlstar() + .setLongRunAverageRewardFormulasAllowed(true) + .setLongRunAverageProbabilitiesAllowed(true) + .setConditionalProbabilityFormulasAllowed(true) + .setConditionalRewardFormulasAllowed(true) + .setTotalRewardFormulasAllowed(true) + .setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true) + .setRewardBoundedUntilFormulasAllowed(true) + .setRewardBoundedCumulativeRewardFormulasAllowed(true) + .setMultiDimensionalBoundedUntilFormulasAllowed(true) + .setMultiDimensionalCumulativeRewardFormulasAllowed(true) + .setTimeOperatorsAllowed(true) + .setReachbilityTimeFormulasAllowed(true) + .setRewardAccumulationAllowed(true) + .setHOAPathFormulasAllowed(true) + .setDiscountedTotalRewardFormulasAllowed(true) + .setDiscountedCumulativeRewardFormulasAllowed(true))) { + return true; + } else if (checkTask.isOnlyInitialStatesRelevantSet() && formula.isInFragment(storm::logic::quantiles())) { + if (requiresSingleInitialState) { + *requiresSingleInitialState = true; + } + return true; } - return true; } + return false; } template -bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { +bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { bool requiresSingleInitialState = false; if (canHandleStatic(checkTask, &requiresSingleInitialState)) { return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1; @@ -74,130 +84,172 @@ bool SparseDtmcPrctlModelChecker::canHandle(CheckTask std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities( - Environment const& env, CheckTask const& checkTask) { - storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) { - 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::logic::OperatorInformation opInfo; - if (checkTask.isBoundSet()) { - opInfo.bound = checkTask.getBound(); - } - auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), opInfo); - auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented bounded until with intervals"); } 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 step bound."); - std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); - std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - storm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper 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()); - std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - return result; + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) { + 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::logic::OperatorInformation opInfo; + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), opInfo); + auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues( + env, this->getModel(), formula); + 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 step bound."); + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + storm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper 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()); + std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + return result; + } } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities( - Environment const& env, CheckTask const& checkTask) { - storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeNextProbabilities( - env, this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented next probabilities with intervals"); + } else { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeNextProbabilities( + env, this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + if (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 && + checkTask.getUncertaintyResolutionMode() != UncertaintyResolutionMode::Cooperative, + storm::exceptions::InvalidSettingsException, + "Uncertainty resolution modes robust or cooperative not allowed if optimization direction is not stated explicitly."); + STORM_LOG_THROW(this->getModel().getTransitionMatrix().hasOnlyPositiveEntries(), storm::exceptions::InvalidSettingsException, + "Computing until probabilities on uncertain model requires graph-preservation."); + } std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), - checkTask.getHint()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), + checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities( - Environment const& env, CheckTask const& checkTask) { - storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented globally probabilities with intervals"); + } else { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeHOAPathProbabilities( - Environment const& env, CheckTask const& checkTask) { - storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); + Environment const& env, CheckTask const& checkTask) { + 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(); - storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - }; - auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); - std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); + auto formulaChecker = [&](storm::logic::Formula const& formula) { + return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + }; + auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); + std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeLTLProbabilities( - Environment const& env, CheckTask const& checkTask) { - storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented LTL with interval models"); + } else { + storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); - storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - }; - std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); + auto formulaChecker = [&](storm::logic::Formula const& formula) { + return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + }; + std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { - 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_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException, - "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given."); - storm::logic::OperatorInformation opInfo; - if (checkTask.isBoundSet()) { - opInfo.bound = checkTask.getBound(); - } - auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo); - auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented cumulative rewards with intervals"); } 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); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), - rewardPathFormula.getNonStrictBound()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { + 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_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException, + "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given."); + storm::logic::OperatorInformation opInfo; + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo); + auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues( + env, this->getModel(), formula); + 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); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + rewardModel.get(), rewardPathFormula.getNonStrictBound()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } } @@ -209,215 +261,281 @@ std::unique_ptr SparseDtmcPrctlModelChecker std::unique_ptr SparseDtmcPrctlModelChecker::computeDiscountedCumulativeRewards( - Environment const& env, CheckTask const& checkTask) { - storm::logic::DiscountedCumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDiscountedCumulativeRewards( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), - rewardPathFormula.getNonStrictBound(), rewardPathFormula.getDiscountFactor()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented discounted cumulative rewards with intervals"); + } else { + storm::logic::DiscountedCumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDiscountedCumulativeRewards( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), + rewardPathFormula.getNonStrictBound(), rewardPathFormula.getDiscountFactor()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards( - Environment const& env, CheckTask const& checkTask) { - storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), - rewardPathFormula.getBound()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented instantaneous rewards with intervals"); + } else { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), + rewardPathFormula.getBound()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + if (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 && + checkTask.getUncertaintyResolutionMode() != UncertaintyResolutionMode::Cooperative, + storm::exceptions::InvalidSettingsException, + "Uncertainty resolution modes robust or cooperative not allowed if optimization direction is not stated explicitly."); + STORM_LOG_THROW(this->getModel().getTransitionMatrix().hasOnlyPositiveEntries(), storm::exceptions::InvalidSettingsException, + "Computing rewards on uncertain model requires graph-preservation."); + } std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityTimes( - Environment const& env, CheckTask const& checkTask) { - storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityTimes( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented reachability times with intervals"); + } else { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityTimes( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeTotalRewards( - Environment const& env, CheckTask const& checkTask) { - auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeTotalRewards( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), checkTask.getHint()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented total rewards with intervals"); + } else { + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeTotalRewards( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template<> std::unique_ptr SparseDtmcPrctlModelChecker>::computeDiscountedTotalRewards( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Discounted properties are not implemented for parametric models."); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeDiscountedTotalRewards( - Environment const& env, CheckTask const& checkTask) { - auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - storm::logic::DiscountedTotalRewardFormula const& rewardPathFormula = checkTask.getFormula(); - auto discountFactor = rewardPathFormula.getDiscountFactor(); - auto ret = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDiscountedTotalRewards( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), discountFactor, checkTask.getHint()); - std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret))); - return result; + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented discounted total rewards with intervals"); + } else { + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + storm::logic::DiscountedTotalRewardFormula const& rewardPathFormula = checkTask.getFormula(); + auto discountFactor = rewardPathFormula.getDiscountFactor(); + auto ret = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDiscountedTotalRewards( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), discountFactor, checkTask.getHint()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret))); + return result; + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities( - Environment const& env, CheckTask const& checkTask) { - storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(env, stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + Environment const& env, CheckTask const& checkTask) { + 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(); + std::unique_ptr subResultPointer = this->check(env, stateFormula); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageRewards( - Environment const& env, CheckTask const& checkTask) { - auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lra with intervals"); + } else { + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities( - Environment const& env, CheckTask const& checkTask) { - storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); - STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, - "Illegal conditional probability formula."); - STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, - "Illegal conditional probability formula."); - - std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); - std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented conditional probabilities with intervals"); + } else { + storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); + STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, + "Illegal conditional probability formula."); + STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, + "Illegal conditional probability formula."); + + std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalRewards( - Environment const& env, CheckTask const& checkTask) { - storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); - STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, - "Illegal conditional probability formula."); - STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, - "Illegal conditional probability formula."); - - std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asReachabilityRewardFormula().getSubformula()); - std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented conditional rewards with intervals"); + } else { + storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); + STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, + "Illegal conditional probability formula."); + STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, + "Illegal conditional probability formula."); + + std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asReachabilityRewardFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalRewards( - env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), - checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), - leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + std::vector numericResult = + storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalRewards( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), + checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), + leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template<> std::unique_ptr SparseDtmcPrctlModelChecker>::checkQuantileFormula( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Quantiles for parametric models are not implemented."); } template std::unique_ptr SparseDtmcPrctlModelChecker::checkQuantileFormula( - Environment const& env, CheckTask const& checkTask) { - STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, - "Computing quantiles is only supported for the initial states of a model."); - STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException, - "Quantiles not supported on models with multiple initial states."); - uint64_t initialState = *this->getModel().getInitialStates().begin(); - - helper::rewardbounded::QuantileHelper qHelper(this->getModel(), checkTask.getFormula()); - auto res = qHelper.computeQuantile(env); - - if (res.size() == 1 && res.front().size() == 1) { - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, std::move(res.front().front()))); + Environment const& env, CheckTask const& checkTask) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented quantile formulas with intervals"); } else { - return std::unique_ptr(new ExplicitParetoCurveCheckResult(initialState, std::move(res))); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, + "Computing quantiles is only supported for the initial states of a model."); + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException, + "Quantiles not supported on models with multiple initial states."); + uint64_t initialState = *this->getModel().getInitialStates().begin(); + + helper::rewardbounded::QuantileHelper qHelper(this->getModel(), checkTask.getFormula()); + auto res = qHelper.computeQuantile(env); + + if (res.size() == 1 && res.front().size() == 1) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, std::move(res.front().front()))); + } else { + return std::unique_ptr(new ExplicitParetoCurveCheckResult(initialState, std::move(res))); + } } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeSteadyStateDistribution(Environment const& env) { - // Initialize helper - storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); - - // Compute result - std::vector result; - auto const& initialStates = this->getModel().getInitialStates(); - uint64_t numInitStates = initialStates.getNumberOfSetBits(); - if (numInitStates == 1) { - result = helper.computeLongRunAverageStateDistribution(env, *initialStates.begin()); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented steady state distributions with intervals"); } else { - STORM_LOG_WARN("Multiple initial states found. A uniform distribution over initial states is assumed."); - ValueType initProb = storm::utility::one() / storm::utility::convertNumber(numInitStates); - result = helper.computeLongRunAverageStateDistribution(env, [&initialStates, &initProb](uint64_t const& stateIndex) { - return initialStates.get(stateIndex) ? initProb : storm::utility::zero(); - }); - } + // Initialize helper + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); + + // Compute result + std::vector result; + auto const& initialStates = this->getModel().getInitialStates(); + uint64_t numInitStates = initialStates.getNumberOfSetBits(); + if (numInitStates == 1) { + result = helper.computeLongRunAverageStateDistribution(env, *initialStates.begin()); + } else { + STORM_LOG_WARN("Multiple initial states found. A uniform distribution over initial states is assumed."); + ValueType initProb = storm::utility::one() / storm::utility::convertNumber(numInitStates); + result = helper.computeLongRunAverageStateDistribution(env, [&initialStates, &initProb](uint64_t const& stateIndex) { + return initialStates.get(stateIndex) ? initProb : storm::utility::zero(); + }); + } - // Return CheckResult - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + // Return CheckResult + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + } } template std::unique_ptr SparseDtmcPrctlModelChecker::computeExpectedVisitingTimes(Environment const& env) { - // Initialize helper - storm::modelchecker::helper::SparseDeterministicVisitingTimesHelper helper(this->getModel().getTransitionMatrix()); - - // Compute result - std::vector result; - auto const& initialStates = this->getModel().getInitialStates(); - uint64_t numInitStates = initialStates.getNumberOfSetBits(); - STORM_LOG_THROW(numInitStates > 0, storm::exceptions::InvalidOperationException, "No initial states given. Cannot compute expected visiting times."); - STORM_LOG_WARN_COND(numInitStates == 1, "Multiple initial states found. A uniform distribution over initial states is assumed."); - result = helper.computeExpectedVisitingTimes(env, initialStates); - - // Return CheckResult - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented expected visiting times with intervals"); + } else { + // Initialize helper + storm::modelchecker::helper::SparseDeterministicVisitingTimesHelper helper(this->getModel().getTransitionMatrix()); + + // Compute result + std::vector result; + auto const& initialStates = this->getModel().getInitialStates(); + uint64_t numInitStates = initialStates.getNumberOfSetBits(); + STORM_LOG_THROW(numInitStates > 0, storm::exceptions::InvalidOperationException, "No initial states given. Cannot compute expected visiting times."); + STORM_LOG_WARN_COND(numInitStates == 1, "Multiple initial states found. A uniform distribution over initial states is assumed."); + result = helper.computeExpectedVisitingTimes(env, initialStates); + + // Return CheckResult + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + } } 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 bff8aa3756..6372205cdc 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -11,6 +11,7 @@ class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker, double, ValueType>::type; explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model); @@ -18,47 +19,47 @@ class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker const& checkTask, bool* requiresSingleInitialState = nullptr); + static bool canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState = nullptr); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; + virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeNextProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeDiscountedCumulativeRewards( - Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, - CheckTask const& checkTask) override; + Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards( + Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeTotalRewards(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeDiscountedTotalRewards( - Environment const& env, CheckTask const& checkTask) override; + Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalRewards(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards( - Environment const& env, CheckTask const& checkTask) override; + Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr checkQuantileFormula(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; /*! * Computes the long run average (or: steady state) distribution over all states diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 16ce6c7bb5..765b0aa98e 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -1,6 +1,6 @@ #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,11 +37,11 @@ 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())) { + if (formula.isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setRewardOperatorsAllowed(true))) { return true; } } else { @@ -111,7 +111,7 @@ bool SparseMdpPrctlModelChecker::canHandle(CheckTask std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities( 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 bounded until with intervals"); return nullptr; } else { @@ -170,6 +170,10 @@ std::unique_ptr SparseMdpPrctlModelChecker::com storm::logic::UntilFormula 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 constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(checkTask.isUncertaintyResolutionModeSet(), storm::exceptions::InvalidSettingsException, + "Uncertainty resolution mode must be set for uncertain (interval) models."); + } std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -206,7 +210,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 +237,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(); @@ -362,6 +366,10 @@ std::unique_ptr SparseMdpPrctlModelChecker::com storm::logic::EventuallyFormula const& eventuallyFormula = 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 constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(checkTask.isUncertaintyResolutionModeSet(), storm::exceptions::InvalidSettingsException, + "Uncertainty resolution mode must be set for uncertain (interval) models."); + } std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); @@ -439,7 +447,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 +472,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 +493,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 +503,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 +518,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, diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 5672b67bc6..4c612ec86b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -41,103 +41,150 @@ std::map SparseDtmc return std::map(); } -template -std::map SparseDtmcPrctlHelper::computeRewardBoundedValues( +template +std::map SparseDtmcPrctlHelper::computeRewardBoundedValues( Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula) { - storm::utility::Stopwatch swAll(true), swBuild, swCheck; - - storm::modelchecker::helper::rewardbounded::MultiDimensionalRewardUnfolding rewardUnfolding(model, rewardBoundedFormula); - - // Get lower and upper bounds for the solution. - auto lowerBound = rewardUnfolding.getLowerObjectiveBound(); - auto upperBound = rewardUnfolding.getUpperObjectiveBound(); - - // Initialize epoch models - auto initEpoch = rewardUnfolding.getStartEpoch(); - auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); - - // initialize data that will be needed for each epoch - std::vector x, b; - std::unique_ptr> linEqSolver; - - Environment preciseEnv = env; - ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision( - initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); - preciseEnv.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber(precision)); - - // In case of cdf export we store the necessary data. - std::vector> cdfData; - - // Set the correct equation problem format. - storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - rewardUnfolding.setEquationSystemFormatForEpochModel(linearEquationSolverFactory.getEquationProblemFormat(preciseEnv)); - - storm::utility::ProgressMeasurement progress("epochs"); - progress.setMaxCount(epochOrder.size()); - progress.startNewMeasurement(0); - uint64_t numCheckedEpochs = 0; - for (auto const& epoch : epochOrder) { - swBuild.start(); - auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); - swBuild.stop(); - swCheck.start(); - rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, x, b, linEqSolver, lowerBound, upperBound)); - swCheck.stop(); - if (storm::settings::getModule().isExportCdfSet() && - !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { - std::vector cdfEntry; - for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { - uint64_t offset = rewardUnfolding.getDimension(i).boundType == helper::rewardbounded::DimensionBoundType::LowerBound ? 1 : 0; - cdfEntry.push_back(storm::utility::convertNumber(rewardUnfolding.getEpochManager().getDimensionOfEpoch(epoch, i) + offset) * - rewardUnfolding.getDimension(i).scalingFactor); + 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; + + storm::modelchecker::helper::rewardbounded::MultiDimensionalRewardUnfolding rewardUnfolding(model, rewardBoundedFormula); + + // Get lower and upper bounds for the solution. + auto lowerBound = rewardUnfolding.getLowerObjectiveBound(); + auto upperBound = rewardUnfolding.getUpperObjectiveBound(); + + // Initialize epoch models + auto initEpoch = rewardUnfolding.getStartEpoch(); + auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); + + // initialize data that will be needed for each epoch + std::vector x, b; + std::unique_ptr> linEqSolver; + + Environment preciseEnv = env; + ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision( + initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); + preciseEnv.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber(precision)); + + // In case of cdf export we store the necessary data. + std::vector> cdfData; + + // Set the correct equation problem format. + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + rewardUnfolding.setEquationSystemFormatForEpochModel(linearEquationSolverFactory.getEquationProblemFormat(preciseEnv)); + + storm::utility::ProgressMeasurement progress("epochs"); + progress.setMaxCount(epochOrder.size()); + progress.startNewMeasurement(0); + uint64_t numCheckedEpochs = 0; + for (auto const& epoch : epochOrder) { + swBuild.start(); + auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + swBuild.stop(); + swCheck.start(); + rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, x, b, linEqSolver, lowerBound, upperBound)); + swCheck.stop(); + if (storm::settings::getModule().isExportCdfSet() && + !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { + std::vector cdfEntry; + for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { + uint64_t offset = rewardUnfolding.getDimension(i).boundType == helper::rewardbounded::DimensionBoundType::LowerBound ? 1 : 0; + cdfEntry.push_back(storm::utility::convertNumber(rewardUnfolding.getEpochManager().getDimensionOfEpoch(epoch, i) + offset) * + rewardUnfolding.getDimension(i).scalingFactor); + } + cdfEntry.push_back(rewardUnfolding.getInitialStateResult(epoch)); + cdfData.push_back(std::move(cdfEntry)); + } + ++numCheckedEpochs; + progress.updateProgress(numCheckedEpochs); + if (storm::utility::resources::isTerminate()) { + break; } - cdfEntry.push_back(rewardUnfolding.getInitialStateResult(epoch)); - cdfData.push_back(std::move(cdfEntry)); } - ++numCheckedEpochs; - progress.updateProgress(numCheckedEpochs); - if (storm::utility::resources::isTerminate()) { - break; + + std::map result; + for (auto initState : model.getInitialStates()) { + result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState); } - } - std::map result; - for (auto initState : model.getInitialStates()) { - result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState); - } + swAll.stop(); - swAll.stop(); + if (storm::settings::getModule().isExportCdfSet()) { + std::vector headers; + for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { + headers.push_back(rewardUnfolding.getDimension(i).formula->toString()); + } + headers.push_back("Result"); + storm::io::exportDataToCSVFile( + storm::settings::getModule().getExportCdfDirectory() + "cdf.csv", cdfData, headers); + } - if (storm::settings::getModule().isExportCdfSet()) { - std::vector headers; - for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { - headers.push_back(rewardUnfolding.getDimension(i).formula->toString()); + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("---------------------------------\n"); + STORM_PRINT_AND_LOG("Statistics:\n"); + STORM_PRINT_AND_LOG("---------------------------------\n"); + STORM_PRINT_AND_LOG(" #checked epochs: " << epochOrder.size() << ".\n"); + STORM_PRINT_AND_LOG(" overall Time: " << swAll << ".\n"); + STORM_PRINT_AND_LOG("Epoch Model building Time: " << swBuild << ".\n"); + STORM_PRINT_AND_LOG("Epoch Model checking Time: " << swCheck << ".\n"); + STORM_PRINT_AND_LOG("---------------------------------\n"); } - headers.push_back("Result"); - storm::io::exportDataToCSVFile( - storm::settings::getModule().getExportCdfDirectory() + "cdf.csv", cdfData, headers); + + return result; } +} - if (storm::settings::getModule().isShowStatisticsSet()) { - STORM_PRINT_AND_LOG("---------------------------------\n"); - STORM_PRINT_AND_LOG("Statistics:\n"); - STORM_PRINT_AND_LOG("---------------------------------\n"); - STORM_PRINT_AND_LOG(" #checked epochs: " << epochOrder.size() << ".\n"); - STORM_PRINT_AND_LOG(" overall Time: " << swAll << ".\n"); - STORM_PRINT_AND_LOG("Epoch Model building Time: " << swBuild << ".\n"); - STORM_PRINT_AND_LOG("Epoch Model checking Time: " << swCheck << ".\n"); - STORM_PRINT_AND_LOG("---------------------------------\n"); +template +std::vector computeRobustValuesForMaybeStates(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix&& submatrix, std::vector const& b, + bool computeReward) { + // Initialize the solution vector. + std::vector x = std::vector(submatrix.getRowGroupCount(), storm::utility::zero()); + + // Set up the solver. + storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver( + env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix), + convert(OptimizationDirection::Maximize)); // default to maximize for IDTMCs; does not affect the result + solver->setUncertaintyResolutionMode(goal.getUncertaintyResolutionMode()); + solver->setHasUniqueSolution(false); + solver->setHasNoEndComponents(false); + + // check requirements of solver + if (!computeReward) { + solver->setLowerBound(storm::utility::zero()); + solver->setUpperBound(storm::utility::one()); } - return result; + auto req = solver->getRequirements(env); + if (!computeReward) { + req.clearBounds(); + } else { + req.clearLowerBounds(); + // TODO: to compute the upper bound for expected rewards of interval models, one needs to implement the functionality of + // `DsMpiMdpUpperRewardBoundsComputer` for IMCs. + // As the robust VI does not use the lower and upper bounds, we are okay for now to just clear the requirement. + req.clearUpperBounds(); + } + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, + "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); + + solver->setRequirementsChecked(); + + // Solve the corresponding system of equations. + solver->solveEquations(env, x, b); + + return x; } -template -std::vector SparseDtmcPrctlHelper::computeUntilProbabilities( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeUntilProbabilities( + 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, bool qualitative, ModelCheckerHint const& hint) { - std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // We need to identify the maybe states (states which have a probability for satisfying the until formula // that is strictly between 0 and 1) and the states that satisfy the formula with probability 1. @@ -147,13 +194,13 @@ std::vector SparseDtmcPrctlHelper::comput maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); // Treat the states with probability one - std::vector const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint().getResultHint(); + std::vector const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint().getResultHint(); statesWithProbability1 = storm::storage::BitVector(maybeStates.size(), false); storm::storage::BitVector nonMaybeStates = ~maybeStates; for (auto state : nonMaybeStates) { if (storm::utility::isOne(resultsForNonMaybeStates[state])) { statesWithProbability1.set(state, true); - result[state] = storm::utility::one(); + result[state] = storm::utility::one(); } else { STORM_LOG_THROW(storm::utility::isZero(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException, "Expected that the result hint specifies probabilities in {0,1} for non-maybe states"); @@ -175,8 +222,8 @@ std::vector SparseDtmcPrctlHelper::comput << " states remaining)."); // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); - storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); } // Check if the values of the maybe states are relevant for the SolveGoal @@ -185,186 +232,226 @@ std::vector SparseDtmcPrctlHelper::comput // Check whether we need to compute exact probabilities for some states. if (qualitative || maybeStatesNotRelevant) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. - storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::convertNumber(0.5)); + storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::convertNumber(0.5)); } else { if (!maybeStates.empty()) { // In this case we have to compute the probabilities. + if constexpr (storm::IsIntervalType) { + // Compute probabilities in a robust fashion by using the logic as for MDPs + storm::storage::SparseMatrix submatrix; + std::vector b; + + submatrix = transitionMatrix.filterEntries(transitionMatrix.getRowFilter(maybeStates)); + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some state that has probability 1. + storm::utility::vector::setAllValues(b, transitionMatrix.getRowFilter(statesWithProbability1)); + + std::vector x = computeRobustValuesForMaybeStates(env, std::move(goal), std::move(submatrix), b, false); + + // Set values of resulting vector according to result. + storm::utility::vector::setVectorValues(result, maybeStates, x); + } else { + // Check whether we need to convert the input to equation system format. + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + bool convertToEquationSystem = + linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + + // We can eliminate the rows and columns from the original transition probability matrix. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, convertToEquationSystem); + if (convertToEquationSystem) { + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } + + // Initialize the x vector with the hint (if available) or with 0.5 for each element. + // This is the initial guess for the iterative solvers. It should be safe as for all + // 'maybe' states we know that the probability is strictly larger than 0. + std::vector x; + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { + x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + } else { + x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); + } + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some 'yes' state. + std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); + + // Now solve the created system of linear equations. + goal.restrictRelevantValues(maybeStates); + std::unique_ptr> solver = + storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); + solver->setBounds(storm::utility::zero(), storm::utility::one()); + solver->solveEquations(env, x, b); + + // Set values of resulting vector according to result. + storm::utility::vector::setVectorValues(result, maybeStates, x); + } + } + } + return result; +} + +template +std::vector SparseDtmcPrctlHelper::computeAllUntilProbabilities( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing all until probabilities with interval models."); + } else { + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); + std::vector result(numberOfStates, storm::utility::zero()); + + // All states are relevant + storm::storage::BitVector relevantStates(numberOfStates, true); + // Compute exact probabilities for some states. + if (!relevantStates.empty()) { // Check whether we need to convert the input to equation system format. storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; - // We can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, convertToEquationSystem); + storm::storage::SparseMatrix submatrix(transitionMatrix); + submatrix.makeRowsAbsorbing(phiStates); + submatrix.makeRowsAbsorbing(psiStates); + // submatrix.deleteDiagonalEntries(psiStates); + // storm::storage::BitVector failState(numberOfStates, false); + // failState.set(0, true); + submatrix.deleteDiagonalEntries(); + submatrix = submatrix.transpose(); + submatrix = submatrix.getSubmatrix(true, relevantStates, relevantStates, convertToEquationSystem); + if (convertToEquationSystem) { // Converting the matrix from the fixpoint notation to the form needed for the equation // system. That is, we go from x = A*x + b to (I-A)x = b. submatrix.convertToEquationSystem(); } - // Initialize the x vector with the hint (if available) or with 0.5 for each element. + // Initialize the x vector with 0.5 for each element. // This is the initial guess for the iterative solvers. It should be safe as for all // 'maybe' states we know that the probability is strictly larger than 0. - std::vector x; - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { - x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); - } else { - x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); - } + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); - // Prepare the right-hand side of the equation system. For entry i this corresponds to - // the accumulated probability of going from state i to some 'yes' state. - std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); + // Prepare the right-hand side of the equation system. + std::vector b(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + // Set initial states + size_t i = 0; + ValueType initDist = storm::utility::one() / storm::utility::convertNumber(initialStates.getNumberOfSetBits()); + for (auto state : relevantStates) { + if (initialStates.get(state)) { + b[i] = initDist; + } + ++i; + } // Now solve the created system of linear equations. - goal.restrictRelevantValues(maybeStates); + goal.restrictRelevantValues(relevantStates); std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->solveEquations(env, x, b); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, x); + storm::utility::vector::setVectorValues(result, relevantStates, x); } + return result; } - return result; -} - -template -std::vector SparseDtmcPrctlHelper::computeAllUntilProbabilities( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); - std::vector result(numberOfStates, storm::utility::zero()); - - // All states are relevant - storm::storage::BitVector relevantStates(numberOfStates, true); - - // Compute exact probabilities for some states. - if (!relevantStates.empty()) { - // Check whether we need to convert the input to equation system format. - storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - bool convertToEquationSystem = - linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; - - storm::storage::SparseMatrix submatrix(transitionMatrix); - submatrix.makeRowsAbsorbing(phiStates); - submatrix.makeRowsAbsorbing(psiStates); - // submatrix.deleteDiagonalEntries(psiStates); - // storm::storage::BitVector failState(numberOfStates, false); - // failState.set(0, true); - submatrix.deleteDiagonalEntries(); - submatrix = submatrix.transpose(); - submatrix = submatrix.getSubmatrix(true, relevantStates, relevantStates, convertToEquationSystem); - - if (convertToEquationSystem) { - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix.convertToEquationSystem(); - } - - // Initialize the x vector with 0.5 for each element. - // This is the initial guess for the iterative solvers. It should be safe as for all - // 'maybe' states we know that the probability is strictly larger than 0. - std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); - - // Prepare the right-hand side of the equation system. - std::vector b(relevantStates.getNumberOfSetBits(), storm::utility::zero()); - // Set initial states - size_t i = 0; - ValueType initDist = storm::utility::one() / storm::utility::convertNumber(initialStates.getNumberOfSetBits()); - for (auto state : relevantStates) { - if (initialStates.get(state)) { - b[i] = initDist; - } - ++i; - } - - // Now solve the created system of linear equations. - goal.restrictRelevantValues(relevantStates); - std::unique_ptr> solver = - storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); - solver->setBounds(storm::utility::zero(), storm::utility::one()); - solver->solveEquations(env, x, b); - - // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, relevantStates, x); - } - return result; } -template -std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative) { - goal.oneMinus(); - std::vector result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, - storm::storage::BitVector(transitionMatrix.getRowCount(), true), ~psiStates, qualitative); - for (auto& entry : result) { - entry = storm::utility::one() - entry; + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing globally probabilities with interval models."); + } else { + goal.oneMinus(); + std::vector result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, + storm::storage::BitVector(transitionMatrix.getRowCount(), true), ~psiStates, qualitative); + for (auto& entry : result) { + entry = storm::utility::one() - entry; + } + return result; } - return result; } -template -std::vector SparseDtmcPrctlHelper::computeNextProbabilities( +template +std::vector SparseDtmcPrctlHelper::computeNextProbabilities( Environment const& env, 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.getRowCount()); - storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support next probabilities with interval models."); + } else { + // Create the vector with which to multiply and initialize it correctly. + std::vector result(transitionMatrix.getRowCount()); + storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); - // Perform one single matrix-vector multiplication. - auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->multiply(env, result, nullptr, result); - return result; + // Perform one single matrix-vector multiplication. + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->multiply(env, result, nullptr, result); + return result; + } } -template -std::vector SparseDtmcPrctlHelper::computeCumulativeRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeCumulativeRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound) { - // Initialize result to the null vector. - std::vector result(transitionMatrix.getRowCount()); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support cumulative rewards with interval models."); + } else { + // Initialize result to the null vector. + std::vector result(transitionMatrix.getRowCount()); - // Compute the reward vector to add in each step based on the available reward models. - std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); + // Compute the reward vector to add in each step based on the available reward models. + std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); - // Perform the matrix vector multiplication as often as required by the formula bound. - auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->repeatedMultiply(env, result, &totalRewardVector, stepBound); + // Perform the matrix vector multiplication as often as required by the formula bound. + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->repeatedMultiply(env, result, &totalRewardVector, stepBound); - return result; + return result; + } } -template -std::vector SparseDtmcPrctlHelper::computeInstantaneousRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeInstantaneousRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount) { - // Only compute the result if the model has a state-based reward this->getModel(). - STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, - "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0."); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support instantaneous rewards with interval models."); + } else { + // Only compute the result if the model has a state-based reward this->getModel(). + STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, + "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0."); - // Initialize result to state rewards of the model. - std::vector result = rewardModel.getStateRewardVector(); + // Initialize result to state rewards of the model. + std::vector result = rewardModel.getStateRewardVector(); - // Perform the matrix vector multiplication as often as required by the formula bound. - auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->repeatedMultiply(env, result, nullptr, stepCount); + // Perform the matrix vector multiplication as often as required by the formula bound. + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->repeatedMultiply(env, result, nullptr, stepCount); - return result; + return result; + } } -template -std::vector SparseDtmcPrctlHelper::computeTotalRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeTotalRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, ModelCheckerHint const& hint) { - // Identify the states from which only states with zero reward are reachable. - // We can then compute reachability rewards assuming these states as target set. - storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(transitionMatrix); - storm::storage::BitVector rew0States = storm::utility::graph::performProbGreater0(backwardTransitions, statesWithoutReward, ~statesWithoutReward); - rew0States.complement(); - return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0States, qualitative, hint); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing total rewards with interval models."); + } else { + // Identify the states from which only states with zero reward are reachable. + // We can then compute reachability rewards assuming these states as target set. + storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(transitionMatrix); + storm::storage::BitVector rew0States = storm::utility::graph::performProbGreater0(backwardTransitions, statesWithoutReward, ~statesWithoutReward); + rew0States.complement(); + return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0States, qualitative, hint); + } } template<> @@ -376,23 +463,27 @@ std::vector SparseDtmcPrctlHelper -std::vector SparseDtmcPrctlHelper::computeDiscountedCumulativeRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeDiscountedCumulativeRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, ValueType discountFactor) { - // Only compute the result if the model has at least one reward this->getModel(). - STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support discounted cumulative rewards with interval models."); + } else { + // Only compute the result if the model has at least one reward this->getModel(). + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - // Compute the reward vector to add in each step based on the available reward models. - std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); + // Compute the reward vector to add in each step based on the available reward models. + std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); - // Initialize result to the zero vector. - std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // Initialize result to the zero vector. + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->repeatedMultiplyWithFactor(env, result, &totalRewardVector, stepBound, discountFactor); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->repeatedMultiplyWithFactor(env, result, &totalRewardVector, stepBound, discountFactor); - return result; + return result; + } } template<> @@ -406,28 +497,32 @@ std::vector SparseDtmcPrctlHelper -std::vector SparseDtmcPrctlHelper::computeDiscountedTotalRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeDiscountedTotalRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, ValueType discountFactor, ModelCheckerHint const& hint) { - // If the solver is set to force exact results, throw an error if the method is not explicitly set to a value iteration type. - STORM_LOG_THROW(!env.solver().isForceExact(), storm::exceptions::NotSupportedException, - "Exact solving of discounted total reward objectives is currently not supported."); - - // Reduce to reachability rewards - std::vector b; - - std::vector x = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - b = rewardModel.getTotalRewardVector(transitionMatrix); - storm::modelchecker::helper::DiscountingHelper discountingHelper(transitionMatrix, discountFactor); - discountingHelper.solveWithDiscountedValueIteration(env, std::nullopt, x, b); - return std::vector(std::move(x)); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support discounted total rewards with interval models."); + } else { + // If the solver is set to force exact results, throw an error if the method is not explicitly set to a value iteration type. + STORM_LOG_THROW(!env.solver().isForceExact(), storm::exceptions::NotSupportedException, + "Exact solving of discounted total reward objectives is currently not supported."); + + // Reduce to reachability rewards + std::vector b; + + std::vector x = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + b = rewardModel.getTotalRewardVector(transitionMatrix); + storm::modelchecker::helper::DiscountingHelper discountingHelper(transitionMatrix, discountFactor); + discountingHelper.solveWithDiscountedValueIteration(env, std::nullopt, x, b); + return std::vector(std::move(x)); + } } -template -std::vector SparseDtmcPrctlHelper::computeReachabilityRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeReachabilityRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint) { return computeReachabilityRewards( @@ -438,41 +533,49 @@ std::vector SparseDtmcPrctlHelper::comput targetStates, qualitative, [&]() { return rewardModel.getStatesWithZeroReward(transitionMatrix); }, hint); } -template -std::vector SparseDtmcPrctlHelper::computeReachabilityRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeReachabilityRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint) { return computeReachabilityRewards( env, std::move(goal), transitionMatrix, backwardTransitions, [&](uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const& maybeStates) { - std::vector result(numberOfRows); + std::vector result(numberOfRows, storm::utility::zero()); storm::utility::vector::selectVectorValues(result, maybeStates, totalStateRewardVector); return result; }, targetStates, qualitative, [&]() { return storm::utility::vector::filterZero(totalStateRewardVector); }, hint); } -template -std::vector SparseDtmcPrctlHelper::computeReachabilityTimes( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeReachabilityTimes( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint) { - return computeReachabilityRewards( - env, std::move(goal), transitionMatrix, backwardTransitions, - [&](uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const&) { - return std::vector(numberOfRows, storm::utility::one()); - }, - targetStates, qualitative, [&]() { return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false); }, hint); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing reachability times with interval models."); + } else { + return computeReachabilityRewards( + env, std::move(goal), transitionMatrix, backwardTransitions, + [&](uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const&) { + return std::vector(numberOfRows, storm::utility::one()); + }, + targetStates, qualitative, [&]() { return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false); }, hint); + } } // This function computes an upper bound on the reachability rewards (see Baier et al, CAV'17). -template -std::vector computeUpperRewardBounds(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& rewards, - std::vector const& oneStepTargetProbabilities) { - DsMpiDtmcUpperRewardBoundsComputer dsmpi(transitionMatrix, rewards, oneStepTargetProbabilities); - std::vector bounds = dsmpi.computeUpperBounds(); - return bounds; +template +std::vector computeUpperRewardBounds(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& rewards, + std::vector const& oneStepTargetProbabilities) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing upper reward bounds with interval models."); + } else { + DsMpiDtmcUpperRewardBoundsComputer dsmpi(transitionMatrix, rewards, oneStepTargetProbabilities); + std::vector bounds = dsmpi.computeUpperBounds(); + return bounds; + } } template<> @@ -482,15 +585,15 @@ std::vector computeUpperRewardBounds(storm::storage::Sp STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing upper reward bounds is not supported for rational functions."); } -template -std::vector SparseDtmcPrctlHelper::computeReachabilityRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeReachabilityRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, std::function const& zeroRewardStatesGetter, ModelCheckerHint const& hint) { - std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // Determine which states have reward zero storm::storage::BitVector rew0States; @@ -504,7 +607,7 @@ std::vector SparseDtmcPrctlHelper::comput storm::storage::BitVector maybeStates; if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); - storm::utility::vector::setVectorValues(result, ~(maybeStates | rew0States), storm::utility::infinity()); + storm::utility::vector::setVectorValues(result, ~(maybeStates | rew0States), storm::utility::infinity()); STORM_LOG_INFO("Preprocessing: " << rew0States.getNumberOfSetBits() << " States with reward zero (" << maybeStates.getNumberOfSetBits() << " states remaining)."); @@ -517,7 +620,7 @@ std::vector SparseDtmcPrctlHelper::comput STORM_LOG_INFO("Preprocessing: " << infinityStates.getNumberOfSetBits() << " states with reward infinity, " << rew0States.getNumberOfSetBits() << " states with reward zero (" << maybeStates.getNumberOfSetBits() << " states remaining)."); - storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); } // Check if the values of the maybe states are relevant for the SolveGoal @@ -527,121 +630,170 @@ std::vector SparseDtmcPrctlHelper::comput if (qualitative || maybeStatesNotRelevant) { // Set the values for all maybe-states to 1 to indicate that their reward values // are neither 0 nor infinity. - storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::one()); + storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::one()); } else { if (!maybeStates.empty()) { - // Check whether we need to convert the input to equation system format. - storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - bool convertToEquationSystem = - linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + if constexpr (storm::IsIntervalType) { + // In this case we have to compute the reward values for the remaining states. + // We can eliminate the rows and columns from the original transition probability matrix. + storm::storage::SparseMatrix submatrix = transitionMatrix.filterEntries(transitionMatrix.getRowFilter(maybeStates)); - // In this case we have to compute the reward values for the remaining states. - // We can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, convertToEquationSystem); + // Prepare the right-hand side of the equation system. + std::vector b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); - // Initialize the x vector with the hint (if available) or with 1 for each element. - // This is the initial guess for the iterative solvers. - std::vector x; - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { - x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + // Compute values for maybe states. + std::vector x = computeRobustValuesForMaybeStates(env, std::move(goal), std::move(submatrix), b, true); + + // Set values of resulting vector according to result. + storm::utility::vector::setVectorValues(result, maybeStates, x); } else { - x = std::vector(submatrix.getColumnCount(), storm::utility::one()); - } + // Check whether we need to convert the input to equation system format. + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + bool convertToEquationSystem = + linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + + // In this case we have to compute the reward values for the remaining states. + // We can eliminate the rows and columns from the original transition probability matrix. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, convertToEquationSystem); + + // Initialize the x vector with the hint (if available) or with 1 for each element. + // This is the initial guess for the iterative solvers. + std::vector x; + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { + x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + } else { + x = std::vector(submatrix.getColumnCount(), storm::utility::one()); + } - // Prepare the right-hand side of the equation system. - std::vector b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); - - storm::solver::LinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env); - boost::optional> upperRewardBounds; - requirements.clearLowerBounds(); - if (requirements.upperBounds()) { - upperRewardBounds = computeUpperRewardBounds(submatrix, b, transitionMatrix.getConstrainedRowSumVector(maybeStates, rew0States)); - requirements.clearUpperBounds(); - } - STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, - "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); + // Prepare the right-hand side of the equation system. + std::vector b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); - // If necessary, convert the matrix from the fixpoint notation to the form needed for the equation system. - if (convertToEquationSystem) { - // go from x = A*x + b to (I-A)x = b. - submatrix.convertToEquationSystem(); - } + storm::solver::LinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env); + boost::optional> upperRewardBounds; + requirements.clearLowerBounds(); + if (requirements.upperBounds()) { + upperRewardBounds = computeUpperRewardBounds(submatrix, b, transitionMatrix.getConstrainedRowSumVector(maybeStates, rew0States)); + requirements.clearUpperBounds(); + } + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, + "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); - // Create the solver. - goal.restrictRelevantValues(maybeStates); - std::unique_ptr> solver = - storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); - solver->setLowerBound(storm::utility::zero()); - if (upperRewardBounds) { - solver->setUpperBounds(std::move(upperRewardBounds.get())); - } + // If necessary, convert the matrix from the fixpoint notation to the form needed for the equation system. + if (convertToEquationSystem) { + // go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } - // Now solve the resulting equation system. - solver->solveEquations(env, x, b); + // Create the solver. + goal.restrictRelevantValues(maybeStates); + std::unique_ptr> solver = + storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); + solver->setLowerBound(storm::utility::zero()); + if (upperRewardBounds) { + solver->setUpperBounds(std::move(upperRewardBounds.get())); + } - // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, x); + // Now solve the resulting equation system. + solver->solveEquations(env, x, b); + + // Set values of resulting vector according to result. + storm::utility::vector::setVectorValues(result, maybeStates, x); + } } } return result; } -template -typename SparseDtmcPrctlHelper::BaierTransformedModel SparseDtmcPrctlHelper::computeBaierTransformation( - Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, - boost::optional> const& stateRewards) { - BaierTransformedModel result; - - // Start by computing all 'before' states, i.e. the states for which the conditional probability is defined. - std::vector probabilitiesToReachConditionStates = - computeUntilProbabilities(env, storm::solver::SolveGoal(), transitionMatrix, backwardTransitions, - storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false); - - result.beforeStates = storm::storage::BitVector(targetStates.size(), true); - uint_fast64_t state = 0; - uint_fast64_t beforeStateIndex = 0; - for (auto const& value : probabilitiesToReachConditionStates) { - if (value == storm::utility::zero()) { - result.beforeStates.set(state, false); - } else { - probabilitiesToReachConditionStates[beforeStateIndex] = value; - ++beforeStateIndex; +template +typename SparseDtmcPrctlHelper::BaierTransformedModel +SparseDtmcPrctlHelper::computeBaierTransformation(Environment const& env, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& conditionStates, + boost::optional> const& stateRewards) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support baier transformation with interval models."); + } else { + BaierTransformedModel result; + + // Start by computing all 'before' states, i.e. the states for which the conditional probability is defined. + std::vector probabilitiesToReachConditionStates = + computeUntilProbabilities(env, storm::solver::SolveGoal(), transitionMatrix, backwardTransitions, + storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false); + + result.beforeStates = storm::storage::BitVector(targetStates.size(), true); + uint_fast64_t state = 0; + uint_fast64_t beforeStateIndex = 0; + for (auto const& value : probabilitiesToReachConditionStates) { + if (value == storm::utility::zero()) { + result.beforeStates.set(state, false); + } else { + probabilitiesToReachConditionStates[beforeStateIndex] = value; + ++beforeStateIndex; + } + ++state; } - ++state; - } - probabilitiesToReachConditionStates.resize(beforeStateIndex); + probabilitiesToReachConditionStates.resize(beforeStateIndex); - if (targetStates.empty()) { - result.noTargetStates = true; - return result; - } else if (!result.beforeStates.empty()) { - // If there are some states for which the conditional probability is defined and there are some - // states that can reach the target states without visiting condition states first, we need to - // do more work. - - // First, compute the relevant states and some offsets. - storm::storage::BitVector allStates(targetStates.size(), true); - std::vector numberOfBeforeStatesUpToState = result.beforeStates.getNumberOfSetBitsBeforeIndices(); - storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, targetStates); - statesWithProbabilityGreater0 &= storm::utility::graph::getReachableStates(transitionMatrix, conditionStates, allStates, targetStates); - uint_fast64_t normalStatesOffset = result.beforeStates.getNumberOfSetBits(); - std::vector numberOfNormalStatesUpToState = statesWithProbabilityGreater0.getNumberOfSetBitsBeforeIndices(); - - // All transitions going to states with probability zero, need to be redirected to a deadlock state. - bool addDeadlockState = false; - uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.getNumberOfSetBits(); - - // Now, we create the matrix of 'before' and 'normal' states. - storm::storage::SparseMatrixBuilder builder; - - // Start by creating the transitions of the 'before' states. - uint_fast64_t currentRow = 0; - for (auto beforeState : result.beforeStates) { - if (conditionStates.get(beforeState)) { - // For condition states, we move to the 'normal' states. + if (targetStates.empty()) { + result.noTargetStates = true; + return result; + } else if (!result.beforeStates.empty()) { + // If there are some states for which the conditional probability is defined and there are some + // states that can reach the target states without visiting condition states first, we need to + // do more work. + + // First, compute the relevant states and some offsets. + storm::storage::BitVector allStates(targetStates.size(), true); + std::vector numberOfBeforeStatesUpToState = result.beforeStates.getNumberOfSetBitsBeforeIndices(); + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, targetStates); + statesWithProbabilityGreater0 &= storm::utility::graph::getReachableStates(transitionMatrix, conditionStates, allStates, targetStates); + uint_fast64_t normalStatesOffset = result.beforeStates.getNumberOfSetBits(); + std::vector numberOfNormalStatesUpToState = statesWithProbabilityGreater0.getNumberOfSetBitsBeforeIndices(); + + // All transitions going to states with probability zero, need to be redirected to a deadlock state. + bool addDeadlockState = false; + uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.getNumberOfSetBits(); + + // Now, we create the matrix of 'before' and 'normal' states. + storm::storage::SparseMatrixBuilder builder; + + // Start by creating the transitions of the 'before' states. + uint_fast64_t currentRow = 0; + for (auto beforeState : result.beforeStates) { + if (conditionStates.get(beforeState)) { + // For condition states, we move to the 'normal' states. + ValueType zeroProbability = storm::utility::zero(); + for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) { + if (statesWithProbabilityGreater0.get(successorEntry.getColumn())) { + builder.addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()], + successorEntry.getValue()); + } else { + zeroProbability += successorEntry.getValue(); + } + } + if (!storm::utility::isZero(zeroProbability)) { + builder.addNextValue(currentRow, deadlockState, zeroProbability); + } + } else { + // For non-condition states, we scale the probabilities going to other before states. + for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) { + if (result.beforeStates.get(successorEntry.getColumn())) { + builder.addNextValue(currentRow, numberOfBeforeStatesUpToState[successorEntry.getColumn()], + successorEntry.getValue() * + probabilitiesToReachConditionStates[numberOfBeforeStatesUpToState[successorEntry.getColumn()]] / + probabilitiesToReachConditionStates[currentRow]); + } + } + } + ++currentRow; + } + + // Then, create the transitions of the 'normal' states. + for (auto state : statesWithProbabilityGreater0) { ValueType zeroProbability = storm::utility::zero(); - for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) { + for (auto const& successorEntry : transitionMatrix.getRow(state)) { if (statesWithProbabilityGreater0.get(successorEntry.getColumn())) { builder.addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()], successorEntry.getValue()); @@ -650,73 +802,47 @@ typename SparseDtmcPrctlHelper::BaierTransformedMode } } if (!storm::utility::isZero(zeroProbability)) { + addDeadlockState = true; builder.addNextValue(currentRow, deadlockState, zeroProbability); } - } else { - // For non-condition states, we scale the probabilities going to other before states. - for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) { - if (result.beforeStates.get(successorEntry.getColumn())) { - builder.addNextValue(currentRow, numberOfBeforeStatesUpToState[successorEntry.getColumn()], - successorEntry.getValue() * - probabilitiesToReachConditionStates[numberOfBeforeStatesUpToState[successorEntry.getColumn()]] / - probabilitiesToReachConditionStates[currentRow]); - } - } + ++currentRow; } - ++currentRow; - } - - // Then, create the transitions of the 'normal' states. - for (auto state : statesWithProbabilityGreater0) { - ValueType zeroProbability = storm::utility::zero(); - for (auto const& successorEntry : transitionMatrix.getRow(state)) { - if (statesWithProbabilityGreater0.get(successorEntry.getColumn())) { - builder.addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()], successorEntry.getValue()); - } else { - zeroProbability += successorEntry.getValue(); - } - } - if (!storm::utility::isZero(zeroProbability)) { - addDeadlockState = true; - builder.addNextValue(currentRow, deadlockState, zeroProbability); + if (addDeadlockState) { + builder.addNextValue(deadlockState, deadlockState, storm::utility::one()); } - ++currentRow; - } - if (addDeadlockState) { - builder.addNextValue(deadlockState, deadlockState, storm::utility::one()); - } - // Build the new transition matrix and the new targets. - result.transitionMatrix = builder.build(addDeadlockState ? (deadlockState + 1) : deadlockState); - storm::storage::BitVector newTargetStates = targetStates % result.beforeStates; - newTargetStates.resize(result.transitionMatrix.get().getRowCount()); - for (auto state : targetStates % statesWithProbabilityGreater0) { - newTargetStates.set(normalStatesOffset + state, true); - } - result.targetStates = std::move(newTargetStates); + // Build the new transition matrix and the new targets. + result.transitionMatrix = builder.build(addDeadlockState ? (deadlockState + 1) : deadlockState); + storm::storage::BitVector newTargetStates = targetStates % result.beforeStates; + newTargetStates.resize(result.transitionMatrix.get().getRowCount()); + for (auto state : targetStates % statesWithProbabilityGreater0) { + newTargetStates.set(normalStatesOffset + state, true); + } + result.targetStates = std::move(newTargetStates); - // If a reward model was given, we need to compute the rewards for the transformed model. - if (stateRewards) { - std::vector newStateRewards(result.beforeStates.getNumberOfSetBits()); - storm::utility::vector::selectVectorValues(newStateRewards, result.beforeStates, stateRewards.get()); + // If a reward model was given, we need to compute the rewards for the transformed model. + if (stateRewards) { + std::vector newStateRewards(result.beforeStates.getNumberOfSetBits()); + storm::utility::vector::selectVectorValues(newStateRewards, result.beforeStates, stateRewards.get()); - newStateRewards.reserve(result.transitionMatrix.get().getRowCount()); - for (auto state : statesWithProbabilityGreater0) { - newStateRewards.push_back(stateRewards.get()[state]); - } - // Add a zero reward to the deadlock state. - if (addDeadlockState) { - newStateRewards.push_back(storm::utility::zero()); + newStateRewards.reserve(result.transitionMatrix.get().getRowCount()); + for (auto state : statesWithProbabilityGreater0) { + newStateRewards.push_back(stateRewards.get()[state]); + } + // Add a zero reward to the deadlock state. + if (addDeadlockState) { + newStateRewards.push_back(storm::utility::zero()); + } + result.stateRewards = std::move(newStateRewards); } - result.stateRewards = std::move(newStateRewards); } - } - return result; + return result; + } } -template -storm::storage::BitVector SparseDtmcPrctlHelper::BaierTransformedModel::getNewRelevantStates() const { +template +storm::storage::BitVector SparseDtmcPrctlHelper::BaierTransformedModel::getNewRelevantStates() const { storm::storage::BitVector newRelevantStates(transitionMatrix.get().getRowCount()); for (uint64_t i = 0; i < this->beforeStates.getNumberOfSetBits(); ++i) { newRelevantStates.set(i); @@ -724,95 +850,104 @@ storm::storage::BitVector SparseDtmcPrctlHelper::Bai return newRelevantStates; } -template -storm::storage::BitVector SparseDtmcPrctlHelper::BaierTransformedModel::getNewRelevantStates( +template +storm::storage::BitVector SparseDtmcPrctlHelper::BaierTransformedModel::getNewRelevantStates( storm::storage::BitVector const& oldRelevantStates) const { storm::storage::BitVector result = oldRelevantStates % this->beforeStates; result.resize(transitionMatrix.get().getRowCount()); return result; } -template -std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative) { - // Prepare result vector. - std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); - - if (!conditionStates.empty()) { - BaierTransformedModel transformedModel = - computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, boost::none); - - if (transformedModel.noTargetStates) { - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); - } else { - // At this point, we do not need to check whether there are 'before' states, since the condition - // states were non-empty so there is at least one state with a positive probability of satisfying - // the condition. - - // Now compute reachability probabilities in the transformed model. - storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); - storm::storage::BitVector newRelevantValues; - if (goal.hasRelevantValues()) { - newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing conditional probabilities with interval models."); + } else { + // Prepare result vector. + std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); + + if (!conditionStates.empty()) { + BaierTransformedModel transformedModel = + computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, boost::none); + + if (transformedModel.noTargetStates) { + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); } else { - newRelevantValues = transformedModel.getNewRelevantStates(); - } - goal.setRelevantValues(std::move(newRelevantValues)); - std::vector conditionalProbabilities = - computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), - storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative); + // At this point, we do not need to check whether there are 'before' states, since the condition + // states were non-empty so there is at least one state with a positive probability of satisfying + // the condition. + + // Now compute reachability probabilities in the transformed model. + storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + storm::storage::BitVector newRelevantValues; + if (goal.hasRelevantValues()) { + newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); + } else { + newRelevantValues = transformedModel.getNewRelevantStates(); + } + goal.setRelevantValues(std::move(newRelevantValues)); + std::vector conditionalProbabilities = computeUntilProbabilities( + env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), + storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative); - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); + } } - } - return result; + return result; + } } -template -std::vector SparseDtmcPrctlHelper::computeConditionalRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, +template +std::vector SparseDtmcPrctlHelper::computeConditionalRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative) { - // Prepare result vector. - std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); - - if (!conditionStates.empty()) { - BaierTransformedModel transformedModel = computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, - rewardModel.getTotalRewardVector(transitionMatrix)); - - if (transformedModel.noTargetStates) { - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); - } else { - // At this point, we do not need to check whether there are 'before' states, since the condition - // states were non-empty so there is at least one state with a positive probability of satisfying - // the condition. - - // Now compute reachability probabilities in the transformed model. - storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); - storm::storage::BitVector newRelevantValues; - if (goal.hasRelevantValues()) { - newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing conditional rewards with interval models."); + } else { + // Prepare result vector. + std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); + + if (!conditionStates.empty()) { + BaierTransformedModel transformedModel = computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, + rewardModel.getTotalRewardVector(transitionMatrix)); + + if (transformedModel.noTargetStates) { + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); } else { - newRelevantValues = transformedModel.getNewRelevantStates(); + // At this point, we do not need to check whether there are 'before' states, since the condition + // states were non-empty so there is at least one state with a positive probability of satisfying + // the condition. + + // Now compute reachability probabilities in the transformed model. + storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + storm::storage::BitVector newRelevantValues; + if (goal.hasRelevantValues()) { + newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); + } else { + newRelevantValues = transformedModel.getNewRelevantStates(); + } + goal.setRelevantValues(std::move(newRelevantValues)); + std::vector conditionalRewards = + computeReachabilityRewards(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), + transformedModel.targetStates.get(), qualitative); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards); } - goal.setRelevantValues(std::move(newRelevantValues)); - std::vector conditionalRewards = - computeReachabilityRewards(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), - transformedModel.targetStates.get(), qualitative); - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards); } - } - return result; + return result; + } } template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper; +template class SparseDtmcPrctlHelper, double>; } // namespace helper } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 4e4efb48f7..53be571185 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -24,88 +24,88 @@ class CheckResult; namespace helper { -template> +template, typename SolutionType = ValueType> class SparseDtmcPrctlHelper { public: - static std::map computeRewardBoundedValues( + static std::map computeRewardBoundedValues( Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula); - static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::BitVector const& nextStates); + static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::BitVector const& nextStates); - static std::vector computeUntilProbabilities(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, - bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); - - static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, - storm::storage::BitVector const& psiStates); - - static std::vector computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, + static std::vector computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& psiStates, bool qualitative); + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, + bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); - static std::vector computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, - uint_fast64_t stepBound); + static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); - static std::vector computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, + static std::vector computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& psiStates, bool qualitative); + + static std::vector computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, - RewardModelType const& rewardModel, uint_fast64_t stepCount); + RewardModelType const& rewardModel, uint_fast64_t stepBound); - static std::vector computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, - bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + RewardModelType const& rewardModel, uint_fast64_t stepCount); - static std::vector computeDiscountedCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - RewardModelType const& rewardModel, uint_fast64_t stepBound, ValueType discountFactor); + static std::vector computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, + bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::vector computeDiscountedCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + RewardModelType const& rewardModel, uint_fast64_t stepBound, ValueType discountFactor); + + static std::vector computeDiscountedTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + RewardModelType const& rewardModel, bool qualitative, ValueType discountFactor, + ModelCheckerHint const& hint = ModelCheckerHint()); - static std::vector computeDiscountedTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, + static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, - RewardModelType const& rewardModel, bool qualitative, ValueType discountFactor, + RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, + bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + std::vector const& totalStateRewardVector, + storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); - static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, - RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, - bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); - - static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, - std::vector const& totalStateRewardVector, - storm::storage::BitVector const& targetStates, bool qualitative, - ModelCheckerHint const& hint = ModelCheckerHint()); - - static std::vector computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& targetStates, bool qualitative, - ModelCheckerHint const& hint = ModelCheckerHint()); - - static std::vector computeConditionalProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& conditionStates, bool qualitative); + static std::vector computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& targetStates, bool qualitative, + ModelCheckerHint const& hint = ModelCheckerHint()); - static std::vector computeConditionalRewards(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, - RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& conditionStates, bool qualitative); + static std::vector computeConditionalProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& conditionStates, bool qualitative); + + static std::vector computeConditionalRewards(Environment const& env, storm::solver::SolveGoal&& goal, + storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& conditionStates, bool qualitative); private: - static std::vector computeReachabilityRewards( - Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, + static std::vector computeReachabilityRewards( + Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp index 275318d813..1719a04a1f 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp @@ -104,11 +104,7 @@ SparseMdpEndComponentInformation SparseMdpEndComponentInformation const* summand, storm::storage::SparseMatrix& submatrix, std::vector* 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) { - 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."); - } + // (1) Compute the number of maybe states not in ECs before any other maybe state. std::vector const& maybeStatesNotInEcBefore = result.getNumberOfMaybeStatesNotInEcBeforeIndices(); uint64_t numberOfStates = result.numberOfMaybeStatesNotInEc + result.numberOfEc; @@ -246,11 +242,6 @@ SparseMdpEndComponentInformation SparseMdpEndComponentInformation const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& 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) { - 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."); - } // (1) Compute the number of maybe states not in ECs before any other maybe state. std::vector maybeStatesNotInEcBefore = result.getNumberOfMaybeStatesNotInEcBeforeIndices(); @@ -353,8 +344,9 @@ SparseMdpEndComponentInformation SparseMdpEndComponentInformation -void SparseMdpEndComponentInformation::setValues(std::vector& result, storm::storage::BitVector const& maybeStates, - std::vector const& fromResult) { +template +void SparseMdpEndComponentInformation::setValues(std::vector& result, storm::storage::BitVector const& maybeStates, + std::vector const& fromResult) { // The following assumes that row groups associated to EC states are at the very end. auto notInEcResultIt = fromResult.begin(); for (auto state : maybeStates) { @@ -422,24 +414,29 @@ template class SparseMdpEndComponentInformation; template class SparseMdpEndComponentInformation; template class SparseMdpEndComponentInformation; +template void SparseMdpEndComponentInformation::setValues(std::vector& result, storm::storage::BitVector const& maybeStates, + std::vector const& fromResult); +template void SparseMdpEndComponentInformation::setValues(std::vector& result, + storm::storage::BitVector const& maybeStates, + std::vector const& fromResult); +template void SparseMdpEndComponentInformation::setValues(std::vector>& result, + storm::storage::BitVector const& maybeStates, + 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 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 void SparseMdpEndComponentInformation::setScheduler(storm::storage::Scheduler& scheduler, +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 } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h index 7c9b78b852..743c54784d 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h @@ -66,7 +66,8 @@ class SparseMdpEndComponentInformation { storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector, bool gatherExitChoices = false); - void setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult); + template + void setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult); template void setScheduler(storm::storage::Scheduler& scheduler, storm::storage::BitVector const& maybeStates, diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index eb620738f3..0a3b57f5d6 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; @@ -133,7 +133,7 @@ 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) { + if constexpr (storm::IsIntervalType) { 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. @@ -342,6 +342,15 @@ SparseMdpHintType computeHints(Environment const& env, SemanticSol // e.g., end components in which infinite reward is collected. result.uniqueSolution = result.hasNoEndComponents(); + if (storm::IsIntervalType && !result.uniqueSolution && type == SemanticSolutionType::ExpectedRewards) { + // For interval models, we currently cannot compute upper reward bounds. + // We therefore trigger end component elimination which guarantees a unique solution and (at least for robust value iteration) removes the need for + // upper bounds. + STORM_LOG_DEBUG("Scheduling EC elimination for interval models."); + result.uniqueSolution = true; + result.eliminateEndComponents = true; + } + // Check for requirements of the solver. bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint(); storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; @@ -449,7 +458,7 @@ MaybeStateResult computeValuesForMaybeStates(Environment const& en std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); solver->setRequirementsChecked(); - solver->setUncertaintyIsRobust(goal.isRobust()); + solver->setUncertaintyResolutionMode(goal.getUncertaintyResolutionMode()); solver->setHasUniqueSolution(hint.hasUniqueSolution()); solver->setHasNoEndComponents(hint.hasNoEndComponents()); if (hint.hasLowerResultBound()) { @@ -612,7 +621,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. @@ -634,9 +643,9 @@ void computeFixedPointSystemUntilProbabilities(storm::solver::SolveGoal @@ -660,16 +669,28 @@ boost::optional> computeFixedPointSy // Only do more work if there are actually end-components. if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s)."); - SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents( - endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, - submatrix, &b, nullptr, produceScheduler); - + std::optional> result; + if constexpr (storm::IsIntervalType) { + // We keep the non-maybe states but erase all transition entries in their rows. + storm::storage::BitVector allStates(transitionMatrix.getRowGroupCount(), true); + auto maybeChoices = transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates); + auto filteredMatrix = transitionMatrix.filterEntries(maybeChoices); + std::vector prob1ChoiceVector(transitionMatrix.getRowCount(), storm::utility::zero()); + storm::utility::vector::setVectorValues(prob1ChoiceVector, transitionMatrix.getRowFilter(qualitativeStateSets.statesWithProbability1), + storm::utility::one()); + result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, filteredMatrix, allStates, nullptr, nullptr, + &prob1ChoiceVector, submatrix, nullptr, &b, produceScheduler); + } else { + result = SparseMdpEndComponentInformation::eliminateEndComponents( + endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, + submatrix, &b, nullptr, produceScheduler); + } // If the solve goal has relevant values, we need to adjust them. if (goal.hasRelevantValues()) { storm::storage::BitVector newRelevantValues(submatrix.getRowGroupCount()); for (auto state : goal.relevantValues()) { - if (qualitativeStateSets.maybeStates.get(state)) { - newRelevantValues.set(result.getRowGroupAfterElimination(state)); + if (storm::IsIntervalType || qualitativeStateSets.maybeStates.get(state)) { + newRelevantValues.set(result->getRowGroupAfterElimination(state)); } } if (!newRelevantValues.empty()) { @@ -677,7 +698,7 @@ boost::optional> computeFixedPointSy } } - return result; + return *result; } else { STORM_LOG_DEBUG("Not eliminating ECs as there are none."); computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b); @@ -697,6 +718,13 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + if constexpr (storm::IsIntervalType) { + // We currently assume that qualitative state sets and end components can be computed as for regular MDPs. + // That means we shall not have intervals of the form [0,x] for x>0. + STORM_LOG_THROW(transitionMatrix.hasOnlyPositiveEntries(), storm::exceptions::NotSupportedException, + "Computing until probabilities on uncertain model requires graph-preservation."); + } + // We need to identify the maybe states (states which have a probability for satisfying the until formula // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1 and 0, respectively. QualitativeStateSetsUntilProbabilities qualitativeStateSets = @@ -757,18 +785,22 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support this end component with interval models."); - } else { + if constexpr (!storm::IsIntervalType) { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); if (produceScheduler) { ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler()); } + } else { + storm::storage::BitVector allStates(transitionMatrix.getRowGroupCount(), true); + ecInformation.get().setValues(result, allStates, resultForMaybeStates.getValues()); + if (produceScheduler) { + ecInformation.get().setScheduler(*scheduler, allStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler()); + } } } else { // Set values of resulting vector according to result. - if constexpr (!std::is_same_v) { + 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 +809,8 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper>(*scheduler, resultForMaybeStates.getScheduler(), - qualitativeStateSets.maybeStates); + extractSchedulerChoices>(*scheduler, resultForMaybeStates.getScheduler(), + qualitativeStateSets.maybeStates); } } } @@ -833,7 +865,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(). @@ -854,7 +886,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(). @@ -1188,29 +1220,42 @@ void extendScheduler(storm::storage::Scheduler& scheduler, storm:: } } -template +template void extractSchedulerChoices(storm::storage::Scheduler& scheduler, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& subChoices, storm::storage::BitVector const& maybeStates, boost::optional const& selectedChoices) { - auto subChoiceIt = subChoices.begin(); + uint64_t choicesIndex = 0; + if (subChoicesCoverOnlyMaybeStates) { + STORM_LOG_ASSERT(subChoices.size() == maybeStates.getNumberOfSetBits(), "Unexpected size of choices."); + } else { + STORM_LOG_ASSERT(subChoices.size() == maybeStates.size(), "Unexpected size of choices."); + choicesIndex = maybeStates.getNextSetIndex(choicesIndex); + } + auto incrementChoicesIndex = [&choicesIndex, &maybeStates]() { + ++choicesIndex; + if (!subChoicesCoverOnlyMaybeStates) { + choicesIndex = maybeStates.getNextSetIndex(choicesIndex); + } + }; + if (selectedChoices) { for (auto maybeState : maybeStates) { // find the rowindex that corresponds to the selected row of the submodel uint_fast64_t firstRowIndex = transitionMatrix.getRowGroupIndices()[maybeState]; uint_fast64_t selectedRowIndex = selectedChoices->getNextSetIndex(firstRowIndex); - for (uint_fast64_t choice = 0; choice < *subChoiceIt; ++choice) { + for (uint_fast64_t choice = 0; choice < subChoices[choicesIndex]; ++choice) { selectedRowIndex = selectedChoices->getNextSetIndex(selectedRowIndex + 1); } scheduler.setChoice(selectedRowIndex - firstRowIndex, maybeState); - ++subChoiceIt; + incrementChoicesIndex(); } } else { for (auto maybeState : maybeStates) { - scheduler.setChoice(*subChoiceIt, maybeState); - ++subChoiceIt; + scheduler.setChoice(subChoices[choicesIndex], maybeState); + incrementChoicesIndex(); } } - assert(subChoiceIt == subChoices.end()); + assert(choicesIndex == subChoices.size()); } template @@ -1220,27 +1265,45 @@ void computeFixedPointSystemReachabilityRewards( std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix& submatrix, std::vector& b, std::vector* oneStepTargetProbabilities = nullptr) { - // Remove rows and columns from the original transition probability matrix for states whose reward values are already known. - // If there are infinity states, we additionally have to remove choices of maybeState that lead to infinity. - if (qualitativeStateSets.infinityStates.empty()) { - submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false); - b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, qualitativeStateSets.maybeStates); + if (storm::IsIntervalType) { + // For interval-based models, we can not merge transitions to non-maybe states since we need to keep track of the possible interval instantiations. + // This is similar to the until probabilities case and can also be optimized. + // Here, we clear all entries in rows of non-maybe states + auto maybeChoices = transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates); + submatrix = transitionMatrix.filterEntries(maybeChoices); + b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); + storm::utility::vector::setVectorValues(b, ~maybeChoices, storm::utility::zero()); + if (!qualitativeStateSets.infinityStates.empty()) { + // Cut away choices that lead to infinity states. + submatrix = submatrix.restrictRows(*selectedChoices); + storm::utility::vector::filterVectorInPlace(b, *selectedChoices); + } if (oneStepTargetProbabilities) { - (*oneStepTargetProbabilities) = - transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.rewardZeroStates); + oneStepTargetProbabilities->assign(b.size(), storm::utility::zero()); } } else { - submatrix = transitionMatrix.getSubmatrix(false, *selectedChoices, qualitativeStateSets.maybeStates, false); - b = totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix, - storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); - storm::utility::vector::filterVectorInPlace(b, *selectedChoices); - if (oneStepTargetProbabilities) { - (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowSumVector(*selectedChoices, qualitativeStateSets.rewardZeroStates); + // Remove rows and columns from the original transition probability matrix for states whose reward values are already known. + // If there are infinity states, we additionally have to remove choices of maybeState that lead to infinity. + if (qualitativeStateSets.infinityStates.empty()) { + submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false); + b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, qualitativeStateSets.maybeStates); + if (oneStepTargetProbabilities) { + (*oneStepTargetProbabilities) = + transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.rewardZeroStates); + } + } else { + submatrix = transitionMatrix.getSubmatrix(false, *selectedChoices, qualitativeStateSets.maybeStates, false); + b = totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix, + storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); + storm::utility::vector::filterVectorInPlace(b, *selectedChoices); + if (oneStepTargetProbabilities) { + (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowSumVector(*selectedChoices, qualitativeStateSets.rewardZeroStates); + } } - } - // If the solve goal has relevant values, we need to adjust them. - goal.restrictRelevantValues(qualitativeStateSets.maybeStates); + // If the solve goal has relevant values, we need to adjust them. + goal.restrictRelevantValues(qualitativeStateSets.maybeStates); + } } template @@ -1301,17 +1364,31 @@ boost::optional> computeFixedPointSy // Only do more work if there are actually end-components. if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs."); - SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents( - endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, - oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, - submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b, produceScheduler); - + std::optional> result; + if (storm::IsIntervalType) { + // We keep the non-maybe states but erase all transition entries in their rows. + storm::storage::BitVector allStates(transitionMatrix.getRowGroupCount(), true); + auto maybeChoices = transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates); + auto filteredMatrix = transitionMatrix.filterEntries(maybeChoices); + storm::utility::vector::setVectorValues(rewardVector, ~maybeChoices, storm::utility::zero()); + result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, filteredMatrix, allStates, nullptr, + selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, + submatrix, nullptr, &b, produceScheduler); + if (oneStepTargetProbabilities) { + oneStepTargetProbabilities->assign(b.size(), storm::utility::zero()); + } + } else { + result = SparseMdpEndComponentInformation::eliminateEndComponents( + endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, + oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, + &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b, produceScheduler); + } // If the solve goal has relevant values, we need to adjust them. if (goal.hasRelevantValues()) { storm::storage::BitVector newRelevantValues(submatrix.getRowGroupCount()); for (auto state : goal.relevantValues()) { - if (qualitativeStateSets.maybeStates.get(state)) { - newRelevantValues.set(result.getRowGroupAfterElimination(state)); + if (storm::IsIntervalType || qualitativeStateSets.maybeStates.get(state)) { + newRelevantValues.set(result->getRowGroupAfterElimination(state)); } } if (!newRelevantValues.empty()) { @@ -1319,7 +1396,7 @@ boost::optional> computeFixedPointSy } } - return result; + return *result; } else { STORM_LOG_DEBUG("Not eliminating ECs as there are none."); computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, @@ -1332,7 +1409,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). @@ -1358,6 +1435,13 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + if constexpr (storm::IsIntervalType) { + // We currently assume that reward infinity and end components can be computed as for regular MDPs. + // That means we shall not have intervals of the form [0,x] for x>0. + STORM_LOG_THROW(transitionMatrix.hasOnlyPositiveEntries(), storm::exceptions::NotSupportedException, + "Computing until probabilities on uncertain model requires graph-preservation."); + } + // Determine which states have a reward that is infinity or less than infinity. QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards( goal, transitionMatrix, backwardTransitions, targetStates, hint, zeroRewardStatesGetter, zeroRewardChoicesGetter); @@ -1366,16 +1450,10 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper()); - // If requested, we will produce a scheduler. std::unique_ptr> scheduler; if (produceScheduler) { - if constexpr (std::is_same_v) { - 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()); - } + scheduler = std::make_unique>(transitionMatrix.getRowGroupCount()); } // Check if the values of the maybe states are relevant for the SolveGoal @@ -1395,6 +1473,10 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper selectedChoices; if (!qualitativeStateSets.infinityStates.empty()) { selectedChoices = transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates, ~qualitativeStateSets.infinityStates); + if (storm::IsIntervalType) { + // For interval models, we keep non-maybe states inside the equation system. Thus, we also select their choices here. + *selectedChoices |= transitionMatrix.getRowFilter(~qualitativeStateSets.maybeStates); + } } // Obtain proper hint information either from the provided hint or from requirements of the solver. @@ -1416,13 +1498,13 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper> ecInformation; if (hintInformation.getEliminateEndComponents()) { - if constexpr (std::is_same_v) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models."); - } else { - ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents( - goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, - oneStepTargetProbabilities, produceScheduler); + if constexpr (storm::IsIntervalType) { + STORM_LOG_ASSERT(transitionMatrix.hasOnlyPositiveEntries(), + "We do not support eliminating end components with non-graph-preserving interval models."); } + ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents( + goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, + oneStepTargetProbabilities, produceScheduler); } else { // Otherwise, we compute the standard equations. computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, @@ -1441,8 +1523,16 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models."); + if (storm::IsIntervalType) { + // For interval models, the result contains a value for all states. + storm::storage::BitVector allStates(transitionMatrix.getRowGroupCount(), true); + // The following also sets the results for non-maybe states. + // In particular, it sets value 0 for infinity states. + // Actually setting the value to infinity therefore must happen afterwards. + ecInformation.get().setValues(result, allStates, resultForMaybeStates.getValues()); + if (produceScheduler) { + ecInformation.get().setScheduler(*scheduler, allStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler()); + } } else { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); if (produceScheduler) { @@ -1451,16 +1541,27 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + if (storm::IsIntervalType) { + // For interval models, the result for maybe states indeed also holds values for all qualitative states. + STORM_LOG_ASSERT(resultForMaybeStates.getValues().size() == transitionMatrix.getColumnCount(), "Dimensions do not match"); + for (auto state : qualitativeStateSets.maybeStates) { + result[state] = resultForMaybeStates.getValues()[state]; + } + } else { + // Set values of resulting vector according to result. + storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + } if (produceScheduler) { - extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, - selectedChoices); + extractSchedulerChoices>( + *scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, selectedChoices); } } } } + // Set value for infinity states. + storm::utility::vector::setVectorValues(result, qualitativeStateSets.infinityStates, storm::utility::infinity()); + // Extend scheduler with choices for the states in the qualitative state sets. if (produceScheduler) { extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter); @@ -1472,11 +1573,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelperisDeterministicScheduler(), "Expected a deterministic scheduler"); STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); - if constexpr (std::is_same_v) { - return MDPSparseModelCheckingHelperReturnType(std::move(result)); - } else { - return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); - } + return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } template class SparseMdpPrctlHelper; diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 196d0db8df..10428e033e 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -81,5 +81,6 @@ template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; +template class SparsePropositionalModelChecker>; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index f372611c84..b0512229c6 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -37,7 +37,7 @@ SparseDtmcEliminationModelChecker::SparseDtmcEliminationMod } template -bool SparseDtmcEliminationModelChecker::canHandle(CheckTask const& checkTask) const { +bool SparseDtmcEliminationModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::prctl().setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); fragment.setNestedOperatorsAllowed(false) @@ -49,7 +49,7 @@ bool SparseDtmcEliminationModelChecker::canHandle(CheckTask template std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -116,7 +116,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); @@ -180,7 +180,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker -std::vector::ValueType> +std::vector::SolutionType> SparseDtmcEliminationModelChecker::computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, @@ -337,7 +337,7 @@ SparseDtmcEliminationModelChecker::computeLongRunValues(sto template std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, @@ -448,7 +448,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. @@ -529,7 +529,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. @@ -637,7 +637,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities( - Environment const& env, CheckTask const& checkTask) { + Environment const& env, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 8446fabb86..f02feee29b 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -27,6 +27,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; /*! * Creates an elimination-based model checker for the given model. @@ -36,19 +37,19 @@ class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; + virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards( - Environment const& env, CheckTask const& checkTask) override; + Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, - CheckTask const& checkTask) override; + CheckTask const& checkTask) override; // Static helper methods static std::unique_ptr computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, @@ -63,10 +64,10 @@ class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker bool computeForInitialStatesOnly); private: - static std::vector computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, - bool computeResultsForInitialStatesOnly, std::vector& stateValues); + static std::vector computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, + storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, + bool computeResultsForInitialStatesOnly, std::vector& stateValues); static std::unique_ptr computeReachabilityRewards( storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index b7b7c61d63..cd88376677 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -416,7 +416,7 @@ std::size_t Model::hash() const { template void Model::printModelInformationHeaderToStream(std::ostream& out) const { out << "-------------------------------------------------------------- \n"; - out << "Model type: \t" << this->getType() << " (sparse)\n"; + out << "Model type: \t" << (storm::IsIntervalType ? "I" : "") << this->getType() << " (sparse)\n"; out << "States: \t" << this->getNumberOfStates() << '\n'; out << "Transitions: \t" << this->getNumberOfTransitions() << '\n'; } diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index f1f8fbafc4..bdcdf92ecd 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -297,7 +297,7 @@ template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const { - std::vector result(numberOfRows); + std::vector result(numberOfRows, storm::utility::zero()); if (this->hasTransitionRewards()) { std::vector pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); storm::utility::vector::selectVectorValues(result, filter, transitionMatrix.getRowGroupIndices(), pointwiseProductRowSumVector); diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index c2d0b1d46e..460208fe31 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -3,6 +3,7 @@ #include #include "storm/adapters/AddExpressionAdapter.h" +#include "storm/adapters/IntervalForward.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/InvalidOperationException.h" @@ -317,7 +318,7 @@ std::vector Model::getLabels() const { template void Model::printModelInformationHeaderToStream(std::ostream& out) const { out << "-------------------------------------------------------------- \n"; - out << "Model type: \t" << this->getType() << " (symbolic)\n"; + out << "Model type: \t" << (storm::IsIntervalType ? "I" : "") << this->getType() << " (symbolic)\n"; out << "States: \t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)\n"; out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)\n"; } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 48d4ab06ae..fb03518106 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -55,6 +55,8 @@ const std::string IOSettings::qvbsInputOptionShortName = "qvbs"; const std::string IOSettings::qvbsRootOptionName = "qvbsroot"; const std::string IOSettings::propertiesAsMultiOptionName = "propsasmulti"; +const std::string IOSettings::uncertaintyResolutionModeName = "uncertainty-resolution"; + std::string preventDRNPlaceholderOptionName = "no-drn-placeholders"; IOSettings::IOSettings() : ModuleSettings(moduleName) { @@ -255,6 +257,13 @@ IOSettings::IOSettings() : ModuleSettings(moduleName) { .setIsAdvanced() .build()); + std::vector uncertaintyResolutionModes = {"minimize", "maximize", "robust", "cooperative", "min", "max"}; + this->addOption(storm::settings::OptionBuilder(moduleName, uncertaintyResolutionModeName, false, "Mode to resolve the uncertainty (intervals)") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "Mode to resolve the uncertainty (intervals) by nature.") + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(uncertaintyResolutionModes)) + .build()) + .build()); + #ifdef STORM_HAVE_QVBS std::string qvbsRootDefault = STORM_QVBS_ROOT; #else @@ -520,6 +529,28 @@ bool IOSettings::isPropertiesAsMultiSet() const { return this->getOption(propertiesAsMultiOptionName).getHasOptionBeenSet(); } +UncertaintyResolutionModeSetting IOSettings::getUncertaintyResolutionMode() const { + std::string uncertaintyResolutionModeString = this->getOption(uncertaintyResolutionModeName).getArgumentByName("mode").getValueAsString(); + + if (uncertaintyResolutionModeString == "minimize" || uncertaintyResolutionModeString == "min") { + return UncertaintyResolutionModeSetting::Minimize; + } else if (uncertaintyResolutionModeString == "maximize" || uncertaintyResolutionModeString == "max") { + return UncertaintyResolutionModeSetting::Maximize; + } else if (uncertaintyResolutionModeString == "robust") { + return UncertaintyResolutionModeSetting::Robust; + } else if (uncertaintyResolutionModeString == "cooperative") { + return UncertaintyResolutionModeSetting::Cooperative; + } else if (uncertaintyResolutionModeString == "both") { + STORM_LOG_ERROR("Uncertainty resolution mode 'both' not yet supported."); + return UncertaintyResolutionModeSetting::Both; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown nature resolution mode '" << uncertaintyResolutionModeString << "'."); +} + +bool IOSettings::isUncertaintyResolutionModeSet() const { + return this->getOption(uncertaintyResolutionModeName).getHasOptionBeenSet(); +} + void IOSettings::finalize() { STORM_LOG_WARN_COND(!isExportDdSet(), "Option '--" << moduleName << ":" << exportDdOptionName << "' is depreciated. Use '--" << moduleName << ":" << exportBuildOptionName << "' instead."); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 93bfe56f08..57008f464c 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -8,6 +8,7 @@ #include "storm/io/ModelExportFormat.h" #include "storm/modelchecker/helper/infinitehorizon/SteadyStateDistributionAlgorithm.h" #include "storm/settings/modules/ModuleSettings.h" +#include "storm/solver/UncertaintyResolutionMode.h" namespace storm { namespace settings { @@ -374,6 +375,18 @@ class IOSettings : public ModuleSettings { */ bool isPropertiesAsMultiSet() const; + /*! + * Retrieves the mode deciding how the uncertainty should be resolved. + * + * @return The nature resolution mode + */ + UncertaintyResolutionModeSetting getUncertaintyResolutionMode() const; + + /*! + * @return whether the mode for how the uncertainty should be resolved has been set. + */ + bool isUncertaintyResolutionModeSet() const; + bool check() const override; void finalize() override; @@ -416,6 +429,7 @@ class IOSettings : public ModuleSettings { static const std::string qvbsInputOptionShortName; static const std::string qvbsRootOptionName; static const std::string propertiesAsMultiOptionName; + static const std::string uncertaintyResolutionModeName; }; } // namespace modules diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index ca1e92555c..3fe6aa749d 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -78,6 +78,13 @@ MinMaxMethod IterativeMinMaxLinearEquationSolver::getMe STORM_LOG_WARN("The selected solution method does not guarantee sound results."); } } + + // Default to robust value iteration in case of interval models. + if (storm::IsIntervalType && method != MinMaxMethod::ValueIteration) { + STORM_LOG_WARN("Selected method is not supported for this solver and interval models, switching to robust value iteration."); + method = MinMaxMethod::ValueIteration; + } + STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::OptimisticValueIteration || method == MinMaxMethod::GuessingValueIteration || method == MinMaxMethod::ViToPi, @@ -159,7 +166,8 @@ void IterativeMinMaxLinearEquationSolver::setUpViOperat template void IterativeMinMaxLinearEquationSolver::extractScheduler(std::vector& x, std::vector const& b, - OptimizationDirection const& dir, bool updateX, bool robust) const { + OptimizationDirection const& dir, + UncertaintyResolutionMode uncertaintyResolutionMode, bool updateX) const { if (std::is_same_v && this->A->hasTrivialRowGrouping()) { // Create robust scheduler index if it doesn't exist yet if (!this->robustSchedulerIndex) { @@ -195,14 +203,14 @@ void IterativeMinMaxLinearEquationSolver::extractSchedu if (viOperatorTriv) { if constexpr (std::is_same() && std::is_same()) { storm::solver::helper::SchedulerTrackingHelper schedHelper(viOperatorTriv); - schedHelper.computeScheduler(x, b, dir, *this->schedulerChoices, robust, updateX ? &x : nullptr, this->robustSchedulerIndex); + schedHelper.computeScheduler(x, b, dir, *this->schedulerChoices, uncertaintyResolutionMode, updateX ? &x : nullptr, this->robustSchedulerIndex); } else { STORM_LOG_ERROR("SchedulerTrackingHelper not implemented for this setting (trivial row grouping but not Interval->double)."); } } if (viOperatorNontriv) { storm::solver::helper::SchedulerTrackingHelper schedHelper(viOperatorNontriv); - schedHelper.computeScheduler(x, b, dir, *this->schedulerChoices, robust, updateX ? &x : nullptr, this->robustSchedulerIndex); + schedHelper.computeScheduler(x, b, dir, *this->schedulerChoices, uncertaintyResolutionMode, updateX ? &x : nullptr, this->robustSchedulerIndex); } } @@ -594,7 +602,7 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir, this->isUncertaintyRobust()); + this->extractScheduler(x, b, dir, this->getUncertaintyResolutionMode()); } if (!this->isCachingEnabled()) { @@ -643,7 +651,7 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir, this->isUncertaintyRobust()); + this->extractScheduler(x, b, dir, this->getUncertaintyResolutionMode()); } if (!this->isCachingEnabled()) { @@ -727,12 +735,12 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation auto status = viHelper.VI(x, b, numIterations, env.solver().minMax().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().minMax().getPrecision()), dir, viCallback, - env.solver().minMax().getMultiplicationStyle(), this->isUncertaintyRobust()); + env.solver().minMax().getMultiplicationStyle(), this->getUncertaintyResolutionMode()); this->reportStatus(status, numIterations); // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir, this->isUncertaintyRobust()); + this->extractScheduler(x, b, dir, this->getUncertaintyResolutionMode()); } if (!this->isCachingEnabled()) { @@ -745,12 +753,12 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation auto status = viHelper.VI(x, b, numIterations, env.solver().minMax().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().minMax().getPrecision()), dir, viCallback, - env.solver().minMax().getMultiplicationStyle(), this->isUncertaintyRobust()); + env.solver().minMax().getMultiplicationStyle(), this->getUncertaintyResolutionMode()); this->reportStatus(status, numIterations); // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir, this->isUncertaintyRobust()); + this->extractScheduler(x, b, dir, this->getUncertaintyResolutionMode()); } if (!this->isCachingEnabled()) { @@ -804,7 +812,7 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir, this->isUncertaintyRobust()); + this->extractScheduler(x, b, dir, this->getUncertaintyResolutionMode()); } if (!this->isCachingEnabled()) { @@ -855,7 +863,7 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir, this->isUncertaintyRobust()); + this->extractScheduler(x, b, dir, this->getUncertaintyResolutionMode()); } this->reportStatus(status, numIterations); @@ -952,7 +960,7 @@ bool IterativeMinMaxLinearEquationSolver::solveEquation // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->extractScheduler(x, b, dir, this->isUncertaintyRobust()); + this->extractScheduler(x, b, dir, this->getUncertaintyResolutionMode()); } if (!this->isCachingEnabled()) { diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index 46b57618e9..f207c7b187 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -62,8 +62,8 @@ class IterativeMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationS bool solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; void setUpViOperator() const; - void extractScheduler(std::vector& x, std::vector const& b, OptimizationDirection const& dir, bool robust, - bool updateX = true) const; + void extractScheduler(std::vector& x, std::vector const& b, OptimizationDirection const& dir, + UncertaintyResolutionMode uncertaintyResolutionMode, bool updateX = true) const; /// The factory used to obtain linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 3a42ae9af3..81242b0296 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -19,7 +19,13 @@ namespace storm::solver { template MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) - : direction(direction), trackScheduler(false), uniqueSolution(false), noEndComponents(false), cachingEnabled(false), requirementsChecked(false) { + : direction(direction), + trackScheduler(false), + uniqueSolution(false), + noEndComponents(false), + cachingEnabled(false), + requirementsChecked(false), + uncertaintyResolutionMode(UncertaintyResolutionMode::Unset) { // Intentionally left empty. } @@ -41,6 +47,8 @@ template void MinMaxLinearEquationSolver::solveEquations(Environment const& env, std::vector& x, std::vector const& b) const { STORM_LOG_THROW(isSet(this->direction), storm::exceptions::IllegalFunctionCallException, "Optimization direction not set."); + STORM_LOG_THROW(isSet(this->uncertaintyResolutionMode) || !storm::IsIntervalType, storm::exceptions::IllegalFunctionCallException, + "Uncertainty resolution mode not set."); solveEquations(env, convert(this->direction), x, b); } @@ -189,13 +197,13 @@ bool MinMaxLinearEquationSolverFactory::isRequirementsC } template -void MinMaxLinearEquationSolver::setUncertaintyIsRobust(bool robust) { - this->robustUncertainty = robust; +void MinMaxLinearEquationSolver::setUncertaintyResolutionMode(storm::solver::UncertaintyResolutionMode uncertaintyResolutionMode) { + this->uncertaintyResolutionMode = uncertaintyResolutionMode; } template -bool MinMaxLinearEquationSolver::isUncertaintyRobust() const { - return this->robustUncertainty; +UncertaintyResolutionMode MinMaxLinearEquationSolver::getUncertaintyResolutionMode() const { + return this->uncertaintyResolutionMode; } template @@ -237,7 +245,7 @@ std::unique_ptr> GeneralMinM Environment const& env) const { std::unique_ptr> result; // TODO some minmax linear equation solvers only support SolutionType == ValueType. - auto method = env.solver().minMax().getMethod(); + auto method = GeneralMinMaxLinearEquationSolverFactory::getMethod(env); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::OptimisticValueIteration || method == MinMaxMethod::GuessingValueIteration || method == MinMaxMethod::ViToPi) { @@ -272,7 +280,7 @@ template<> std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::create( Environment const& env) const { std::unique_ptr> result; - auto method = env.solver().minMax().getMethod(); + auto method = getMethod(env); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::OptimisticValueIteration || method == MinMaxMethod::GuessingValueIteration || method == MinMaxMethod::ViToPi) { @@ -291,6 +299,17 @@ std::unique_ptr> GeneralMinMax return result; } +template +MinMaxMethod GeneralMinMaxLinearEquationSolverFactory::getMethod(storm::Environment env) const { + // Default to robust value iteration in case of interval models. + auto method = env.solver().minMax().getMethod(); + if (storm::IsIntervalType && method != MinMaxMethod::ValueIteration) { + STORM_LOG_WARN("Selected method is not supported for this solver and interval models, switching to robust value iteration."); + method = MinMaxMethod::ValueIteration; + } + return method; +} + template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolverFactory; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 252889c1cc..ccb32227c9 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -10,6 +10,7 @@ #include "storm/solver/MinMaxLinearEquationSolverRequirements.h" #include "storm/solver/OptimizationDirection.h" #include "storm/solver/SolverSelectionOptions.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/storage/sparse/StateType.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -72,14 +73,14 @@ class MinMaxLinearEquationSolver : public AbstractEquationSolver { void unsetOptimizationDirection(); /*! - * Set whether uncertainty should be interpreted adverserially (robust) or not + * Sets how the uncertainty should be resolved. */ - void setUncertaintyIsRobust(bool robust); + void setUncertaintyResolutionMode(UncertaintyResolutionMode uncertaintyResolutionMode); /*! - * Is the uncertainty to be interpreted robustly (adverserially) or not? + * Retrieves the mode indicating how the uncertainty should be resolved. */ - bool isUncertaintyRobust() const; + UncertaintyResolutionMode getUncertaintyResolutionMode() const; /*! * Sets the states for which the choices are fixed. @@ -235,8 +236,8 @@ class MinMaxLinearEquationSolver : public AbstractEquationSolver { /// A flag storing whether the requirements of the solver were checked. bool requirementsChecked; - /// For uncertain models, if this flag is set to true, the uncertainty is resolved adverserially and angelically otherwise. - bool robustUncertainty; + /// For uncertain models, this mode decides how the uncertainty will be resolved by nature. + UncertaintyResolutionMode uncertaintyResolutionMode; }; template @@ -273,6 +274,9 @@ class GeneralMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolv using MinMaxLinearEquationSolverFactory::create; virtual std::unique_ptr> create(Environment const& env) const override; + + protected: + MinMaxMethod getMethod(Environment env) const; }; } // namespace solver diff --git a/src/storm/solver/SolveGoal.cpp b/src/storm/solver/SolveGoal.cpp index 1f23b34f3f..c42b8a9d8a 100644 --- a/src/storm/solver/SolveGoal.cpp +++ b/src/storm/solver/SolveGoal.cpp @@ -3,6 +3,7 @@ #include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" +#include "storm/exceptions/InvalidPropertyException.h" #include "storm/modelchecker/CheckTask.h" #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" @@ -86,6 +87,7 @@ bool SolveGoal::minimize() const { template OptimizationDirection SolveGoal::direction() const { + STORM_LOG_THROW(optimizationDirection.has_value(), storm::exceptions::InvalidPropertyException, "Optimization direction not set."); return optimizationDirection.get(); } @@ -105,8 +107,8 @@ bool SolveGoal::boundIsStrict() const { } template -bool SolveGoal::isRobust() const { - return robustAgainstUncertainty; +UncertaintyResolutionMode SolveGoal::getUncertaintyResolutionMode() const { + return uncertaintyResolutionMode; } template diff --git a/src/storm/solver/SolveGoal.h b/src/storm/solver/SolveGoal.h index f5f672f8e1..79072a38ea 100644 --- a/src/storm/solver/SolveGoal.h +++ b/src/storm/solver/SolveGoal.h @@ -6,6 +6,7 @@ #include "storm/logic/ComparisonType.h" #include "storm/solver/OptimizationDirection.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/storage/BitVector.h" #include "storm/solver/LinearEquationSolver.h" @@ -56,7 +57,7 @@ class SolveGoal { comparisonType = checkTask.getBoundComparisonType(); threshold = checkTask.getBoundThreshold(); } - robustAgainstUncertainty = checkTask.getRobustUncertainty(); + uncertaintyResolutionMode = checkTask.getUncertaintyResolutionMode(); } SolveGoal(bool minimize); @@ -76,7 +77,7 @@ class SolveGoal { OptimizationDirection direction() const; - bool isRobust() const; + UncertaintyResolutionMode getUncertaintyResolutionMode() const; bool isBounded() const; @@ -100,15 +101,16 @@ class SolveGoal { boost::optional comparisonType; boost::optional threshold; boost::optional relevantValueVector; - bool robustAgainstUncertainty = true; // If set to false, the uncertainty is interpreted as controllable. + UncertaintyResolutionMode uncertaintyResolutionMode; }; template std::unique_ptr> configureMinMaxLinearEquationSolver( Environment const& env, SolveGoal&& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, - MatrixType&& matrix) { + MatrixType&& matrix, OptimizationDirectionSetting optimizationDirectionSetting = OptimizationDirectionSetting::Unset) { std::unique_ptr> solver = factory.create(env, std::forward(matrix)); - solver->setOptimizationDirection(goal.direction()); + solver->setOptimizationDirection((optimizationDirectionSetting == OptimizationDirectionSetting::Unset) ? goal.direction() + : convert(optimizationDirectionSetting)); if (goal.isBounded()) { if (goal.boundIsALowerBound()) { solver->setTerminationCondition(std::make_unique>( diff --git a/src/storm/solver/UncertaintyResolutionMode.cpp b/src/storm/solver/UncertaintyResolutionMode.cpp new file mode 100644 index 0000000000..32e2a2a759 --- /dev/null +++ b/src/storm/solver/UncertaintyResolutionMode.cpp @@ -0,0 +1,55 @@ +#include "UncertaintyResolutionMode.h" + +namespace storm { +namespace solver { +std::ostream& operator<<(std::ostream& out, UncertaintyResolutionMode mode) { + switch (mode) { + case UncertaintyResolutionMode::Minimize: + out << "minimize"; + break; + case UncertaintyResolutionMode::Maximize: + out << "maximize"; + break; + case UncertaintyResolutionMode::Robust: + out << "robust"; + break; + case UncertaintyResolutionMode::Cooperative: + out << "cooperative"; + break; + case UncertaintyResolutionMode::Unset: + out << "unset"; + break; + } + return out; +} + +bool isSet(UncertaintyResolutionMode uncertaintyResolutionMode) { + return uncertaintyResolutionMode != UncertaintyResolutionMode::Unset; +} + +bool isUncertaintyResolvedRobust(UncertaintyResolutionMode uncertaintyResolutionMode, OptimizationDirection optimizationDirection) { + switch (uncertaintyResolutionMode) { + case UncertaintyResolutionMode::Maximize: + return optimizationDirection != OptimizationDirection::Maximize; + case UncertaintyResolutionMode::Minimize: + return optimizationDirection != OptimizationDirection::Minimize; + case UncertaintyResolutionMode::Robust: + return true; + case UncertaintyResolutionMode::Cooperative: + return false; + case UncertaintyResolutionMode::Unset: + STORM_LOG_WARN("Uncertainty resolution mode not set properly, assuming to resolve uncertainty in a robust fashion."); + break; + } + + return true; +} + +UncertaintyResolutionMode convert(UncertaintyResolutionModeSetting settingMode) { + STORM_LOG_THROW(settingMode != UncertaintyResolutionModeSetting::Both, storm::exceptions::InvalidSettingsException, + "Cannot convert uncertainty resolution setting mode 'both'"); + return static_cast(settingMode); +} + +} // namespace solver +} // namespace storm \ No newline at end of file diff --git a/src/storm/solver/UncertaintyResolutionMode.h b/src/storm/solver/UncertaintyResolutionMode.h new file mode 100644 index 0000000000..be39db10b7 --- /dev/null +++ b/src/storm/solver/UncertaintyResolutionMode.h @@ -0,0 +1,25 @@ +#pragma once + +#include +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/solver/OptimizationDirection.h" +#include "storm/utility/macros.h" + +namespace storm { +namespace solver { +// An enumeration of all resolution modes to resolve the uncertainty (e.g. intervals) by nature. +enum class UncertaintyResolutionMode { Minimize, Maximize, Robust, Cooperative, Unset }; + +// An enumeration of all resolution modes, available through the CLI, to resolve the uncertainty (e.g. intervals) by nature. +enum class UncertaintyResolutionModeSetting { Minimize, Maximize, Robust, Cooperative, Both }; + +std::ostream& operator<<(std::ostream& out, UncertaintyResolutionMode mode); +bool isSet(UncertaintyResolutionMode uncertaintyResolutionMode); +bool isUncertaintyResolvedRobust(UncertaintyResolutionMode uncertaintyResolutionMode, OptimizationDirection optimizationDirection); +UncertaintyResolutionMode convert(UncertaintyResolutionModeSetting uncertaintyResolutionModeSetting); + +} // namespace solver + +using UncertaintyResolutionModeSetting = solver::UncertaintyResolutionModeSetting; +using UncertaintyResolutionMode = solver::UncertaintyResolutionMode; +} // namespace storm diff --git a/src/storm/solver/helper/SchedulerTrackingHelper.cpp b/src/storm/solver/helper/SchedulerTrackingHelper.cpp index 73e40dae75..c8256255a6 100644 --- a/src/storm/solver/helper/SchedulerTrackingHelper.cpp +++ b/src/storm/solver/helper/SchedulerTrackingHelper.cpp @@ -103,15 +103,15 @@ bool SchedulerTrackingHelper::compu } template -bool SchedulerTrackingHelper::computeScheduler(std::vector& operandIn, - std::vector const& offsets, - storm::OptimizationDirection const& dir, - std::vector& schedulerStorage, bool robust, - std::vector* operandOut, - boost::optional> const& robustIndices) const { +bool SchedulerTrackingHelper::computeScheduler( + std::vector& operandIn, std::vector const& offsets, storm::OptimizationDirection const& dir, + std::vector& schedulerStorage, UncertaintyResolutionMode uncertaintyResolutionMode, std::vector* operandOut, + boost::optional> const& robustIndices) const { // TODO this currently assumes antagonistic intervals <-> !TrivialRowGrouping + + bool robustUncertainty = isUncertaintyResolvedRobust(uncertaintyResolutionMode, dir); if (maximize(dir)) { - if (robust && !TrivialRowGrouping) { + if (robustUncertainty && !TrivialRowGrouping) { return computeScheduler(operandIn, offsets, schedulerStorage, operandOut, robustIndices); } else { @@ -119,7 +119,7 @@ bool SchedulerTrackingHelper::compu operandOut, robustIndices); } } else { - if (robust && !TrivialRowGrouping) { + if (robustUncertainty && !TrivialRowGrouping) { return computeScheduler(operandIn, offsets, schedulerStorage, operandOut, robustIndices); } else { diff --git a/src/storm/solver/helper/SchedulerTrackingHelper.h b/src/storm/solver/helper/SchedulerTrackingHelper.h index b2f6472530..7a3ad04c37 100644 --- a/src/storm/solver/helper/SchedulerTrackingHelper.h +++ b/src/storm/solver/helper/SchedulerTrackingHelper.h @@ -3,6 +3,7 @@ #include #include "storm/solver/OptimizationDirection.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/solver/helper/ValueIterationOperatorForward.h" namespace storm::solver::helper { @@ -76,7 +77,7 @@ class SchedulerTrackingHelper { * @param offsets Offsets that are added to each choice result. * @param dir Optimization direction to consider. * @param schedulerStorage where the scheduler choices will be stored. Should have the same size as the operand(s). - * @param robust Flag whether any uncertainty should be interpreted robustly. + * @param uncertaintyResolutionMode Represents the mode indicating how the uncertainty should be resolved. * @param operandOut if given, the result values of the performed value iteration step will be stored in this vector. Can be the same as operandIn. * @return True if the scheduler coincides with the provided scheduler encoded in schedulerStorage * @@ -84,8 +85,8 @@ class SchedulerTrackingHelper { * group i */ bool computeScheduler(std::vector& operandIn, std::vector const& offsets, storm::OptimizationDirection const& dir, - std::vector& schedulerStorage, bool robust, std::vector* operandOut = nullptr, - boost::optional> const& robustIndices = boost::none) const; + std::vector& schedulerStorage, UncertaintyResolutionMode uncertaintyResolutionMode, + std::vector* operandOut = nullptr, boost::optional> const& robustIndices = boost::none) const; private: /*! diff --git a/src/storm/solver/helper/ValueIterationHelper.cpp b/src/storm/solver/helper/ValueIterationHelper.cpp index 9837385a57..3a06739e8f 100644 --- a/src/storm/solver/helper/ValueIterationHelper.cpp +++ b/src/storm/solver/helper/ValueIterationHelper.cpp @@ -2,6 +2,7 @@ #include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" +#include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/solver/helper/ValueIterationOperator.h" #include "storm/utility/Extremum.h" @@ -103,9 +104,15 @@ template template SolverStatus ValueIterationHelper::VI(std::vector& operand, std::vector const& offsets, uint64_t& numIterations, SolutionType const& precision, - std::function const& iterationCallback, - MultiplicationStyle mult, bool adversarialRobust) const { - if (adversarialRobust) { + const std::function& iterationCallback, + MultiplicationStyle mult, + const UncertaintyResolutionMode& uncertaintyResolutionMode) const { + bool robustUncertainty = false; + if (storm::IsIntervalType) { + robustUncertainty = isUncertaintyResolvedRobust(uncertaintyResolutionMode, Dir); + } + + if (robustUncertainty) { return VI(operand, offsets, numIterations, precision, iterationCallback, mult); } else { return VI(operand, offsets, numIterations, precision, iterationCallback, mult); @@ -117,19 +124,33 @@ SolverStatus ValueIterationHelper:: uint64_t& numIterations, bool relative, SolutionType const& precision, std::optional const& dir, std::function const& iterationCallback, - MultiplicationStyle mult, bool adversarialRobust) const { + MultiplicationStyle mult, + UncertaintyResolutionMode const& uncertaintyResolutionMode) const { + if (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 && + uncertaintyResolutionMode != UncertaintyResolutionMode::Cooperative), + storm::exceptions::IllegalFunctionCallException, + "Robust or cooperative nature resolution modes cannot be used if optimization direction is not set."); + } + STORM_LOG_ASSERT(TrivialRowGrouping || dir.has_value(), "no optimization direction given!"); if (!dir.has_value() || maximize(*dir)) { if (relative) { - return VI(operand, offsets, numIterations, precision, iterationCallback, mult, adversarialRobust); + return VI(operand, offsets, numIterations, precision, iterationCallback, mult, + uncertaintyResolutionMode); } else { - return VI(operand, offsets, numIterations, precision, iterationCallback, mult, adversarialRobust); + return VI(operand, offsets, numIterations, precision, iterationCallback, mult, + uncertaintyResolutionMode); } } else { if (relative) { - return VI(operand, offsets, numIterations, precision, iterationCallback, mult, adversarialRobust); + return VI(operand, offsets, numIterations, precision, iterationCallback, mult, + uncertaintyResolutionMode); } else { - return VI(operand, offsets, numIterations, precision, iterationCallback, mult, adversarialRobust); + return VI(operand, offsets, numIterations, precision, iterationCallback, mult, + uncertaintyResolutionMode); } } } @@ -139,9 +160,10 @@ SolverStatus ValueIterationHelper:: bool relative, SolutionType const& precision, std::optional const& dir, std::function const& iterationCallback, - MultiplicationStyle mult, bool adversarialRobust) const { + MultiplicationStyle mult, + UncertaintyResolutionMode const& uncertaintyResolutionMode) const { uint64_t numIterations = 0; - return VI(operand, offsets, numIterations, relative, precision, dir, iterationCallback, mult, adversarialRobust); + return VI(operand, offsets, numIterations, relative, precision, dir, iterationCallback, mult, uncertaintyResolutionMode); } template class ValueIterationHelper; diff --git a/src/storm/solver/helper/ValueIterationHelper.h b/src/storm/solver/helper/ValueIterationHelper.h index e29c2f193e..3a78450463 100644 --- a/src/storm/solver/helper/ValueIterationHelper.h +++ b/src/storm/solver/helper/ValueIterationHelper.h @@ -8,6 +8,7 @@ #include "storm/solver/MultiplicationStyle.h" #include "storm/solver/OptimizationDirection.h" #include "storm/solver/SolverStatus.h" +#include "storm/solver/UncertaintyResolutionMode.h" #include "storm/solver/helper/ValueIterationOperatorForward.h" namespace storm::solver::helper { @@ -24,17 +25,18 @@ class ValueIterationHelper { template SolverStatus VI(std::vector& operand, std::vector const& offsets, uint64_t& numIterations, SolutionType const& precision, - std::function const& iterationCallback = {}, MultiplicationStyle mult = MultiplicationStyle::GaussSeidel, - bool robust = true) const; + const std::function& iterationCallback = {}, MultiplicationStyle mult = MultiplicationStyle::GaussSeidel, + UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset) const; SolverStatus VI(std::vector& operand, std::vector const& offsets, uint64_t& numIterations, bool relative, SolutionType const& precision, std::optional const& dir = {}, std::function const& iterationCallback = {}, MultiplicationStyle mult = MultiplicationStyle::GaussSeidel, - bool robust = true) const; + UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset) const; SolverStatus VI(std::vector& operand, std::vector const& offsets, bool relative, SolutionType const& precision, std::optional const& dir = {}, std::function const& iterationCallback = {}, - MultiplicationStyle mult = MultiplicationStyle::GaussSeidel, bool robust = true) const; + MultiplicationStyle mult = MultiplicationStyle::GaussSeidel, + UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset) const; private: std::shared_ptr> viOperator; diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index a5db7a903c..10defa7606 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -173,7 +173,8 @@ boost::optional const& Scheduler::ge } template -void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices, +template +void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices, bool skipDontCareStates) const { STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); @@ -308,7 +309,8 @@ void Scheduler::printToStream(std::ostream& out, std::shared_ptr -void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices, +template +void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices, bool skipDontCareStates) const { STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); @@ -392,5 +394,24 @@ template class Scheduler; template class Scheduler; template class Scheduler; +template void Scheduler::printToStream(std::ostream&, std::shared_ptr>, bool, bool) const; +template void Scheduler::printToStream(std::ostream&, std::shared_ptr>, bool, + bool) const; +template void Scheduler::printToStream(std::ostream&, std::shared_ptr>, bool, + bool) const; +template void Scheduler>::printToStream(std::ostream&, std::shared_ptr>, + bool, bool) const; +template void Scheduler::printToStream(std::ostream&, std::shared_ptr>, bool, bool) const; + +template void Scheduler::printJsonToStream(std::ostream&, std::shared_ptr>, bool, bool) const; +template void Scheduler::printJsonToStream(std::ostream&, std::shared_ptr>, bool, + bool) const; +template void Scheduler::printJsonToStream(std::ostream&, std::shared_ptr>, bool, + bool) const; +template void Scheduler>::printJsonToStream(std::ostream&, + std::shared_ptr>, bool, + bool) const; +template void Scheduler::printJsonToStream(std::ostream&, std::shared_ptr>, bool, bool) const; + } // namespace storage } // namespace storm diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 4bf67f486a..3f0f660201 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -138,7 +138,8 @@ class Scheduler { * Requires a model to be given. * @param skipDontCareStates If true, the choice for dontCareStates states is not printed explicitly. */ - void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, + template + void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const; /*! @@ -150,7 +151,8 @@ class Scheduler { * Requires a model to be given. * @param skipDontCareStates If true, the choice for dontCareStates states is not printed explicitly. */ - void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, + template + void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const; private: diff --git a/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp b/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp index 4956c8ef73..b0e51a0fe8 100644 --- a/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp +++ b/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp @@ -79,8 +79,8 @@ void testModelInterval(std::string programFile, std::string formulaAsString, std solver2->setMatrix(withoutMECs); auto x2 = std::vector(target2.size(), 0); - solver1->setUncertaintyIsRobust(false); - solver2->setUncertaintyIsRobust(false); + solver1->setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative); + solver2->setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative); // Check that maximize is the same solver1->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); diff --git a/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 0000000000..8e707e9363 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,229 @@ +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/api/model_descriptions.h" +#include "storm-parsers/api/properties.h" +#include "storm-parsers/parser/DirectEncodingParser.h" +#include "storm/adapters/IntervalAdapter.h" +#include "storm/api/builder.h" +#include "storm/api/properties.h" +#include "storm/api/verification.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/transformer/AddUncertainty.h" + +std::unique_ptr getInitialStateFilter( + std::shared_ptr> const& model) { + return std::make_unique(model->getInitialStates()); +} + +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); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); +} + +double 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::optional uncertaintyResolutionMode = std::nullopt) { + std::shared_ptr> modelPtr = storm::parser::DirectEncodingParser::parseModel(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 expectThrowPrism(std::string const& path, std::string const& formulaString) { + 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 task = storm::modelchecker::CheckTask(*formulas[0]); + + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(*dtmc); + STORM_SILENT_EXPECT_THROW(checker.check(env, task), storm::exceptions::InvalidArgumentException); +} + +void checkExplicitModelForQuantitativeResult(std::string const& path, std::string const& formulaString, double min, double max) { + std::shared_ptr> modelPtr = storm::parser::DirectEncodingParser::parseModel(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_NEAR(max, getQuantitativeResultAtInitialState(dtmc, resultMax), 0.0001); + + auto taskMin = storm::modelchecker::CheckTask(*formulas[1]); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + + auto resultMin = checker.check(env, taskMin); + EXPECT_NEAR(min, getQuantitativeResultAtInitialState(dtmc, resultMin), 0.0001); +} + +void checkPrismModelForQuantitativeResult(std::string const& path, std::string const& formulaString, double min, double 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_NEAR(max, getQuantitativeResultAtInitialState(dtmc, resultMax), 0.0001); + + auto taskMin = storm::modelchecker::CheckTask(*formulas[1]); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + + auto resultMin = checker.check(env, taskMin); + EXPECT_NEAR(min, getQuantitativeResultAtInitialState(dtmc, resultMin), 0.0001); +} + +void checkModelForQualitativeResult(std::string const& path, std::string const& formulaString, std::vector expectedResultVector) { + std::shared_ptr> modelPtr = storm::parser::DirectEncodingParser::parseModel(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 task1 = storm::modelchecker::CheckTask(*formulas[0]); + + auto checker = storm::modelchecker::SparsePropositionalModelChecker>(*dtmc); + auto result = checker.check(env, task1); + + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + + for (size_t i = 0; i < expectedResultVector[0].size(); i++) { + EXPECT_EQ(expectedResultVector[0].get(i), result->asExplicitQualitativeCheckResult()[i]); + } + + auto task2 = storm::modelchecker::CheckTask(*formulas[1]); + + result = checker.check(env, task2); + + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + + for (size_t i = 0; i < expectedResultVector[1].size(); i++) { + EXPECT_EQ(expectedResultVector[1].get(i), result->asExplicitQualitativeCheckResult()[i]); + } +} + +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); +} + +TEST(RobustDtmcModelCheckerTest, Tiny01MaxReachProbNoUncertaintyResolutionMode) { + // Nature requires a resolution mode, expect thrown. + expectThrow(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-01.drn", "P=? [ F \"target\"];", + std::make_optional(storm::UncertaintyResolutionMode::Unset)); +} + +TEST(RobustDtmcModelCheckerTest, Tiny01MaxReachProbNoOptimizationDirectionButRobust) { + // Nature requires a resolution mode, expect thrown. + expectThrow(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-01.drn", "P=? [ F \"target\"];", + std::make_optional(storm::UncertaintyResolutionMode::Robust)); +} + +TEST(RobustDtmcModelCheckerTest, Tiny02GloballyMaxMinProbs) { + // Globally not yet supported, expect throw. + expectThrow(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-02.drn", "P=? [ G \"target\"];P=? [ G \"target\"]"); +} + +TEST(RobustDtmcModelCheckerTest, DieIntervalsMaxMin) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + // Maxima reachability probabilities using PRISM format. + checkPrismModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/die-intervals.pm", "P=? [ F \"one\"];P=? [ F \"one\"]", 9.0 / 189.0, 72.0 / 189.0); +} + +TEST(RobustDtmcModelCheckerTest, BrpIntervalsMaxMin) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + // Maxima reachability probabilities using PRISM format. + checkPrismModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/brp-32-2-intervals.pm", "P=? [ F \"error\" ];P=? [ F \"error\" ]", + 2.559615918664207e-10, 0.0008464876763422187); +} + +TEST(RobustDtmcModelCheckerTest, DieIntervalsMaxMinRewards) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + // Maxima reachability rewards using PRISM format. + checkPrismModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/die-intervals.pm", "R=? [ F \"done\"];R=? [ F \"done\"]", 3.25, 4.6); +} + +TEST(RobustDtmcModelCheckerTest, Tiny03MaxMinRewards) { + // Maxima reachability rewards using explicit format. + checkExplicitModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-03.drn", "R=? [ F \"target\"];R=? [ F \"target\"]", 6.5, 8.5); +} + +TEST(RobustDtmcModelCheckerTest, Tiny03RewardsNoUncertaintyResolutionMode) { + // Nature requires a resolution mode, expect thrown. + expectThrow(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-03.drn", "R=? [ F \"target\"]", storm::UncertaintyResolutionMode::Unset); +} + +TEST(RobustDtmcModelCheckerTest, Tiny04MaxMinRewards) { + // Maxima reachability rewards using explicit format - infinite reward case. + checkExplicitModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-04.drn", "R=? [ F \"target\"];R=? [ F \"target\"]", + std::numeric_limits::infinity(), std::numeric_limits::infinity()); +} + +TEST(RobustDtmcModelCheckerTest, TinyO2Propositional) { + // Propositional formula using explicit format. + std::vector expectedResults; + auto result1 = storm::storage::BitVector(3); + result1.set(0); + result1.set(2); + expectedResults.push_back(result1); + result1.complement(); + expectedResults.push_back(result1); + + checkModelForQualitativeResult(STORM_TEST_RESOURCES_DIR "/idtmc/tiny-02.drn", "\"target\";!\"target\"", expectedResults); +} diff --git a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp index 27a9254a16..1d80f650cd 100644 --- a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "storm-parsers/api/model_descriptions.h" #include "storm-parsers/api/properties.h" #include "storm-parsers/parser/DirectEncodingParser.h" +#include "storm/adapters/IntervalAdapter.h" #include "storm/api/builder.h" #include "storm/api/properties.h" #include "storm/api/verification.h" @@ -50,7 +51,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::BaseException); } void checkModel(std::string const& path, std::string const& formulaString, double maxmin, double maxmax, double minmax, double minmin, bool produceScheduler) { @@ -62,25 +63,77 @@ void checkModel(std::string const& path, std::string const& formulaString, doubl std::shared_ptr> mdp = modelPtr->as>(); ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType()); auto taskMax = storm::modelchecker::CheckTask(*formulas[0]); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust); taskMax.setProduceSchedulers(produceScheduler); auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); auto resultMax = checker.check(env, taskMax); EXPECT_NEAR(maxmin, getQuantitativeResultAtInitialState(mdp, resultMax), 0.0001); - taskMax.setRobustUncertainty(false); + taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative); auto resultMaxNonRobust = checker.check(env, taskMax); EXPECT_NEAR(maxmax, getQuantitativeResultAtInitialState(mdp, resultMaxNonRobust), 0.0001); auto taskMin = storm::modelchecker::CheckTask(*formulas[1]); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust); taskMin.setProduceSchedulers(produceScheduler); auto resultMin = checker.check(env, taskMin); EXPECT_NEAR(minmax, getQuantitativeResultAtInitialState(mdp, resultMin), 0.0001); - taskMin.setRobustUncertainty(false); + taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative); auto resultMinNonRobust = checker.check(env, taskMin); EXPECT_NEAR(minmin, getQuantitativeResultAtInitialState(mdp, resultMinNonRobust), 0.0001); } +void checkPrismModelForQuantitativeResult(std::string const& path, std::string const& formulaString, double minmin, double minmax, double maxmin, double maxmax, + std::string constantsString) { + storm::prism::Program program = storm::api::parseProgram(path); + program = storm::utility::prism::preprocess(program, constantsString); + + 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> mdp = modelPtr->as>(); + ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType()); + + auto taskMinMin = storm::modelchecker::CheckTask(*formulas[0]); + taskMinMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + + auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); + auto resultMinMin = checker.check(env, taskMinMin); + EXPECT_NEAR(minmin, getQuantitativeResultAtInitialState(mdp, resultMinMin), 0.0001); + + auto taskMinMax = storm::modelchecker::CheckTask(*formulas[1]); + taskMinMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize); + + auto resultMinMax = checker.check(env, taskMinMax); + EXPECT_NEAR(minmax, getQuantitativeResultAtInitialState(mdp, resultMinMax), 0.0001); + + auto taskMaxMin = storm::modelchecker::CheckTask(*formulas[2]); + taskMaxMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize); + + auto resultMaxMin = checker.check(env, taskMaxMin); + EXPECT_NEAR(maxmin, getQuantitativeResultAtInitialState(mdp, resultMaxMin), 0.0001); + + auto taskMaxMax = storm::modelchecker::CheckTask(*formulas[3]); + taskMaxMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize); + + auto resultMaxMax = checker.check(env, taskMaxMax); + EXPECT_NEAR(maxmax, getQuantitativeResultAtInitialState(mdp, resultMaxMax), 0.0001); +} + +TEST(RobustMdpModelCheckerTest, RobotMinMaxTest) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + // Maxima reachability rewards using PRISM format. + checkPrismModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/imdp/robot.prism", + "Pmin=? [ F \"goal2\"];Pmin=? [ F \"goal2\"];Pmax=? [ F \"goal2\"];Pmax=? [ F \"goal2\"]", 0.4, 0.6, 1.0, 1.0, + "delta=0.1"); +} + void makeUncertainAndCheck(std::string const& path, std::string const& formulaString, double amountOfUncertainty) { storm::prism::Program program = storm::api::parseProgram(path); program = storm::utility::prism::preprocess(program, ""); @@ -109,7 +162,7 @@ void makeUncertainAndCheck(std::string const& path, std::string const& formulaSt auto iresultMin = checker.check(env, task); double minValue = getQuantitativeResultAtInitialState(mdp, iresultMin); EXPECT_LE(minValue, certainValue); - task.setRobustUncertainty(false); + task.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative); auto iresultMax = checker.check(env, task); double maxValue = getQuantitativeResultAtInitialState(mdp, iresultMax); EXPECT_LE(certainValue, maxValue);