From 5c748254a664acc243a1e32de8dfa28661254fd8 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 17 Mar 2020 09:22:19 +0100 Subject: [PATCH] Cleaning up the POMDP CLI code a bit. Now supports switching to exact arithmetic with the --exact switch. --- .../settings/PomdpSettings.cpp | 67 ++ src/storm-pomdp-cli/settings/PomdpSettings.h | 13 + src/storm-pomdp-cli/storm-pomdp.cpp | 739 +++++++++--------- 3 files changed, 435 insertions(+), 384 deletions(-) create mode 100644 src/storm-pomdp-cli/settings/PomdpSettings.cpp create mode 100644 src/storm-pomdp-cli/settings/PomdpSettings.h diff --git a/src/storm-pomdp-cli/settings/PomdpSettings.cpp b/src/storm-pomdp-cli/settings/PomdpSettings.cpp new file mode 100644 index 000000000..f08dbe932 --- /dev/null +++ b/src/storm-pomdp-cli/settings/PomdpSettings.cpp @@ -0,0 +1,67 @@ +#include "storm-pomdp-cli/settings/PomdpSettings.h" + +#include "storm/settings/SettingsManager.h" + +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/CuddSettings.h" +#include "storm/settings/modules/SylvanSettings.h" +#include "storm/settings/modules/EigenEquationSolverSettings.h" +#include "storm/settings/modules/GmmxxEquationSolverSettings.h" +#include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/MinMaxEquationSolverSettings.h" +#include "storm/settings/modules/GameSolverSettings.h" +#include "storm/settings/modules/BisimulationSettings.h" +#include "storm/settings/modules/GlpkSettings.h" +#include "storm/settings/modules/GurobiSettings.h" +#include "storm/settings/modules/Smt2SmtSolverSettings.h" +#include "storm/settings/modules/ExplorationSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/AbstractionSettings.h" +#include "storm/settings/modules/BuildSettings.h" +#include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/TopologicalEquationSolverSettings.h" +#include "storm/settings/modules/ModelCheckerSettings.h" +#include "storm/settings/modules/MultiplierSettings.h" +#include "storm/settings/modules/TransformationSettings.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/settings/modules/HintSettings.h" + +#include "storm-pomdp-cli/settings/modules/POMDPSettings.h" + +namespace storm { + namespace settings { + void initializePomdpSettings(std::string const& name, std::string const& executableName) { + storm::settings::mutableManager().setName(name, executableName); + + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + + storm::settings::addModule(); + + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + 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/PomdpSettings.h b/src/storm-pomdp-cli/settings/PomdpSettings.h new file mode 100644 index 000000000..f3788c598 --- /dev/null +++ b/src/storm-pomdp-cli/settings/PomdpSettings.h @@ -0,0 +1,13 @@ +#pragma once + +#include + +namespace storm { + namespace settings { + /*! + * Initialize the settings manager. + */ + void initializePomdpSettings(std::string const& name, std::string const& executableName); + + } +} \ No newline at end of file diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 5420e9b75..6aae4d493 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -3,35 +3,10 @@ #include "storm/utility/initialize.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/CuddSettings.h" -#include "storm/settings/modules/SylvanSettings.h" -#include "storm/settings/modules/EigenEquationSolverSettings.h" -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/settings/modules/EliminationSettings.h" -#include "storm/settings/modules/MinMaxEquationSolverSettings.h" -#include "storm/settings/modules/GameSolverSettings.h" -#include "storm/settings/modules/BisimulationSettings.h" -#include "storm/settings/modules/GlpkSettings.h" -#include "storm/settings/modules/GurobiSettings.h" -#include "storm/settings/modules/Smt2SmtSolverSettings.h" -#include "storm/settings/modules/ExplorationSettings.h" -#include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/AbstractionSettings.h" -#include "storm/settings/modules/BuildSettings.h" -#include "storm/settings/modules/JitBuilderSettings.h" -#include "storm/settings/modules/TopologicalEquationSolverSettings.h" -#include "storm/settings/modules/ModelCheckerSettings.h" -#include "storm/settings/modules/MultiplierSettings.h" - -#include "storm/settings/modules/TransformationSettings.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" - -#include "storm/settings/modules/HintSettings.h" #include "storm-pomdp-cli/settings/modules/POMDPSettings.h" +#include "storm-pomdp-cli/settings/PomdpSettings.h" + #include "storm/analysis/GraphConditions.h" #include "storm-cli-utilities/cli.h" @@ -51,129 +26,370 @@ #include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" #include "storm/api/storm.h" -#include - -/*! - * Initialize the settings manager. - */ -void initializeSettings() { - storm::settings::mutableManager().setName("Storm-POMDP", "storm-pomdp"); - - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - - storm::settings::addModule(); +#include "storm/exceptions/UnexpectedException.h" - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); -} +#include -template -bool extractTargetAndSinkObservationSets(std::shared_ptr> const& pomdp, storm::logic::Formula const& subformula, std::set& targetObservationSet, storm::storage::BitVector& targetStates, storm::storage::BitVector& badStates) { - //TODO refactor (use model checker to determine the states, then transform into observations). - //TODO rename into appropriate function name. - 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)); - targetStates.set(state); +namespace storm { + namespace pomdp { + namespace cli { + + + template + bool extractTargetAndSinkObservationSets(std::shared_ptr> const& pomdp, storm::logic::Formula const& subformula, std::set& targetObservationSet, storm::storage::BitVector& targetStates, storm::storage::BitVector& badStates) { + //TODO refactor (use model checker to determine the states, then transform into observations). + //TODO rename into appropriate function name. + 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)); + targetStates.set(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)); + targetStates.set(state); + } + } + } + } else if (subformula.isUntilFormula()) { + storm::logic::UntilFormula const &untilFormula = subformula.asUntilFormula(); + storm::logic::Formula const &subformula1 = untilFormula.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 = untilFormula.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)); + targetStates.set(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)); + targetStates.set(state); + } + + } + } } + return validFormula; } - } 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)); - targetStates.set(state); + + template + void processOptionsWithValueTypeAndDdLib(storm::cli::SymbolicInput const& symbolicInput, storm::cli::ModelProcessingInformation const& mpi) { + auto const& pomdpSettings = storm::settings::getModule(); + + auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, mpi); + STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp && model->isSparseModel(), storm::exceptions::WrongFormatException, "Expected a POMDP in sparse representation."); + + std::shared_ptr> pomdp = model->template as>(); + storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); + pomdp = makeCanonic.transform(); + + std::shared_ptr formula; + if (!symbolicInput.properties.empty()) { + formula = symbolicInput.properties.front().getRawFormula(); + STORM_PRINT_AND_LOG("Analyzing property '" << *formula << "'" << std::endl); + STORM_LOG_WARN_COND(symbolicInput.properties.size() == 1, "There is currently no support for multiple properties. All other properties will be ignored."); } - } - } - } else if (subformula.isUntilFormula()) { - storm::logic::UntilFormula const &untilFormula = subformula.asUntilFormula(); - storm::logic::Formula const &subformula1 = untilFormula.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); + + if (pomdpSettings.isAnalyzeUniqueObservationsSet()) { + STORM_PRINT_AND_LOG("Analyzing states with unique observation ..." << std::endl); + storm::analysis::UniqueObservationStates uniqueAnalysis(*pomdp); + std::cout << uniqueAnalysis.analyse() << std::endl; } - } - } 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); + + if (formula) { + if (formula->isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula(); + storm::logic::Formula const &subformula1 = probFormula.getSubformula(); + std::set targetObservationSet; + storm::storage::BitVector targetStates(pomdp->getNumberOfStates()); + storm::storage::BitVector badStates(pomdp->getNumberOfStates()); + + bool validFormula = extractTargetAndSinkObservationSets(pomdp, subformula1, targetObservationSet, targetStates, badStates); + 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())) { + STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); + uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); + storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); + pomdp = selfLoopEliminator.transform(); + STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); + } + if (pomdpSettings.isQualitativeReductionSet()) { + storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); + STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); + prob0States = qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()); + std::cout << *prob0States << std::endl; + STORM_PRINT_AND_LOG(" done." << std::endl); + STORM_PRINT_AND_LOG("Computing states with probability 1 ..."); + prob1States = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()); + std::cout << *prob1States << std::endl; + STORM_PRINT_AND_LOG(" done." << std::endl); + //std::cout << "actual reduction not yet implemented..." << std::endl; + storm::pomdp::transformer::KnownProbabilityTransformer kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); + pomdp = kpt.transform(*pomdp, *prob0States, *prob1States); + } + if (pomdpSettings.isGridApproximationSet()) { + + storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); + auto overRes = storm::utility::one(); + auto underRes = storm::utility::zero(); + std::unique_ptr> result; + + result = checker.refineReachabilityProbability(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, + pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold()); + //result = checker.computeReachabilityProbabilityOTF(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold()); + overRes = result->overApproxValue; + underRes = result->underApproxValue; + if (overRes != underRes) { + STORM_PRINT("Overapproximation Result: " << overRes << std::endl) + STORM_PRINT("Underapproximation Result: " << underRes << std::endl) + } else { + STORM_PRINT("Result: " << overRes << std::endl) + } + } + if (pomdpSettings.isMemlessSearchSet()) { + // std::cout << std::endl; + // pomdp->writeDotToStream(std::cout); + // std::cout << std::endl; + // std::cout << std::endl; + storm::expressions::ExpressionManager expressionManager; + std::shared_ptr smtSolverFactory = std::make_shared(); + if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") { + storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); + memlessSearch.findNewStrategyForSomeState(5); + } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { + storm::pomdp::MemlessStrategySearchQualitative memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); + memlessSearch.findNewStrategyForSomeState(5); + } else { + STORM_LOG_ERROR("This method is not implemented."); + } + + + } + } else if (formula->isRewardOperatorFormula()) { + if (pomdpSettings.isSelfloopReductionSet() && storm::solver::minimize(formula->asRewardOperatorFormula().getOptimalityType())) { + STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); + uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); + storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); + pomdp = selfLoopEliminator.transform(); + STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); + } + if (pomdpSettings.isGridApproximationSet()) { + std::string rewardModelName; + storm::logic::RewardOperatorFormula const &rewFormula = formula->asRewardOperatorFormula(); + if (rewFormula.hasRewardModelName()) { + rewardModelName = rewFormula.getRewardModelName(); + } + storm::logic::Formula const &subformula1 = rewFormula.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(); + auto overRes = storm::utility::one(); + auto underRes = storm::utility::zero(); + std::unique_ptr> result; + result = checker.computeReachabilityReward(*pomdp, targetObservationSet, + rewFormula.getOptimalityType() == + storm::OptimizationDirection::Minimize, + pomdpSettings.getGridResolution()); + overRes = result->overApproxValue; + underRes = result->underApproxValue; + } + + } + if (pomdpSettings.getMemoryBound() > 1) { + STORM_PRINT_AND_LOG("Computing the unfolding for memory bound " << pomdpSettings.getMemoryBound() << " and memory pattern '" << storm::storage::toString(pomdpSettings.getMemoryPattern()) << "' ..."); + storm::storage::PomdpMemory memory = storm::storage::PomdpMemoryBuilder().build(pomdpSettings.getMemoryPattern(), pomdpSettings.getMemoryBound()); + std::cout << memory.toString() << std::endl; + storm::transformer::PomdpMemoryUnfolder memoryUnfolder(*pomdp, memory); + pomdp = memoryUnfolder.transform(); + STORM_PRINT_AND_LOG(" done." << std::endl); + pomdp->printModelInformationToStream(std::cout); + } else { + STORM_PRINT_AND_LOG("Assumming memoryless schedulers." << std::endl;) + } + + // From now on the pomdp is considered memoryless + + if (pomdpSettings.isMecReductionSet()) { + STORM_PRINT_AND_LOG("Eliminating mec choices ..."); + // Note: Elimination of mec choices only preserves memoryless schedulers. + uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); + storm::transformer::GlobalPomdpMecChoiceEliminator mecChoiceEliminator(*pomdp); + pomdp = mecChoiceEliminator.transform(*formula); + STORM_PRINT_AND_LOG(" done." << std::endl); + STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl); + pomdp->printModelInformationToStream(std::cout); + } + + if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) { + if (pomdpSettings.isTransformSimpleSet()) { + STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP."); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, true); + } else { + STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP."); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); + } + pomdp->printModelInformationToStream(std::cout); + STORM_PRINT_AND_LOG(" done." << std::endl); + } + + + if (pomdpSettings.isExportToParametricSet()) { + STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC..."); + storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*pomdp); + std::string transformMode = pomdpSettings.getFscApplicationTypeString(); + auto pmc = toPMCTransformer.transform(storm::transformer::parsePomdpFscApplicationMode(transformMode)); + STORM_PRINT_AND_LOG(" done." << std::endl); + pmc->printModelInformationToStream(std::cout); + STORM_PRINT_AND_LOG("Simplifying pMC..."); + //if (generalSettings.isBisimulationSet()) { + pmc = storm::api::performBisimulationMinimization(pmc->template as>(),{formula}, storm::storage::BisimulationType::Strong)->template as>(); + + //} + STORM_PRINT_AND_LOG(" done." << std::endl); + pmc->printModelInformationToStream(std::cout); + STORM_PRINT_AND_LOG("Exporting pMC..."); + storm::analysis::ConstraintCollector constraints(*pmc); + auto const& parameterSet = constraints.getVariables(); + std::vector parameters(parameterSet.begin(), parameterSet.end()); + std::vector parameterNames; + for (auto const& parameter : parameters) { + parameterNames.push_back(parameter.name()); + } + storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames); + STORM_PRINT_AND_LOG(" done." << std::endl); + } + + } else { + STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?"); } + } - } else { - return false; - } - storm::logic::Formula const &subformula2 = untilFormula.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)); - targetStates.set(state); + + template + void processOptionsWithDdLib(storm::cli::SymbolicInput const& symbolicInput, storm::cli::ModelProcessingInformation const& mpi) { + switch (mpi.buildValueType) { + case storm::cli::ModelProcessingInformation::ValueType::FinitePrecision: + processOptionsWithValueTypeAndDdLib(symbolicInput, mpi); + break; + case storm::cli::ModelProcessingInformation::ValueType::Exact: + STORM_LOG_THROW(DdType == storm::dd::DdType::Sylvan, storm::exceptions::UnexpectedException, "Exact arithmetic is only supported with Dd library Sylvan."); + processOptionsWithValueTypeAndDdLib(symbolicInput, mpi); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected ValueType for model building."); } - } - } 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)); - targetStates.set(state); + + void processOptions() { + auto symbolicInput = storm::cli::parseSymbolicInput(); + storm::cli::ModelProcessingInformation mpi; + std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput); + switch (mpi.ddType) { + case storm::dd::DdType::CUDD: + processOptionsWithDdLib(symbolicInput, mpi); + break; + case storm::dd::DdType::Sylvan: + processOptionsWithDdLib(symbolicInput, mpi); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Dd Type."); } - } } } - return validFormula; } /*! @@ -187,7 +403,7 @@ int main(const int argc, const char** argv) { //try { storm::utility::setUp(); storm::cli::printHeader("Storm-pomdp", argc, argv); - initializeSettings(); + storm::settings::initializePomdpSettings("Storm-POMDP", "storm-pomdp"); bool optionsCorrect = storm::cli::parseOptions(argc, argv); if (!optionsCorrect) { @@ -195,253 +411,8 @@ int main(const int argc, const char** argv) { } storm::cli::setUrgentOptions(); - typedef double VT; - - auto const& pomdpSettings = storm::settings::getModule(); - auto const &general = storm::settings::getModule(); - auto const &debug = storm::settings::getModule(); - - - if (general.isVerboseSet()) { - storm::utility::setLogLevel(l3pp::LogLevel::INFO); - } - if (debug.isDebugSet()) { - storm::utility::setLogLevel(l3pp::LogLevel::DEBUG); - } - if (debug.isTraceSet()) { - storm::utility::setLogLevel(l3pp::LogLevel::TRACE); - } - - auto symbolicInput = storm::cli::parseSymbolicInput(); - storm::cli::ModelProcessingInformation mpi; - std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput); - - // We should not export here if we are going to do some processing first. - auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, mpi); - STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP."); - - std::shared_ptr> pomdp = model->template as>(); - storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); - pomdp = makeCanonic.transform(); - - std::shared_ptr formula; - if (!symbolicInput.properties.empty()) { - formula = symbolicInput.properties.front().getRawFormula(); - STORM_PRINT_AND_LOG("Analyzing property '" << *formula << "'" << std::endl); - STORM_LOG_WARN_COND(symbolicInput.properties.size() == 1, "There is currently no support for multiple properties. All other properties will be ignored."); - } - - if (pomdpSettings.isAnalyzeUniqueObservationsSet()) { - STORM_PRINT_AND_LOG("Analyzing states with unique observation ..." << std::endl); - storm::analysis::UniqueObservationStates uniqueAnalysis(*pomdp); - std::cout << uniqueAnalysis.analyse() << std::endl; - } - - if (formula) { - if (formula->isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula(); - storm::logic::Formula const &subformula1 = probFormula.getSubformula(); - std::set targetObservationSet; - storm::storage::BitVector targetStates(pomdp->getNumberOfStates()); - storm::storage::BitVector badStates(pomdp->getNumberOfStates()); - - bool validFormula = extractTargetAndSinkObservationSets(pomdp, subformula1, targetObservationSet, targetStates, badStates); - 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())) { - STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); - uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); - storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); - pomdp = selfLoopEliminator.transform(); - STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); - } - if (pomdpSettings.isQualitativeReductionSet()) { - storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); - STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); - prob0States = qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()); - std::cout << *prob0States << std::endl; - STORM_PRINT_AND_LOG(" done." << std::endl); - STORM_PRINT_AND_LOG("Computing states with probability 1 ..."); - prob1States = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()); - std::cout << *prob1States << std::endl; - STORM_PRINT_AND_LOG(" done." << std::endl); - //std::cout << "actual reduction not yet implemented..." << std::endl; - storm::pomdp::transformer::KnownProbabilityTransformer kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); - pomdp = kpt.transform(*pomdp, *prob0States, *prob1States); - } - if (pomdpSettings.isGridApproximationSet()) { - - storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - auto overRes = storm::utility::one(); - auto underRes = storm::utility::zero(); - std::unique_ptr> result; - - result = checker.refineReachabilityProbability(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, - pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold()); - //result = checker.computeReachabilityProbabilityOTF(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold()); - overRes = result->overApproxValue; - underRes = result->underApproxValue; - if (overRes != underRes) { - STORM_PRINT("Overapproximation Result: " << overRes << std::endl) - STORM_PRINT("Underapproximation Result: " << underRes << std::endl) - } else { - STORM_PRINT("Result: " << overRes << std::endl) - } - } - if (pomdpSettings.isMemlessSearchSet()) { -// std::cout << std::endl; -// pomdp->writeDotToStream(std::cout); -// std::cout << std::endl; -// std::cout << std::endl; - storm::expressions::ExpressionManager expressionManager; - std::shared_ptr smtSolverFactory = std::make_shared(); - if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") { - storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); - memlessSearch.findNewStrategyForSomeState(5); - } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::MemlessStrategySearchQualitative memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); - memlessSearch.findNewStrategyForSomeState(5); - } else { - STORM_LOG_ERROR("This method is not implemented."); - } - - - } - } else if (formula->isRewardOperatorFormula()) { - if (pomdpSettings.isSelfloopReductionSet() && storm::solver::minimize(formula->asRewardOperatorFormula().getOptimalityType())) { - STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); - uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); - storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); - pomdp = selfLoopEliminator.transform(); - STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); - } - if (pomdpSettings.isGridApproximationSet()) { - std::string rewardModelName; - storm::logic::RewardOperatorFormula const &rewFormula = formula->asRewardOperatorFormula(); - if (rewFormula.hasRewardModelName()) { - rewardModelName = rewFormula.getRewardModelName(); - } - storm::logic::Formula const &subformula1 = rewFormula.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(); - auto overRes = storm::utility::one(); - auto underRes = storm::utility::zero(); - std::unique_ptr> result; - result = checker.computeReachabilityReward(*pomdp, targetObservationSet, - rewFormula.getOptimalityType() == - storm::OptimizationDirection::Minimize, - pomdpSettings.getGridResolution()); - overRes = result->overApproxValue; - underRes = result->underApproxValue; - } - - } - if (pomdpSettings.getMemoryBound() > 1) { - STORM_PRINT_AND_LOG("Computing the unfolding for memory bound " << pomdpSettings.getMemoryBound() << " and memory pattern '" << storm::storage::toString(pomdpSettings.getMemoryPattern()) << "' ..."); - storm::storage::PomdpMemory memory = storm::storage::PomdpMemoryBuilder().build(pomdpSettings.getMemoryPattern(), pomdpSettings.getMemoryBound()); - std::cout << memory.toString() << std::endl; - storm::transformer::PomdpMemoryUnfolder memoryUnfolder(*pomdp, memory); - pomdp = memoryUnfolder.transform(); - STORM_PRINT_AND_LOG(" done." << std::endl); - pomdp->printModelInformationToStream(std::cout); - } else { - STORM_PRINT_AND_LOG("Assumming memoryless schedulers." << std::endl;) - } - - // From now on the pomdp is considered memoryless - - if (pomdpSettings.isMecReductionSet()) { - STORM_PRINT_AND_LOG("Eliminating mec choices ..."); - // Note: Elimination of mec choices only preserves memoryless schedulers. - uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); - storm::transformer::GlobalPomdpMecChoiceEliminator mecChoiceEliminator(*pomdp); - pomdp = mecChoiceEliminator.transform(*formula); - STORM_PRINT_AND_LOG(" done." << std::endl); - STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl); - pomdp->printModelInformationToStream(std::cout); - } - - if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) { - if (pomdpSettings.isTransformSimpleSet()) { - STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP."); - pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, true); - } else { - STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP."); - pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); - } - pomdp->printModelInformationToStream(std::cout); - STORM_PRINT_AND_LOG(" done." << std::endl); - } - - - if (pomdpSettings.isExportToParametricSet()) { - STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC..."); - storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*pomdp); - std::string transformMode = pomdpSettings.getFscApplicationTypeString(); - auto pmc = toPMCTransformer.transform(storm::transformer::parsePomdpFscApplicationMode(transformMode)); - STORM_PRINT_AND_LOG(" done." << std::endl); - pmc->printModelInformationToStream(std::cout); - STORM_PRINT_AND_LOG("Simplifying pMC..."); - //if (generalSettings.isBisimulationSet()) { - pmc = storm::api::performBisimulationMinimization(pmc->as>(),{formula}, storm::storage::BisimulationType::Strong)->as>(); - - //} - STORM_PRINT_AND_LOG(" done." << std::endl); - pmc->printModelInformationToStream(std::cout); - STORM_PRINT_AND_LOG("Exporting pMC..."); - storm::analysis::ConstraintCollector constraints(*pmc); - auto const& parameterSet = constraints.getVariables(); - std::vector parameters(parameterSet.begin(), parameterSet.end()); - std::vector parameterNames; - for (auto const& parameter : parameters) { - parameterNames.push_back(parameter.name()); - } - storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames); - STORM_PRINT_AND_LOG(" done." << std::endl); - } - - } else { - STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?"); - } + // Invoke storm-pomdp with obtained settings + storm::pomdp::cli::processOptions(); // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp();