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