Revised POMDP belief exploration

resources/examples/testfiles/pomdp/simple.prism

@@ -11,6 +11,7 @@ module main
     [alpha] s>0 & s<5 -> (1-slippery): (s'=s+2) + slippery: true;
     [beta]  s=3 -> (1-slippery): (s'=6)   + slippery: true;
     [beta]  s=4 -> (1-slippery): (s'=5) + slippery: true;
+    [alpha]  s=5 | s=6 -> 1: true;
 endmodule
 
 rewards

resources/examples/testfiles/pomdp/simple_unit_rewards.prism

@@ -0,0 +1,22 @@
+pomdp
+
+observable "start" = s<3;
+observable "end" = s>4;
+
+const double slippery;
+
+module main
+    s : [0..6] init 0;
+    [alpha] s=0 -> (1-slippery) * 0.7: (s'=1) + (1-slippery) * 0.3: (s'=2) + slippery: true;
+    [alpha] s>0 & s<5 -> (1-slippery): (s'=s+2) + slippery: true;
+    [beta]  s=3 -> (1-slippery): (s'=6) + slippery: true;
+    [beta]  s=4 -> (1-slippery): (s'=5) + slippery: true;
+    [alpha] s=5 | s=6 -> 1: true;
+endmodule
+
+rewards
+    [alpha] true : 1;
+    [beta] true : 1;
+endrewards
+
+label "goal" = s=5;

src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h

@@ -1,24 +1,8 @@
 #pragma once
 
-#include "storm-config.h"
 #include "storm/settings/modules/ModuleSettings.h"
 
-namespace storm {
-namespace builder {
-template<typename PomdpType, typename BeliefValueType>
-class BeliefMdpExplorer;
-}
-namespace pomdp {
-namespace modelchecker {
-template<typename ValueType>
-struct BeliefExplorationPomdpModelCheckerOptions;
-}
-
-enum BeliefNumberType { Default, Float, Rational };
-}  // namespace pomdp
-
-namespace settings {
-namespace modules {
+namespace storm::settings::modules {
 
 /*!
  * This class represents the settings for POMDP model checking.
@@ -33,56 +17,34 @@ class BeliefExplorationSettings : public ModuleSettings {
     virtual ~BeliefExplorationSettings() = default;
 
     bool isCutZeroGapSet() const;
-    bool isRefineSet() const;
-    double getRefinePrecision() const;
-    uint64_t getRefineStepLimit() const;
 
     uint64_t getExplorationTimeLimit() const;
 
     /// Discretization Resolution
     uint64_t getResolutionInit() const;
-    double getResolutionFactor() const;
 
     /// Clipping Grid Resolution
     uint64_t getClippingGridResolution() const;
 
     /// The maximal number of newly expanded MDP states in a refinement step
     uint64_t getSizeThresholdInit() const;
-    double getSizeThresholdFactor() const;
-
-    /// Controls how large the gap between known lower- and upper bounds at a beliefstate needs to be in order to explore
-    double getGapThresholdInit() const;
-    double getGapThresholdFactor() const;
-
-    /// Controls whether "almost optimal" choices will be considered optimal
-    double getOptimalChoiceValueThresholdInit() const;
-    double getOptimalChoiceValueThresholdFactor() const;
-
-    /// Controls which observations are refined.
-    double getObservationScoreThresholdInit() const;
-    double getObservationScoreThresholdFactor() const;
-
-    /// Used to determine whether two beliefs are equal
-    bool isNumericPrecisionSetFromDefault() const;
-    double getNumericPrecision() const;
 
     bool isDynamicTriangulationModeSet() const;
     bool isStaticTriangulationModeSet() const;
 
-    /// Controls if (grid) clipping is to be used
+    /// Controls if grid clipping is to be used
     bool isUseClippingSet() const;
 
-    bool isStateEliminationCutoffSet() const;
+    bool isBeliefMDPNumberTypeDouble() const;
+    bool isBeliefMDPNumberTypeRational() const;
+    bool isBeliefMDPNumberTypeMatch() const;
 
-    template<typename ValueType>
-    void setValuesInOptionsStruct(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) const;
+    bool isInexactPreprocessingSet() const;
 
     // The name of the module.
     static const std::string moduleName;
 
    private:
 };
 
-}  // namespace modules
-}  // namespace settings
-}  // namespace storm
+}  // namespace storm::settings::modules

src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp

@@ -24,6 +24,8 @@ const std::string memoryPatternOption = "memorypattern";
 const std::vector<std::string> memoryPatterns = {"trivial", "fixedcounter", "selectivecounter", "ring", "fixedring", "settablebits", "full"};
 const std::string checkFullyObservableOption = "check-fully-observable";
 const std::string isQualitativeOption = "qualitative-analysis";
+const std::string isBoundedToUnboundedReachabilityTransformationOption = "unfold-reward-bound";
+const std::string isRewardObservableOption = "reward-aware";
 
 POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) {
     this->addOption(storm::settings::OptionBuilder(moduleName, noCanonicOption, false,
@@ -52,17 +54,29 @@ POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) {
                                          .setDefaultValueString("full")
                                          .build())
                         .build());
-    this->addOption(
-        storm::settings::OptionBuilder(moduleName, beliefExplorationOption, false, "Analyze the POMDP by exploring the belief state-space.")
-            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "Sets whether lower, upper, or interval result bounds are computed.")
-                             .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(beliefExplorationModes))
-                             .setDefaultValueString("both")
-                             .makeOptional()
-                             .build())
-            .build());
+    this->addOption(storm::settings::OptionBuilder(moduleName, beliefExplorationOption, false, "Analyze the POMDP by exploring the belief space.")
+                        .addArgument(storm::settings::ArgumentBuilder::createStringArgument(
+                                         "mode", "Sets whether lower bounds, upper bounds, or interval bounds are computed.")
+                                         .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(beliefExplorationModes))
+                                         .setDefaultValueString("both")
+                                         .makeOptional()
+                                         .build())
+                        .build());
     this->addOption(
         storm::settings::OptionBuilder(moduleName, checkFullyObservableOption, false, "Performs standard model checking on the underlying MDP").build());
     this->addOption(storm::settings::OptionBuilder(moduleName, isQualitativeOption, false, "Sets the option qualitative analysis").build());
+    this->addOption(storm::settings::OptionBuilder(
+                        moduleName, isBoundedToUnboundedReachabilityTransformationOption, false,
+                        "Sets the option that reward bounded reachability properties are transformed to an unbounded problem on an unfolded POMDP.")
+                        .build());
+    this->addOption(storm::settings::OptionBuilder(moduleName, isRewardObservableOption, false,
+                                                   "Sets the option that rewards are observable for bounded reachability properties.")
+                        .addArgument(storm::settings::ArgumentBuilder::createStringArgument(
+                                         "levelwidths", "comma separated list of (unsigned integer) width of reward levels.")
+                                         .setDefaultValueString("")
+                                         .makeOptional()
+                                         .build())
+                        .build());
 }
 
 bool POMDPSettings::isNoCanonicSet() const {
@@ -111,6 +125,25 @@ bool POMDPSettings::isQualitativeAnalysisSet() const {
     return this->getOption(isQualitativeOption).getHasOptionBeenSet();
 }
 
+bool POMDPSettings::isBoundedToUnboundedReachabilityTransformationSet() const {
+    return this->getOption(isBoundedToUnboundedReachabilityTransformationOption).getHasOptionBeenSet();
+}
+
+bool POMDPSettings::isRewardObservableSet() const {
+    return this->getOption(isRewardObservableOption).getHasOptionBeenSet();
+}
+
+std::vector<uint64_t> POMDPSettings::getLevelWidthForBoundedReachability() const {
+    auto const input = this->getOption(isRewardObservableOption).getArgumentByName("levelwidths").getValueAsString();
+    if (input.empty()) {
+        return {};
+    }
+    // split the string by comma
+    auto result = input | std::ranges::views::split(',') |
+                  std::ranges::views::transform([](auto&& r) -> uint64_t { return std::stoull(std::string(r.begin(), r.end())); });
+    return {result.begin(), result.end()};
+}
+
 uint64_t POMDPSettings::getMemoryBound() const {
     return this->getOption(memoryBoundOption).getArgumentByName("bound").getValueAsUnsignedInteger();
 }

src/storm-pomdp-cli/settings/modules/POMDPSettings.h

@@ -33,6 +33,9 @@ class POMDPSettings : public ModuleSettings {
     bool isSelfloopReductionSet() const;
     bool isCheckFullyObservableSet() const;
     bool isQualitativeAnalysisSet() const;
+    bool isBoundedToUnboundedReachabilityTransformationSet() const;
+    std::vector<uint64_t> getLevelWidthForBoundedReachability() const;
+    bool isRewardObservableSet() const;
     uint64_t getMemoryBound() const;
 
     storm::storage::PomdpMemoryPattern getMemoryPattern() const;