From 6b6f44100ee66aaac7550f3fbf63b3ac9db02665 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Mar 2021 16:16:39 -0800 Subject: [PATCH 01/10] allow building parametric models of the form s --p-->, s--q--> --- src/storm/generator/JaniNextStateGenerator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 4710dd432..66f69c9cb 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -741,7 +741,7 @@ namespace storm { if (this->options.isExplorationChecksSet()) { // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); + STORM_LOG_THROW(!this->isDiscreteTimeModel() || (!storm::utility::isConstant(probabilitySum) || this->comparator.isOne(probabilitySum)), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); } return choice; From 08f928456cb6c1184f3b5bf8691917bdcfb17eb3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Mar 2021 16:18:24 -0800 Subject: [PATCH 02/10] fix guard for code that considers transient assignments to also consider only transient assignments --- src/storm/generator/JaniNextStateGenerator.cpp | 2 +- src/storm/storage/jani/OrderedAssignments.cpp | 5 ++++- src/storm/storage/jani/OrderedAssignments.h | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 66f69c9cb..58a2d9010 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -763,7 +763,7 @@ namespace storm { storm::jani::Edge const& edge = *iteratorList[i]->second; lowestDestinationAssignmentLevel = std::min(lowestDestinationAssignmentLevel, edge.getLowestAssignmentLevel()); highestDestinationAssignmentLevel = std::max(highestDestinationAssignmentLevel, edge.getHighestAssignmentLevel()); - if (!edge.getAssignments().empty()) { + if (!edge.getAssignments().empty(true)) { lowestEdgeAssignmentLevel = std::min(lowestEdgeAssignmentLevel, edge.getAssignments().getLowestLevel(true)); highestEdgeAssignmentLevel = std::max(highestEdgeAssignmentLevel, edge.getAssignments().getHighestLevel(true)); } diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 747fbcecd..5d76ae03b 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -87,7 +87,10 @@ namespace storm { return getLowestLevel(onlyTransient) != 0 || getHighestLevel(onlyTransient) != 0; } - bool OrderedAssignments::empty() const { + bool OrderedAssignments::empty(bool onlyTransient) const { + if (onlyTransient) { + return transientAssignments.empty(); + } return allAssignments.empty(); } diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index de914b738..877ea845d 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -57,7 +57,7 @@ namespace storm { /*! * Retrieves whether this set of assignments is empty. */ - bool empty() const; + bool empty(bool onlyTransient = false) const; /*! * Removes all assignments from this set. From 3c58b5b2f74d8762c140d254b5abb30b0551cad4 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Mar 2021 16:19:18 -0800 Subject: [PATCH 03/10] case split for MDPs actually checks for MDPs --- src/storm-pars-cli/storm-pars.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 65c68a6c9..165bda5d4 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -380,7 +380,7 @@ namespace storm { verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); } else if (model->isOfType(storm::models::ModelType::Ctmc)) { verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); - } else if (model->isOfType(storm::models::ModelType::Ctmc)) { + } else if (model->isOfType(storm::models::ModelType::Mdp)) { verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs."); From d6ab421cb703fb52869b23b0aa4be5a8ea1a5492 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Mar 2021 16:27:28 -0800 Subject: [PATCH 04/10] add belief-support-mdp generator --- .../settings/PomdpSettings.cpp | 1 + .../QualitativePOMDPAnalysisSettings.cpp | 6 + .../QualitativePOMDPAnalysisSettings.h | 1 + src/storm-pomdp-cli/storm-pomdp.cpp | 128 ++++++---- .../JaniBeliefSupportMdpGenerator.cpp | 235 ++++++++++++++++++ .../analysis/JaniBeliefSupportMdpGenerator.h | 27 ++ 6 files changed, 343 insertions(+), 55 deletions(-) create mode 100644 src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp create mode 100644 src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h diff --git a/src/storm-pomdp-cli/settings/PomdpSettings.cpp b/src/storm-pomdp-cli/settings/PomdpSettings.cpp index f529d8073..a8def4e9e 100644 --- a/src/storm-pomdp-cli/settings/PomdpSettings.cpp +++ b/src/storm-pomdp-cli/settings/PomdpSettings.cpp @@ -47,6 +47,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp index 1d6ff6d49..112ecff25 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp @@ -23,6 +23,7 @@ namespace storm { const std::string printWinningRegionOption = "printwinningregion"; const std::string exportWinningRegionOption = "exportwinningregion"; const std::string preventGraphPreprocessing = "nographprocessing"; + const std::string beliefSupportMCOption = "belsupmc"; const std::string memlessSearchOption = "memlesssearch"; std::vector memlessSearchMethods = {"one-shot", "iterative"}; @@ -33,6 +34,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, exportSATCallsOption, false, "Export the SAT calls?.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the path to which to write the models.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadHorizonOption, false, "In reachability in combination with a discrete ranking function, a lookahead is necessary.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("bound", "The lookahead. Use 0 for the number of states.").setDefaultValueUnsignedInteger(0).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, onlyDeterministicOption, false, "Search only for deterministic schedulers").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, beliefSupportMCOption, false, "Create a symbolic description of the belief-support MDP to use for analysis purposes").build()); this->addOption(storm::settings::OptionBuilder(moduleName, winningRegionOption, false, "Search for the winning region").build()); this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadTypeOption, false, "What type to use for the ranking function").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type.").setDefaultValueString("real").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"bool", "int", "real"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, validationLevel, true, "Validate algorithm during runtime (for debugging)").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "how regular to apply this validation. Use 0 for never, 1 for the end, and >=2 within computation steps.").setDefaultValueUnsignedInteger(0).build()).build()); @@ -66,6 +68,10 @@ namespace storm { return this->getOption(winningRegionOption).getHasOptionBeenSet(); } + bool QualitativePOMDPAnalysisSettings::isComputeOnBeliefSupportSet() const { + return this->getOption(beliefSupportMCOption).getHasOptionBeenSet(); + } + bool QualitativePOMDPAnalysisSettings::validateIntermediateSteps() const { return this->getOption(validationLevel).getArgumentByName("level").getValueAsUnsignedInteger() >= 2; } diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h index cebb356e3..51477c771 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h @@ -29,6 +29,7 @@ namespace storm { bool validateIntermediateSteps() const; bool validateFinalResult() const; bool computeExpensiveStats() const; + bool isComputeOnBeliefSupportSet() const; bool isPrintWinningRegionSet() const; bool isExportWinningRegionSet() const; std::string exportWinningRegionPath() const; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 7cc999ec9..ba2ed275d 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -26,6 +26,7 @@ #include "storm-pomdp/analysis/FormulaInformation.h" #include "storm-pomdp/analysis/IterativePolicySearch.h" #include "storm-pomdp/analysis/OneShotPolicySearch.h" +#include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h" #include "storm/api/storm.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -154,68 +155,85 @@ namespace storm { formula.asProbabilityOperatorFormula()); pomdp.getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget); storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula()); - - storm::expressions::ExpressionManager expressionManager; - std::shared_ptr smtSolverFactory = std::make_shared(); - storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings(); - uint64_t lookahead = qualSettings.getLookahead(); - if (lookahead == 0) { - lookahead = pomdp.getNumberOfStates(); - } - if (qualSettings.getMemlessSearchMethod() == "one-shot") { - storm::pomdp::OneShotPolicySearch memlessSearch(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); - if (qualSettings.isWinningRegionSet()) { - STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless."); - } else { - memlessSearch.analyzeForInitialStates(lookahead); - } - } else if (qualSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::IterativePolicySearch search(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); - if (qualSettings.isWinningRegionSet()) { - search.computeWinningRegion(lookahead); - } else { - search.analyzeForInitialStates(lookahead); + if (qualSettings.isMemlessSearchSet()) { + storm::expressions::ExpressionManager expressionManager; + std::shared_ptr smtSolverFactory = std::make_shared(); + storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings(); + uint64_t lookahead = qualSettings.getLookahead(); + if (lookahead == 0) { + lookahead = pomdp.getNumberOfStates(); } + if (qualSettings.getMemlessSearchMethod() == "one-shot") { + storm::pomdp::OneShotPolicySearch memlessSearch(pomdp, targetStates, + surelyNotAlmostSurelyReachTarget, + smtSolverFactory); + if (qualSettings.isWinningRegionSet()) { + STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless."); + } else { + memlessSearch.analyzeForInitialStates(lookahead); + } + } else if (qualSettings.getMemlessSearchMethod() == "iterative") { + storm::pomdp::IterativePolicySearch search(pomdp, targetStates, + surelyNotAlmostSurelyReachTarget, + smtSolverFactory, options); + if (qualSettings.isWinningRegionSet()) { + search.computeWinningRegion(lookahead); + } else { + search.analyzeForInitialStates(lookahead); + } - if (qualSettings.isPrintWinningRegionSet()) { - search.getLastWinningRegion().print(); - std::cout << std::endl; - } - if (qualSettings.isExportWinningRegionSet()) { - std::size_t hash = pomdp.hash(); - search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath(), "model hash: " + std::to_string(hash)); - } + if (qualSettings.isPrintWinningRegionSet()) { + search.getLastWinningRegion().print(); + std::cout << std::endl; + } + if (qualSettings.isExportWinningRegionSet()) { + std::size_t hash = pomdp.hash(); + search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath(), + "model hash: " + std::to_string(hash)); + } - search.finalizeStatistics(); - if(pomdp.getInitialStates().getNumberOfSetBits() == 1) { - uint64_t initialState = pomdp.getInitialStates().getNextSetIndex(0); - uint64_t initialObservation = pomdp.getObservation(initialState); - // TODO this is inefficient. - uint64_t offset = 0; - for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { - if (state == initialState) { - break; - } - if (pomdp.getObservation(state) == initialObservation) { - ++offset; + search.finalizeStatistics(); + if (pomdp.getInitialStates().getNumberOfSetBits() == 1) { + uint64_t initialState = pomdp.getInitialStates().getNextSetIndex(0); + uint64_t initialObservation = pomdp.getObservation(initialState); + // TODO this is inefficient. + uint64_t offset = 0; + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + if (state == initialState) { + break; + } + if (pomdp.getObservation(state) == initialObservation) { + ++offset; + } } + STORM_PRINT_AND_LOG("Initial state is safe: " + << search.getLastWinningRegion().isWinning(initialObservation, + offset)); + } else { + STORM_LOG_WARN("Output for multiple initial states is incomplete"); } - STORM_PRINT_AND_LOG("Initial state is safe: " << search.getLastWinningRegion().isWinning(initialObservation, offset)); + 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()) { + search.getStatistics().print(); + } + } else { - STORM_LOG_WARN("Output for multiple initial states is incomplete"); + STORM_LOG_ERROR("This method is not implemented."); } - 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()) { - search.getStatistics().print(); - } - - } else { - STORM_LOG_ERROR("This method is not implemented."); + } + if (qualSettings.isComputeOnBeliefSupportSet()) { + 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"); } } diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp new file mode 100644 index 000000000..127c2cdc3 --- /dev/null +++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp @@ -0,0 +1,235 @@ +#include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/io/file.h" +#include "storm/api/verification.h" +#include "storm/api/builder.h" +#include "storm-parsers/api/properties.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" + + +namespace storm { + namespace pomdp { + namespace qualitative { + namespace detail { + struct ObsActPair { + ObsActPair(uint64_t observation, uint64 action) : observation(observation), action(action) {} + + uint64_t observation; + uint64_t action; + }; + + bool operator<(ObsActPair const& o1, ObsActPair const& o2) { + if (o1.observation == o2.observation) { + return o1.action < o2.action; + } + return o1.observation < o2.observation; + } + } + + template + JaniBeliefSupportMdpGenerator::JaniBeliefSupportMdpGenerator(storm::models::sparse::Pomdp const& pomdp) : + pomdp(pomdp), model("beliefsupport", jani::ModelType::MDP) { + // Intentionally left empty. + } + + template + void JaniBeliefSupportMdpGenerator::generate(storm::storage::BitVector const& targetStates, storm::storage::BitVector const& badStates) { + // + std::map>> predecessorInfo; + std::map>> obsPredInfo; + std::set obsactpairs; + // Initialize predecessorInfo for clean steps. + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + predecessorInfo[state] = {}; + } + + // Fill predecessorInfo + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + uint64_t curObs = pomdp.getObservation(state); + for (uint64_t act = 0; act < pomdp.getNumberOfChoices(state); ++act) { + detail::ObsActPair oap(curObs, act); + obsactpairs.insert(oap); + if (obsPredInfo.count(oap) == 0) { + obsPredInfo[oap] = std::map>(); + } + for (auto const& entry : pomdp.getTransitionMatrix().getRow(state, act)) { + if (predecessorInfo[entry.getColumn()].count(oap) == 0) { + predecessorInfo[entry.getColumn()][oap] = {state}; + } else { + predecessorInfo[entry.getColumn()][oap].push_back(state); + } + uint64_t newObs = pomdp.getObservation(entry.getColumn()); + if (obsPredInfo[oap].count(newObs)==0) { + obsPredInfo[oap][newObs] = {state}; + } else { + obsPredInfo[oap][newObs].insert(state); + } + } + } + } + uint64_t initialObs = pomdp.getObservation(*(pomdp.getInitialStates().begin())); + + expressions::ExpressionManager& exprManager = model.getManager(); + storm::expressions::Variable posProbVar = exprManager.declareRationalVariable("posProb"); + model.addConstant(jani::Constant("posProb", posProbVar)); + std::map stateVariables; + jani::BoundedIntegerVariable obsVar = model.addVariable(jani::BoundedIntegerVariable("obs", exprManager.declareIntegerVariable("obs"), exprManager.integer(initialObs), exprManager.integer(0), exprManager.integer(pomdp.getNrObservations()))); + jani::BoundedIntegerVariable oldobsActVar = model.addVariable(jani::BoundedIntegerVariable("prevact", exprManager.declareIntegerVariable("prevact"), exprManager.integer(0), exprManager.integer(0), exprManager.integer(obsactpairs.size()))); + + for (uint64_t i = 0; i < pomdp.getNumberOfStates(); ++i) { + std::string name = "s" + std::to_string(i); + bool isInitial = pomdp.getInitialStates().get(i); + stateVariables.emplace(i, model.addVariable(jani::BooleanVariable(name, exprManager.declareBooleanVariable(name), exprManager.boolean(isInitial)))); + + } + + std::map actionIndices; + for (auto const& oap : obsactpairs) { + std::string actname = "act" + std::to_string(oap.action) + "from" + std::to_string(oap.observation); + uint64_t actindex = model.addAction(jani::Action(actname)); + actionIndices[oap] = actindex; + } + + for (uint64_t i = 0; i < pomdp.getNumberOfStates(); ++i) { + std::string name = "aut-s" + std::to_string(i); + jani::Automaton aut(name, exprManager.declareIntegerVariable(name)); + uint64_t primeloc = aut.addLocation(jani::Location("default")); + aut.addInitialLocation(primeloc); + for (auto const& oaps : actionIndices) { + if (obsPredInfo[oaps.first].count(pomdp.getObservation(i)) == 0 && pomdp.getObservation(i) != oaps.first.observation) { + continue; + } + std::shared_ptr tedge = std::make_shared(exprManager.boolean(true)); + jani::TemplateEdgeDestination edgedest; + std::vector exprVec; + for (auto const& pred : predecessorInfo[i][oaps.first]) { + exprVec.push_back(stateVariables.at(pred).getExpressionVariable().getExpression()); + } + if (exprVec.empty()) { + edgedest.addAssignment(jani::Assignment(stateVariables.at(i), exprManager.boolean(false))); + } else { + edgedest.addAssignment( + jani::Assignment(stateVariables.at(i), (exprManager.integer(pomdp.getObservation(i)) == obsVar.getExpressionVariable().getExpression()) && storm::expressions::disjunction(exprVec))); + } + tedge->addDestination(edgedest); + aut.addEdge(jani::Edge(primeloc, oaps.second, boost::none, tedge, {primeloc}, {exprManager.rational(1.0)})); + } + + + model.addAutomaton(aut); + } + jani::Automaton obsAut("obsAut", exprManager.declareIntegerVariable("obsAut")); + auto const& targetVar = model.addVariable(jani::BooleanVariable("target", exprManager.declareBooleanVariable("target"), exprManager.boolean(false), true)); + std::vector notTargetExpression; + for (auto const& state : ~targetStates) { + notTargetExpression.push_back(!stateVariables.at(state).getExpressionVariable().getExpression()); + } + auto const& badVar = model.addVariable(jani::BooleanVariable("bad", exprManager.declareBooleanVariable("bad"), exprManager.boolean(false), true)); + std::vector badExpression; + for (auto const& state : badStates) { + badExpression.push_back(stateVariables.at(state).getExpressionVariable().getExpression()); + } + + auto primeLocation = jani::Location("primary"); + primeLocation.addTransientAssignment(jani::Assignment(targetVar, expressions::conjunction(notTargetExpression))); + primeLocation.addTransientAssignment(jani::Assignment(badVar, badExpression.empty() ? exprManager.boolean(false) : expressions::disjunction(badExpression))); + uint64_t primeloc = obsAut.addLocation(primeLocation); + obsAut.addInitialLocation(primeloc); + uint64_t secloc = obsAut.addLocation(jani::Location("secondary")); + // First edges, select observation + for (auto const& oaps : actionIndices) { + std::shared_ptr tedge = std::make_shared(exprManager.integer(oaps.first.observation) == obsVar.getExpressionVariable().getExpression()); + std::vector destLocs; + std::vector probs; + + for (auto const& obsAndPredStates : obsPredInfo[oaps.first]) { + jani::TemplateEdgeDestination tedgedest; + tedgedest.addAssignment(jani::Assignment(obsVar, exprManager.integer(obsAndPredStates.first)), true); + tedgedest.addAssignment(jani::Assignment(oldobsActVar, exprManager.integer(oaps.second)), true); + + tedge->addDestination(tedgedest); + + destLocs.push_back(secloc); + std::vector predExpressions; + for (auto predstate : obsAndPredStates.second) { + predExpressions.push_back(stateVariables.at(predstate).getExpressionVariable().getExpression()); + } + probs.push_back(storm::expressions::ite(storm::expressions::disjunction(predExpressions), posProbVar.getExpression(), exprManager.rational(0))); + } + jani::Edge edge(primeloc, jani::Model::SILENT_ACTION_INDEX, boost::none, tedge, destLocs, probs); + obsAut.addEdge(edge); + } + // Back edges + for (auto const& oaps : obsactpairs) { + std::shared_ptr tedge = std::make_shared(oldobsActVar.getExpressionVariable() == exprManager.integer(actionIndices[oaps])); + + jani::TemplateEdgeDestination tedgedest; + tedgedest.addAssignment(jani::Assignment(oldobsActVar, exprManager.integer(0))); + tedge->addDestination(tedgedest); + jani::Edge edge(secloc, actionIndices[oaps], boost::none, tedge, {primeloc}, {exprManager.rational(1.0)}); + obsAut.addEdge(edge); + } + model.addAutomaton(obsAut); + + model.setStandardSystemComposition(); + + + model.finalize(); + std::ofstream ostr; + + storm::utility::openFile("beliefsupport-mdp.jani", ostr); + ostr << model; + model = storm::api::parseJaniModel("beliefsupport-mdp.jani").first; + storm::utility::closeFile(ostr); + } + + template + void JaniBeliefSupportMdpGenerator::verifySymbolic(bool onlyInitial) { + storage::SymbolicModelDescription symdesc(model); + symdesc = symdesc.preprocess("posProb=0.1"); + auto property = storm::api::parsePropertiesForJaniModel("Pmax>=1 [!\"bad\" U \"target\"]", model)[0]; + auto mdp = storm::api::buildSymbolicModel(symdesc, {property.getRawFormula()}); + mdp->printModelInformationToStream(std::cout); + storm::Environment env; + std::unique_ptr result = storm::api::verifyWithDdEngine(env, mdp, storm::api::createTask(property.getRawFormula(), onlyInitial)); + std::unique_ptr filter; + + if (onlyInitial) { + filter = std::make_unique>(mdp->getReachableStates(), mdp->getInitialStates()); + } else { + auto relstates = storm::api::parsePropertiesForJaniModel("prevact=0", model)[0]; + filter = storm::api::verifyWithDdEngine(env, mdp, storm::api::createTask(relstates.getRawFormula(), false)); + } + if (result && filter) { + result->filter(filter->asQualitativeCheckResult()); + } + + if(result && !onlyInitial) { + std::cout << "count: " << result->asQualitativeCheckResult().count() << std::endl; + } else if (result) { + initialIsWinning = result->asQualitativeCheckResult().existsTrue(); + } + + + + } + + template + bool JaniBeliefSupportMdpGenerator::isInitialWinning() const { + return initialIsWinning; + } + + + template class JaniBeliefSupportMdpGenerator; + template class JaniBeliefSupportMdpGenerator; + template class JaniBeliefSupportMdpGenerator; + + + + } + } +} \ No newline at end of file diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h new file mode 100644 index 000000000..f10fa3d0d --- /dev/null +++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h @@ -0,0 +1,27 @@ +#pragma once +#include "storm/models/sparse/Pomdp.h" +#include "storm/storage/jani/Model.h" + + +namespace storm { + + namespace pomdp { + + namespace qualitative { + template + class JaniBeliefSupportMdpGenerator { + + public: + JaniBeliefSupportMdpGenerator(storm::models::sparse::Pomdp const& pomdp); + 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; + bool initialIsWinning = false; + }; + + } + } +} \ No newline at end of file From 3355b21b72926e8fc1060b9f53e072a17c222f6a Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Mar 2021 16:28:17 -0800 Subject: [PATCH 05/10] add timing info to storm-pomdp --- src/storm-pomdp-cli/storm-pomdp.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index ba2ed275d..5df3aeee6 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -475,12 +475,18 @@ int main(const int argc, const char** argv) { if (!optionsCorrect) { return -1; } + storm::utility::Stopwatch totalTimer(true); storm::cli::setUrgentOptions(); // Invoke storm-pomdp with obtained settings storm::pomdp::cli::processOptions(); - // All operations have now been performed, so we clean up everything and terminate. + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + + // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); return 0; // } catch (storm::exceptions::BaseException const &exception) { From 5d45514af26c9d273e2f4de2d8d81920945be787 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Mar 2021 21:21:14 -0800 Subject: [PATCH 06/10] avoid parsing jani after creating model - fix in lvalue to allow this --- .../JaniBeliefSupportMdpGenerator.cpp | 39 +++++++------------ 1 file changed, 15 insertions(+), 24 deletions(-) diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp index 127c2cdc3..be6a65f78 100644 --- a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp +++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp @@ -76,14 +76,14 @@ namespace storm { expressions::ExpressionManager& exprManager = model.getManager(); storm::expressions::Variable posProbVar = exprManager.declareRationalVariable("posProb"); model.addConstant(jani::Constant("posProb", posProbVar)); - std::map stateVariables; - jani::BoundedIntegerVariable obsVar = model.addVariable(jani::BoundedIntegerVariable("obs", exprManager.declareIntegerVariable("obs"), exprManager.integer(initialObs), exprManager.integer(0), exprManager.integer(pomdp.getNrObservations()))); - jani::BoundedIntegerVariable oldobsActVar = model.addVariable(jani::BoundedIntegerVariable("prevact", exprManager.declareIntegerVariable("prevact"), exprManager.integer(0), exprManager.integer(0), exprManager.integer(obsactpairs.size()))); + std::map stateVariables; + const jani::BoundedIntegerVariable* obsVar = &model.addVariable(jani::BoundedIntegerVariable("obs", exprManager.declareIntegerVariable("obs"), exprManager.integer(initialObs), exprManager.integer(0), exprManager.integer(pomdp.getNrObservations()))); + const jani::BoundedIntegerVariable* oldobsActVar = &model.addVariable(jani::BoundedIntegerVariable("prevact", exprManager.declareIntegerVariable("prevact"), exprManager.integer(0), exprManager.integer(0), exprManager.integer(obsactpairs.size()))); for (uint64_t i = 0; i < pomdp.getNumberOfStates(); ++i) { std::string name = "s" + std::to_string(i); bool isInitial = pomdp.getInitialStates().get(i); - stateVariables.emplace(i, model.addVariable(jani::BooleanVariable(name, exprManager.declareBooleanVariable(name), exprManager.boolean(isInitial)))); + stateVariables.emplace(i, &model.addVariable(jani::BooleanVariable(name, exprManager.declareBooleanVariable(name), exprManager.boolean(isInitial)))); } @@ -107,13 +107,13 @@ namespace storm { jani::TemplateEdgeDestination edgedest; std::vector exprVec; for (auto const& pred : predecessorInfo[i][oaps.first]) { - exprVec.push_back(stateVariables.at(pred).getExpressionVariable().getExpression()); + exprVec.push_back(stateVariables.at(pred)->getExpressionVariable().getExpression()); } if (exprVec.empty()) { - edgedest.addAssignment(jani::Assignment(stateVariables.at(i), exprManager.boolean(false))); + edgedest.addAssignment(jani::Assignment(storm::jani::LValue(*stateVariables.at(i)), exprManager.boolean(false))); } else { edgedest.addAssignment( - jani::Assignment(stateVariables.at(i), (exprManager.integer(pomdp.getObservation(i)) == obsVar.getExpressionVariable().getExpression()) && storm::expressions::disjunction(exprVec))); + jani::Assignment(storm::jani::LValue(*stateVariables.at(i)), (exprManager.integer(pomdp.getObservation(i)) == obsVar->getExpressionVariable().getExpression()) && storm::expressions::disjunction(exprVec))); } tedge->addDestination(edgedest); aut.addEdge(jani::Edge(primeloc, oaps.second, boost::none, tedge, {primeloc}, {exprManager.rational(1.0)})); @@ -126,12 +126,12 @@ namespace storm { auto const& targetVar = model.addVariable(jani::BooleanVariable("target", exprManager.declareBooleanVariable("target"), exprManager.boolean(false), true)); std::vector notTargetExpression; for (auto const& state : ~targetStates) { - notTargetExpression.push_back(!stateVariables.at(state).getExpressionVariable().getExpression()); + notTargetExpression.push_back(!stateVariables.at(state)->getExpressionVariable().getExpression()); } auto const& badVar = model.addVariable(jani::BooleanVariable("bad", exprManager.declareBooleanVariable("bad"), exprManager.boolean(false), true)); std::vector badExpression; for (auto const& state : badStates) { - badExpression.push_back(stateVariables.at(state).getExpressionVariable().getExpression()); + badExpression.push_back(stateVariables.at(state)->getExpressionVariable().getExpression()); } auto primeLocation = jani::Location("primary"); @@ -142,21 +142,21 @@ namespace storm { uint64_t secloc = obsAut.addLocation(jani::Location("secondary")); // First edges, select observation for (auto const& oaps : actionIndices) { - std::shared_ptr tedge = std::make_shared(exprManager.integer(oaps.first.observation) == obsVar.getExpressionVariable().getExpression()); + std::shared_ptr tedge = std::make_shared(exprManager.integer(oaps.first.observation) == obsVar->getExpressionVariable().getExpression()); std::vector destLocs; std::vector probs; for (auto const& obsAndPredStates : obsPredInfo[oaps.first]) { jani::TemplateEdgeDestination tedgedest; - tedgedest.addAssignment(jani::Assignment(obsVar, exprManager.integer(obsAndPredStates.first)), true); - tedgedest.addAssignment(jani::Assignment(oldobsActVar, exprManager.integer(oaps.second)), true); + tedgedest.addAssignment(jani::Assignment(jani::LValue(*obsVar), exprManager.integer(obsAndPredStates.first)), true); + tedgedest.addAssignment(jani::Assignment(jani::LValue(*oldobsActVar), exprManager.integer(oaps.second)), true); tedge->addDestination(tedgedest); destLocs.push_back(secloc); std::vector predExpressions; for (auto predstate : obsAndPredStates.second) { - predExpressions.push_back(stateVariables.at(predstate).getExpressionVariable().getExpression()); + predExpressions.push_back(stateVariables.at(predstate)->getExpressionVariable().getExpression()); } probs.push_back(storm::expressions::ite(storm::expressions::disjunction(predExpressions), posProbVar.getExpression(), exprManager.rational(0))); } @@ -165,26 +165,17 @@ namespace storm { } // Back edges for (auto const& oaps : obsactpairs) { - std::shared_ptr tedge = std::make_shared(oldobsActVar.getExpressionVariable() == exprManager.integer(actionIndices[oaps])); + std::shared_ptr tedge = std::make_shared(oldobsActVar->getExpressionVariable() == exprManager.integer(actionIndices[oaps])); jani::TemplateEdgeDestination tedgedest; - tedgedest.addAssignment(jani::Assignment(oldobsActVar, exprManager.integer(0))); + tedgedest.addAssignment(jani::Assignment(jani::LValue(*oldobsActVar), exprManager.integer(0))); tedge->addDestination(tedgedest); jani::Edge edge(secloc, actionIndices[oaps], boost::none, tedge, {primeloc}, {exprManager.rational(1.0)}); obsAut.addEdge(edge); } model.addAutomaton(obsAut); - model.setStandardSystemComposition(); - - model.finalize(); - std::ofstream ostr; - - storm::utility::openFile("beliefsupport-mdp.jani", ostr); - ostr << model; - model = storm::api::parseJaniModel("beliefsupport-mdp.jani").first; - storm::utility::closeFile(ostr); } template From 1218991e6ac6159324112f17c57510467f6c3246 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 21 Apr 2021 10:34:40 -0700 Subject: [PATCH 07/10] can switch off producing schedulers in the instantiation model checker --- .../SparseMdpInstantiationModelChecker.cpp | 23 ++++++++++++------- .../SparseMdpInstantiationModelChecker.h | 3 ++- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index eac3df86a..d92dbb157 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -15,7 +15,7 @@ namespace storm { namespace modelchecker { template - SparseMdpInstantiationModelChecker::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker(parametricModel), modelInstantiator(parametricModel) { + SparseMdpInstantiationModelChecker::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel, bool produceScheduler) : SparseInstantiationModelChecker(parametricModel), modelInstantiator(parametricModel), produceScheduler(produceScheduler) { //Intentionally left empty } @@ -40,9 +40,11 @@ namespace storm { template std::unique_ptr SparseMdpInstantiationModelChecker::checkReachabilityProbabilityFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel) { - - this->currentCheckTask->setProduceSchedulers(true); - + + if (produceScheduler) { + this->currentCheckTask->setProduceSchedulers(true); + } + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { this->currentCheckTask->setHint(std::make_shared>()); } @@ -82,16 +84,21 @@ namespace storm { // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { result = modelChecker.check(env, *this->currentCheckTask); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - hint.setSchedulerHint(dynamic_cast const&>(scheduler)); + if (produceScheduler) { + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setSchedulerHint(dynamic_cast const &>(scheduler)); + } } else { auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask); result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); + if (produceScheduler) { + storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setSchedulerHint( + std::move(dynamic_cast &>(scheduler))); + } } return result; diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h index ff6a6735e..4be0812b1 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h @@ -18,7 +18,7 @@ namespace storm { template class SparseMdpInstantiationModelChecker : public SparseInstantiationModelChecker { public: - SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel); + SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel, bool produceScheduler = true); virtual std::unique_ptr check(Environment const& env, storm::utility::parametric::Valuation const& valuation) override; @@ -29,6 +29,7 @@ namespace storm { std::unique_ptr checkBoundedUntilFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker); storm::utility::ModelInstantiator> modelInstantiator; + bool produceScheduler; }; } } From 85b676ff5704135048c53e22abe13837d4e2f304 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 25 Apr 2021 15:37:29 -0700 Subject: [PATCH 08/10] better output --- src/storm-pomdp-cli/storm-pomdp.cpp | 36 ++++++++++++------- .../analysis/IterativePolicySearch.cpp | 26 ++++++-------- .../JaniBeliefSupportMdpGenerator.cpp | 8 ++--- .../analysis/JaniBeliefSupportMdpGenerator.h | 1 + .../analysis/OneShotPolicySearch.h | 4 +-- 5 files changed, 40 insertions(+), 35 deletions(-) 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); } } From bbbe178572ec89bde03494c5ff89ab4d894b5e59 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 25 Apr 2021 21:00:06 -0700 Subject: [PATCH 09/10] Cleaning and support for linux platforms --- .../analysis/JaniBeliefSupportMdpGenerator.cpp | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp index f8501eb96..4dbce89ef 100644 --- a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp +++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp @@ -1,12 +1,12 @@ #include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h" #include "storm/storage/jani/Model.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/io/file.h" #include "storm/api/verification.h" #include "storm/api/builder.h" #include "storm-parsers/api/properties.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm-parsers/api/model_descriptions.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -84,7 +84,6 @@ namespace storm { std::string name = "s" + std::to_string(i); bool isInitial = pomdp.getInitialStates().get(i); stateVariables.emplace(i, &model.addVariable(jani::BooleanVariable(name, exprManager.declareBooleanVariable(name), exprManager.boolean(isInitial)))); - } std::map actionIndices; @@ -118,8 +117,6 @@ namespace storm { tedge->addDestination(edgedest); aut.addEdge(jani::Edge(primeloc, oaps.second, boost::none, tedge, {primeloc}, {exprManager.rational(1.0)})); } - - model.addAutomaton(aut); } jani::Automaton obsAut("obsAut", exprManager.declareIntegerVariable("obsAut")); @@ -181,10 +178,10 @@ namespace storm { template void JaniBeliefSupportMdpGenerator::verifySymbolic(bool onlyInitial) { storage::SymbolicModelDescription symdesc(model); + // This trick only works because we do not explictly check that the model is stochastic! symdesc = symdesc.preprocess("posProb=0.1"); auto property = storm::api::parsePropertiesForJaniModel("Pmax>=1 [!\"bad\" U \"target\"]", model)[0]; auto mdp = storm::api::buildSymbolicModel(symdesc, {property.getRawFormula()}); - mdp->printModelInformationToStream(std::cout); storm::Environment env; std::unique_ptr result = storm::api::verifyWithDdEngine(env, mdp, storm::api::createTask(property.getRawFormula(), onlyInitial)); std::unique_ptr filter; @@ -200,14 +197,14 @@ namespace storm { } if(result && !onlyInitial) { - auto vars = result->asSymbolicQualitativeCheckResult().getTruthValuesVector().getContainedMetaVariables(); - + auto vars = result->asSymbolicQualitativeCheckResult().getTruthValuesVector().getContainedMetaVariables(); + // TODO Export these results. } else if (result) { initialIsWinning = result->asQualitativeCheckResult().existsTrue(); } } - template + template bool JaniBeliefSupportMdpGenerator::isInitialWinning() const { return initialIsWinning; } @@ -217,8 +214,6 @@ namespace storm { template class JaniBeliefSupportMdpGenerator; template class JaniBeliefSupportMdpGenerator; - - } } } \ No newline at end of file From 58e1cc6af042de4a4f0a0dab96ef90fce8afc2ce Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 26 Apr 2021 10:01:35 -0700 Subject: [PATCH 10/10] extend prism maze example with bad state --- resources/examples/testfiles/pomdp/maze2.prism | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/examples/testfiles/pomdp/maze2.prism b/resources/examples/testfiles/pomdp/maze2.prism index e1f60ae07..19771c972 100644 --- a/resources/examples/testfiles/pomdp/maze2.prism +++ b/resources/examples/testfiles/pomdp/maze2.prism @@ -135,5 +135,5 @@ endrewards // target observation label "goal" = o=7; - +label "bad" = o=6;