From 77c63f4c128e19caaaf93ba5660d79ad94d732cd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 29 Nov 2019 18:17:24 +0100 Subject: [PATCH] SAT based zerostate analysis: work in progress --- .../settings/modules/POMDPSettings.cpp | 8 +- .../settings/modules/POMDPSettings.h | 1 + src/storm-pomdp-cli/storm-pomdp.cpp | 162 +++++++++++++----- .../MemlessStrategySearchQualitative.cpp | 114 ++++++++++++ 4 files changed, 238 insertions(+), 47 deletions(-) create mode 100644 src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index 617cebf36..2a637d436 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -26,6 +26,7 @@ namespace storm { std::vector fscModes = {"standard", "simple-linear", "simple-linear-inverse"}; const std::string transformBinaryOption = "transformbinary"; const std::string transformSimpleOption = "transformsimple"; + const std::string memlessSearchOption = "memlesssearch"; POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportAsParametricModelOption, false, "Export the parametric file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which to write the model.").build()).build()); @@ -45,6 +46,7 @@ namespace storm { 10).addValidatorUnsignedInteger( storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator( 0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, memlessSearchOption, false, "Search for a qualitative memoryless scheuler").build()); } bool POMDPSettings::isExportToParametricSet() const { @@ -79,7 +81,11 @@ namespace storm { return this->getOption(gridApproximationOption).getArgumentByName( "resolution").getValueAsUnsignedInteger(); } - + + bool POMDPSettings::isMemlessSearchSet() const { + return this->getOption(memlessSearchOption).getHasOptionBeenSet(); + } + uint64_t POMDPSettings::getMemoryBound() const { return this->getOption(memoryBoundOption).getArgumentByName("bound").getValueAsUnsignedInteger(); } diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h index 1e68871e8..9f7332774 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h @@ -32,6 +32,7 @@ namespace storm { bool isSelfloopReductionSet() const; bool isTransformSimpleSet() const; bool isTransformBinarySet() const; + bool isMemlessSearchSet() const; std::string getFscApplicationTypeString() const; uint64_t getMemoryBound() const; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 0af965ddd..3927d0728 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -43,6 +43,7 @@ #include "storm-pomdp/analysis/UniqueObservationStates.h" #include "storm-pomdp/analysis/QualitativeAnalysis.h" #include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h" +#include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h" #include "storm/api/storm.h" #include @@ -77,6 +78,91 @@ void initializeSettings() { storm::settings::addModule(); } +template +bool extractTargetAndSinkObservationSets(std::shared_ptr> const& pomdp, storm::logic::Formula const& subformula, std::set& targetObservationSet, storm::storage::BitVector& badStates) { + //TODO refactor (use model checker to determine the states, then transform into observations). + + bool validFormula = false; + if (subformula.isEventuallyFormula()) { + storm::logic::EventuallyFormula const &eventuallyFormula = subformula.asEventuallyFormula(); + storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula(); + if (subformula2.isAtomicLabelFormula()) { + storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula(); + validFormula = true; + std::string targetLabel = alFormula.getLabel(); + auto labeling = pomdp->getStateLabeling(); + for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { + if (labeling.getStateHasLabel(targetLabel, state)) { + targetObservationSet.insert(pomdp->getObservation(state)); + } + } + } else if (subformula2.isAtomicExpressionFormula()) { + validFormula = true; + std::stringstream stream; + stream << subformula2.asAtomicExpressionFormula().getExpression(); + storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str()); + std::string targetLabel = formula3.getLabel(); + auto labeling = pomdp->getStateLabeling(); + for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { + if (labeling.getStateHasLabel(targetLabel, state)) { + targetObservationSet.insert(pomdp->getObservation(state)); + } + } + } + } else if (subformula.isUntilFormula()) { + storm::logic::UntilFormula const &eventuallyFormula = subformula.asUntilFormula(); + storm::logic::Formula const &subformula1 = eventuallyFormula.getLeftSubformula(); + if (subformula1.isAtomicLabelFormula()) { + storm::logic::AtomicLabelFormula const &alFormula = subformula1.asAtomicLabelFormula(); + std::string targetLabel = alFormula.getLabel(); + auto labeling = pomdp->getStateLabeling(); + for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { + if (labeling.getStateHasLabel(targetLabel, state)) { + badStates.set(state); + } + } + } else if (subformula1.isAtomicExpressionFormula()) { + std::stringstream stream; + stream << subformula1.asAtomicExpressionFormula().getExpression(); + storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str()); + std::string targetLabel = formula3.getLabel(); + auto labeling = pomdp->getStateLabeling(); + for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { + if (labeling.getStateHasLabel(targetLabel, state)) { + badStates.set(state); + } + } + } else { + return false; + } + storm::logic::Formula const &subformula2 = eventuallyFormula.getRightSubformula(); + if (subformula2.isAtomicLabelFormula()) { + storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula(); + validFormula = true; + std::string targetLabel = alFormula.getLabel(); + auto labeling = pomdp->getStateLabeling(); + for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { + if (labeling.getStateHasLabel(targetLabel, state)) { + targetObservationSet.insert(pomdp->getObservation(state)); + } + } + } else if (subformula2.isAtomicExpressionFormula()) { + validFormula = true; + std::stringstream stream; + stream << subformula2.asAtomicExpressionFormula().getExpression(); + storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str()); + std::string targetLabel = formula3.getLabel(); + auto labeling = pomdp->getStateLabeling(); + for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { + if (labeling.getStateHasLabel(targetLabel, state)) { + targetObservationSet.insert(pomdp->getObservation(state)); + } + } + } + } + return validFormula; +} + /*! * Entry point for the pomdp backend. * @@ -85,7 +171,7 @@ void initializeSettings() { * @return Return code, 0 if successfull, not 0 otherwise. */ int main(const int argc, const char** argv) { - try { + //try { storm::utility::setUp(); storm::cli::printHeader("Storm-pomdp", argc, argv); initializeSettings(); @@ -134,7 +220,21 @@ int main(const int argc, const char** argv) { } if (formula) { + storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula(); + storm::logic::Formula const &subformula1 = probFormula.getSubformula(); + + if (formula->isProbabilityOperatorFormula()) { + + std::set targetObservationSet; + std::set badObservationSet; + + bool validFormula = extractTargetAndSinkObservationSets(pomdp, subformula1, targetObservationSet, badObservationSet); + STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException, + "The formula is not supported by the grid approximation"); + STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!"); + + boost::optional prob1States; boost::optional prob0States; if (pomdpSettings.isSelfloopReductionSet() && !storm::solver::minimize(formula->asProbabilityOperatorFormula().getOptimalityType())) { @@ -159,42 +259,6 @@ int main(const int argc, const char** argv) { pomdp = kpt.transform(*pomdp, *prob0States, *prob1States); } if (pomdpSettings.isGridApproximationSet()) { - storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula(); - storm::logic::Formula const &subformula1 = probFormula.getSubformula(); - - std::set targetObservationSet; - //TODO refactor - bool validFormula = false; - if (subformula1.isEventuallyFormula()) { - storm::logic::EventuallyFormula const &eventuallyFormula = subformula1.asEventuallyFormula(); - storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula(); - if (subformula2.isAtomicLabelFormula()) { - storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula(); - validFormula = true; - std::string targetLabel = alFormula.getLabel(); - auto labeling = pomdp->getStateLabeling(); - for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { - if (labeling.getStateHasLabel(targetLabel, state)) { - targetObservationSet.insert(pomdp->getObservation(state)); - } - } - } else if (subformula2.isAtomicExpressionFormula()) { - validFormula = true; - std::stringstream stream; - stream << subformula2.asAtomicExpressionFormula().getExpression(); - storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str()); - std::string targetLabel = formula3.getLabel(); - auto labeling = pomdp->getStateLabeling(); - for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) { - if (labeling.getStateHasLabel(targetLabel, state)) { - targetObservationSet.insert(pomdp->getObservation(state)); - } - } - } - } - STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException, - "The formula is not supported by the grid approximation"); - STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!"); storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); double overRes = storm::utility::one(); @@ -213,6 +277,14 @@ int main(const int argc, const char** argv) { STORM_PRINT("Result: " << overRes << std::endl) } } + if (pomdpSettings.isMemlessSearchSet()) { + storm::expressions::ExpressionManager expressionManager; + std::shared_ptr smtSolverFactory = std::make_shared(); + + storm::pomdp::MemlessStrategySearchQualitative memlessSearch(*pomdp, targetObservationSet, smtSolverFactory); + memlessSearch.analyze(5); + + } } else if (formula->isRewardOperatorFormula()) { if (pomdpSettings.isSelfloopReductionSet() && storm::solver::minimize(formula->asRewardOperatorFormula().getOptimalityType())) { STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); @@ -344,16 +416,14 @@ int main(const int argc, const char** argv) { STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?"); } - - // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); return 0; - } catch (storm::exceptions::BaseException const &exception) { - STORM_LOG_ERROR("An exception caused Storm-pomdp to terminate. The message of the exception is: " << exception.what()); - return 1; - } catch (std::exception const &exception) { - STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pomdp to terminate. The message of this exception is: " << exception.what()); - return 2; - } + // } catch (storm::exceptions::BaseException const &exception) { + // STORM_LOG_ERROR("An exception caused Storm-pomdp to terminate. The message of the exception is: " << exception.what()); + // return 1; + //} catch (std::exception const &exception) { + // STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pomdp to terminate. The message of this exception is: " << exception.what()); + // return 2; + //} } diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp new file mode 100644 index 000000000..0c46fd0d3 --- /dev/null +++ b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp @@ -0,0 +1,114 @@ +#include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h" + + +namespace storm { + namespace pomdp { + + template + void MemlessStrategySearchQualitative::initialize(uint64_t k) { + if (maxK == -1) { + // not initialized at all. + + // Create some data structures. + for(uint64_t obs = 0; obs < pomdp.getNrObservations(); ++obs) { + actionSelectionVars.push_back(std::vector()); + statesPerObservation.push_back(std::vector()); // Consider using bitvectors instead. + } + + // Fill the states-per-observation mapping, + // declare the reachability variables, + // declare the path variables. + uint64_t stateId = 0; + for(auto obs : pomdp.getObservations()) { + pathVars.push_back(std::vector()); + for (uint64_t i = 0; i < k; ++i) { + pathVars.back().push_back(expressionManager->declareBooleanVariable("P-"+std::to_string(stateId)+"-"+std::to_string(i)).getExpression()); + } + reachVars.push_back(expressionManager->declareBooleanVariable("C-" + std::to_string(stateId)).getExpression()); + + statesPerObservation.at(obs).push_back(stateId++); + + } + assert(pathVars.size() == pomdp.getNumberOfStates()); + + // Create the action selection variables. + uint64_t obs = 0; + for(auto const& statesForObservation : statesPerObservation) { + for (uint64_t a = 0; a < pomdp.getNumberOfChoices(statesForObservation.front()); ++a) { + std::string varName = "A-" + std::to_string(obs) + "-" + std::to_string(a); + actionSelectionVars.at(obs).push_back(expressionManager->declareBooleanVariable(varName).getExpression()); + } + ++obs; + } + + + } else { + + assert(false); + + } + + uint64_t rowindex = 0; + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + std::vector> pathsubsubexprs; + for (uint64_t j = 1; j < k; ++j) { + pathsubsubexprs.push_back(std::vector()); + } + + if (targetObservations.count(pomdp.getObservation(state)) > 0) { + smtSolver->add(pathVars[state][0]); + } else { + smtSolver->add(!pathVars[state][0]); + } + + if (surelyReachSinkStates.at(state)) { + smtSolver->add(!reachVars[state]); + } + else { + for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) { + std::vector subexprreach; + + subexprreach.push_back(!reachVars.at(state)); + subexprreach.push_back(!actionSelectionVars.at(pomdp.getObservation(state)).at(action)); + for (auto const &entries : pomdp.getTransitionMatrix().getRow(rowindex)) { + subexprreach.push_back(reachVars.at(entries.getColumn())); + } + smtSolver->add(storm::expressions::disjunction(subexprreach)); + for (auto const &entries : pomdp.getTransitionMatrix().getRow(rowindex)) { + for (uint64_t j = 1; j < k; ++j) { + pathsubsubexprs[j - 1].push_back(pathVars[entries.getColumn()][j - 1]); + } + } + rowindex++; + } + smtSolver->add(storm::expressions::implies(reachVars.at(state), pathVars.at(state).back())); + + + for (uint64_t j = 1; j < k; ++j) { + std::vector pathsubexprs; + + for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) { + pathsubexprs.push_back(actionSelectionVars.at(pomdp.getObservation(state)).at(action) && storm::expressions::disjunction(pathsubsubexprs[j - 1])); + } + smtSolver->add(storm::expressions::iff(pathVars[state][j], storm::expressions::disjunction(pathsubexprs))); + } + } + + } + + for (auto const& actionVars : actionSelectionVars) { + smtSolver->add(storm::expressions::disjunction(actionVars)); + } + + + + + //for (auto const& ) + + } + + + + template class MemlessStrategySearchQualitative; + } +}