diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 5df3aeee6..08b64a406 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -155,7 +155,9 @@ namespace storm { formula.asProbabilityOperatorFormula()); pomdp.getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget); storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula()); + bool computedSomething = false; if (qualSettings.isMemlessSearchSet()) { + computedSomething = true; storm::expressions::ExpressionManager expressionManager; std::shared_ptr smtSolverFactory = std::make_shared(); storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings(); @@ -168,7 +170,7 @@ namespace storm { surelyNotAlmostSurelyReachTarget, smtSolverFactory); if (qualSettings.isWinningRegionSet()) { - STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless."); + STORM_LOG_ERROR("Computing winning regions is not supported by the one-shot method."); } else { memlessSearch.analyzeForInitialStates(lookahead); } @@ -206,21 +208,28 @@ namespace storm { ++offset; } } - STORM_PRINT_AND_LOG("Initial state is safe: " - << search.getLastWinningRegion().isWinning(initialObservation, - offset)); + + if (search.getLastWinningRegion().isWinning(initialObservation, + offset)) { + STORM_PRINT_AND_LOG("Initial state is safe!" + << std::endl); + } else { + STORM_PRINT_AND_LOG("Initial state may not be safe." + << std::endl); + } } else { STORM_LOG_WARN("Output for multiple initial states is incomplete"); } - std::cout << "Number of belief support states: " - << search.getLastWinningRegion().beliefSupportStates() << std::endl; - if (coreSettings.isShowStatisticsSet() && qualSettings.computeExpensiveStats()) { - auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs(); - STORM_PRINT_AND_LOG( - "Number of winning belief support states: [" << wbss.first << "," << wbss.second - << "]"); - } + if (coreSettings.isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("#STATS Number of belief support states: " + << search.getLastWinningRegion().beliefSupportStates() << std::endl); + if (qualSettings.computeExpensiveStats()) { + auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs(); + STORM_PRINT_AND_LOG( + "#STATS Number of winning belief support states: [" << wbss.first << "," << wbss.second + << "]"); + } search.getStatistics().print(); } @@ -229,12 +238,15 @@ namespace storm { } } if (qualSettings.isComputeOnBeliefSupportSet()) { + computedSomething = true; storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator janicreator(pomdp); janicreator.generate(targetStates, surelyNotAlmostSurelyReachTarget); bool initialOnly = !qualSettings.isWinningRegionSet(); janicreator.verifySymbolic(initialOnly); STORM_PRINT_AND_LOG("Initial state is safe: " << janicreator.isInitialWinning() << "\n"); } + STORM_LOG_THROW(computedSomething, storm::exceptions::InvalidSettingsException, "Nothing to be done, did you forget to set a method?"); + } template diff --git a/src/storm-pomdp/analysis/IterativePolicySearch.cpp b/src/storm-pomdp/analysis/IterativePolicySearch.cpp index f41550e9a..9dd1357d8 100644 --- a/src/storm-pomdp/analysis/IterativePolicySearch.cpp +++ b/src/storm-pomdp/analysis/IterativePolicySearch.cpp @@ -35,16 +35,16 @@ namespace storm { template void IterativePolicySearch::Statistics::print() const { - STORM_PRINT_AND_LOG("Total time: " << totalTimer); - STORM_PRINT_AND_LOG("SAT Calls " << satCalls); - STORM_PRINT_AND_LOG("SAT Calls time: " << smtCheckTimer); - STORM_PRINT_AND_LOG("Outer iterations: " << outerIterations); - STORM_PRINT_AND_LOG("Solver initialization time: " << initializeSolverTimer); - STORM_PRINT_AND_LOG("Obtain partial scheduler time: " << evaluateExtensionSolverTime); - STORM_PRINT_AND_LOG("Update solver to extend partial scheduler time: " << encodeExtensionSolverTime); - STORM_PRINT_AND_LOG("Update solver with new scheduler time: " << updateNewStrategySolverTime); - STORM_PRINT_AND_LOG("Winning regions update time: " << winningRegionUpdatesTimer); - STORM_PRINT_AND_LOG("Graph search time: " << graphSearchTime); + STORM_PRINT_AND_LOG("#STATS Total time: " << totalTimer << std::endl); + STORM_PRINT_AND_LOG("#STATS SAT Calls: " << satCalls << std::endl); + STORM_PRINT_AND_LOG("#STATS SAT Calls time: " << smtCheckTimer << std::endl); + STORM_PRINT_AND_LOG("#STATS Outer iterations: " << outerIterations << std::endl); + STORM_PRINT_AND_LOG("#STATS Solver initialization time: " << initializeSolverTimer << std::endl); + STORM_PRINT_AND_LOG("#STATS Obtain partial scheduler time: " << evaluateExtensionSolverTime << std::endl ); + STORM_PRINT_AND_LOG("#STATS Update solver to extend partial scheduler time: " << encodeExtensionSolverTime << std::endl); + STORM_PRINT_AND_LOG("#STATS Update solver with new scheduler time: " << updateNewStrategySolverTime << std::endl); + STORM_PRINT_AND_LOG("#STATS Winning regions update time: " << winningRegionUpdatesTimer << std::endl); + STORM_PRINT_AND_LOG("#STATS Graph search time: " << graphSearchTime << std::endl); } template @@ -203,8 +203,6 @@ namespace storm { ++obs; } - - // Update at least one observation. // PAPER COMMENT: 2 smtSolver->add(storm::expressions::disjunction(observationUpdatedExpressions)); @@ -265,8 +263,6 @@ namespace storm { } } - - rowindex = 0; for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { // PAPER COMMENT 5 @@ -334,7 +330,6 @@ namespace storm { actPathDisjunction.push_back(storm::expressions::disjunction(pathDisjunction) && actionSelectionVarExpressions.at(pomdp.getObservation(state)).at(action)); rowindex++; } - // TODO reconsider if this next add is sound actPathDisjunction.push_back(switchVarExpressions.at(pomdp.getObservation(state))); actPathDisjunction.push_back(followVarExpressions[pomdp.getObservation(state)]); actPathDisjunction.push_back(!reachVarExpressions[state]); @@ -349,7 +344,6 @@ namespace storm { } } else { smtSolver->add(pathVarExpressions[state][0] == expressionManager->integer(0)); - //assert(false); } } smtSolver->add(reachVars[state]); diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp index be6a65f78..f8501eb96 100644 --- a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp +++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp @@ -200,16 +200,14 @@ namespace storm { } if(result && !onlyInitial) { - std::cout << "count: " << result->asQualitativeCheckResult().count() << std::endl; + auto vars = result->asSymbolicQualitativeCheckResult().getTruthValuesVector().getContainedMetaVariables(); + } else if (result) { initialIsWinning = result->asQualitativeCheckResult().existsTrue(); } - - - } - template + template bool JaniBeliefSupportMdpGenerator::isInitialWinning() const { return initialIsWinning; } diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h index f10fa3d0d..d0e7a8a5c 100644 --- a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h +++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h @@ -16,6 +16,7 @@ namespace storm { void generate(storm::storage::BitVector const& targetStates, storm::storage::BitVector const& badStates); void verifySymbolic(bool onlyInitial = true); bool isInitialWinning() const; + private: storm::models::sparse::Pomdp const& pomdp; jani::Model model; diff --git a/src/storm-pomdp/analysis/OneShotPolicySearch.h b/src/storm-pomdp/analysis/OneShotPolicySearch.h index fb2b4d5a7..af7203cea 100644 --- a/src/storm-pomdp/analysis/OneShotPolicySearch.h +++ b/src/storm-pomdp/analysis/OneShotPolicySearch.h @@ -55,9 +55,9 @@ namespace storm { STORM_LOG_TRACE("Questionmark states: " << (~surelyReachSinkStates & ~targetStates)); bool result = analyze(k, ~surelyReachSinkStates & ~targetStates, pomdp.getInitialStates()); if (result) { - STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target."); + STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target." << std::endl); } else { - STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target ."); + STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target ." << std::endl); } }