From 149fc2e00978e22eb0e38f765cf51e7c8b5c1281 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 24 Nov 2017 11:54:09 +0100 Subject: [PATCH] The solution to the minmax equation system becomes unique after eliminating end components. --- .../modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp | 6 ++++++ .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 2 ++ 2 files changed, 8 insertions(+) diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index c38b32c91..ad1903d1c 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -199,6 +199,10 @@ namespace storm { // Eliminate the end components and remove the states that are not interesting (target or non-filter). eliminateEndComponentsAndExtendedStatesUntilProbabilities(explicitRepresentation, solverRequirementsData, targetStates); + + // The solution becomes unique after end components have been eliminated. + uniqueSolution = true; + } else { // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all // maybe states. @@ -571,6 +575,8 @@ namespace storm { if (requirements.requiresNoEndComponents()) { eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.requiresUpperBounds()); + // The solution becomes unique after end components have been eliminated. + uniqueSolution = true; } else { if (requirements.requiresValidInitialScheduler()) { // Compute a valid initial scheduler. diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 1316eff78..8c7b0dc7e 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -441,6 +441,8 @@ namespace storm { STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique."); STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); result.eliminateEndComponents = true; + // If end components have been eliminated we can assume a unique solution. + result.uniqueSolution = true; requirements.clearNoEndComponents(); }