Conditional model checking

src/storm-pomdp/transformer/ObservationTraceUnfolder.h

@@ -47,7 +47,7 @@ class ObservationTraceUnfolder {
     bool isRestartSemanticsSet() const;
 
    private:
-    storm::models::sparse::Pomdp<ValueType> const& model;
+    storm::models::sparse::Pomdp<ValueType> model;
     std::vector<ValueType> risk;  // TODO reconsider holding this as a reference, but there were some strange bugs
     std::shared_ptr<storm::expressions::ExpressionManager>& exprManager;
     std::vector<uint32_t> traceSoFar;

src/storm/environment/SubEnvironment.cpp

@@ -48,6 +48,7 @@ void SubEnvironment<EnvironmentType>::assertInitialized() const {
 
 template class SubEnvironment<InternalEnvironment>;
 
+template class SubEnvironment<ConditionalModelCheckerEnvironment>;
 template class SubEnvironment<MultiObjectiveModelCheckerEnvironment>;
 template class SubEnvironment<ModelCheckerEnvironment>;
 

src/storm/environment/modelchecker/AllModelCheckerEnvironments.h

@@ -1,4 +1,5 @@
 #pragma once
 
+#include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h"
 #include "storm/environment/modelchecker/ModelCheckerEnvironment.h"
 #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"

src/storm/environment/modelchecker/ConditionalModelCheckerEnvironment.cpp

@@ -0,0 +1,51 @@
+#include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h"
+
+#include "storm/adapters/RationalNumberForward.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/ConditionalSettings.h"
+#include "storm/utility/constants.h"
+
+namespace storm {
+
+ConditionalModelCheckerEnvironment::ConditionalModelCheckerEnvironment() {
+    auto const& mcSettings = storm::settings::getModule<storm::settings::modules::ConditionalSettings>();
+    algorithm = mcSettings.getConditionalAlgorithmSetting();
+    precision = storm::utility::convertNumber<storm::RationalNumber>(mcSettings.getConditionalPrecision());
+    relative = !mcSettings.isConditionalPrecisionAbsolute();
+    precisionSetFromDefault = mcSettings.isConditionalPrecisionSetFromDefaultValue();
+}
+
+ConditionalModelCheckerEnvironment::~ConditionalModelCheckerEnvironment() {
+    // Intentionally left empty
+}
+
+ConditionalAlgorithmSetting ConditionalModelCheckerEnvironment::getAlgorithm() const {
+    return algorithm;
+}
+
+void ConditionalModelCheckerEnvironment::setAlgorithm(ConditionalAlgorithmSetting value) {
+    algorithm = value;
+}
+
+storm::RationalNumber ConditionalModelCheckerEnvironment::getPrecision() const {
+    return precision;
+}
+
+void ConditionalModelCheckerEnvironment::setPrecision(storm::RationalNumber const& value, bool setFromDefault) {
+    precision = value;
+    precisionSetFromDefault = setFromDefault;
+}
+
+bool ConditionalModelCheckerEnvironment::isPrecisionSetFromDefault() const {
+    return precisionSetFromDefault;
+}
+
+bool ConditionalModelCheckerEnvironment::isRelativePrecision() const {
+    return relative;
+}
+
+void ConditionalModelCheckerEnvironment::setRelativePrecision(bool value) {
+    relative = value;
+}
+
+}  // namespace storm

src/storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h

@@ -0,0 +1,30 @@
+#pragma once
+
+#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/modelchecker/helper/conditional/ConditionalAlgorithmSetting.h"
+
+namespace storm {
+
+class ConditionalModelCheckerEnvironment {
+   public:
+    ConditionalModelCheckerEnvironment();
+    ~ConditionalModelCheckerEnvironment();
+
+    ConditionalAlgorithmSetting getAlgorithm() const;
+    void setAlgorithm(ConditionalAlgorithmSetting value);
+
+    storm::RationalNumber getPrecision() const;
+    bool isPrecisionSetFromDefault() const;
+    void setPrecision(storm::RationalNumber const& value, bool setFromDefault);
+
+    bool isRelativePrecision() const;
+    void setRelativePrecision(bool value);
+
+   private:
+    ConditionalAlgorithmSetting algorithm;
+    storm::RationalNumber precision;
+    bool precisionSetFromDefault;
+    bool relative;
+};
+
+}  // namespace storm

src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp

@@ -1,5 +1,6 @@
 #include "storm/environment/modelchecker/ModelCheckerEnvironment.h"
 
+#include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h"
 #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
 
 #include "storm/settings/SettingsManager.h"
@@ -19,28 +20,26 @@ ModelCheckerEnvironment::ModelCheckerEnvironment() {
     }
     auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
     steadyStateDistributionAlgorithm = ioSettings.getSteadyStateDistributionAlgorithm();
-
-    conditionalAlgorithmSetting = mcSettings.getConditionalAlgorithmSetting();
 }
 
 ModelCheckerEnvironment::~ModelCheckerEnvironment() {
     // Intentionally left empty
 }
 
-SteadyStateDistributionAlgorithm ModelCheckerEnvironment::getSteadyStateDistributionAlgorithm() const {
-    return steadyStateDistributionAlgorithm;
+ConditionalModelCheckerEnvironment& ModelCheckerEnvironment::conditional() {
+    return conditionalModelCheckerEnvironment.get();
 }
 
-void ModelCheckerEnvironment::setSteadyStateDistributionAlgorithm(SteadyStateDistributionAlgorithm value) {
-    steadyStateDistributionAlgorithm = value;
+ConditionalModelCheckerEnvironment const& ModelCheckerEnvironment::conditional() const {
+    return conditionalModelCheckerEnvironment.get();
 }
 
-ConditionalAlgorithmSetting ModelCheckerEnvironment::getConditionalAlgorithmSetting() const {
-    return conditionalAlgorithmSetting;
+SteadyStateDistributionAlgorithm ModelCheckerEnvironment::getSteadyStateDistributionAlgorithm() const {
+    return steadyStateDistributionAlgorithm;
 }
 
-void ModelCheckerEnvironment::setConditionalAlgorithmSetting(ConditionalAlgorithmSetting value) {
-    conditionalAlgorithmSetting = value;
+void ModelCheckerEnvironment::setSteadyStateDistributionAlgorithm(SteadyStateDistributionAlgorithm value) {
+    steadyStateDistributionAlgorithm = value;
 }
 
 MultiObjectiveModelCheckerEnvironment& ModelCheckerEnvironment::multi() {

src/storm/environment/modelchecker/ModelCheckerEnvironment.h

@@ -1,42 +1,41 @@
 #pragma once
 
 #include <boost/optional.hpp>
-#include <memory>
 #include <string>
 
 #include "storm/environment/Environment.h"
 #include "storm/environment/SubEnvironment.h"
-#include "storm/modelchecker/helper/conditional/ConditionalAlgorithmSetting.h"
 #include "storm/modelchecker/helper/infinitehorizon/SteadyStateDistributionAlgorithm.h"
 
 namespace storm {
 
 // Forward declare subenvironments
+class ConditionalModelCheckerEnvironment;
 class MultiObjectiveModelCheckerEnvironment;
 
 class ModelCheckerEnvironment {
    public:
     ModelCheckerEnvironment();
     ~ModelCheckerEnvironment();
 
+    ConditionalModelCheckerEnvironment& conditional();
+    ConditionalModelCheckerEnvironment const& conditional() const;
+
     MultiObjectiveModelCheckerEnvironment& multi();
     MultiObjectiveModelCheckerEnvironment const& multi() const;
 
     SteadyStateDistributionAlgorithm getSteadyStateDistributionAlgorithm() const;
     void setSteadyStateDistributionAlgorithm(SteadyStateDistributionAlgorithm value);
 
-    ConditionalAlgorithmSetting getConditionalAlgorithmSetting() const;
-    void setConditionalAlgorithmSetting(ConditionalAlgorithmSetting value);
-
     bool isLtl2daToolSet() const;
     std::string const& getLtl2daTool() const;
     void setLtl2daTool(std::string const& value);
     void unsetLtl2daTool();
 
    private:
+    SubEnvironment<ConditionalModelCheckerEnvironment> conditionalModelCheckerEnvironment;
     SubEnvironment<MultiObjectiveModelCheckerEnvironment> multiObjectiveModelCheckerEnvironment;
     boost::optional<std::string> ltl2daTool;
     SteadyStateDistributionAlgorithm steadyStateDistributionAlgorithm;
-    ConditionalAlgorithmSetting conditionalAlgorithmSetting;
 };
 }  // namespace storm

src/storm/io/DirectEncodingExporter.cpp

@@ -329,6 +329,9 @@ template void explicitExportSparseModel<storm::RationalFunction>(std::filesystem
 template void explicitExportSparseModel<storm::Interval>(std::filesystem::path const& os,
                                                          std::shared_ptr<storm::models::sparse::Model<storm::Interval>> sparseModel,
                                                          std::vector<std::string> const& parameters, DirectEncodingExporterOptions const& options);
+template void explicitExportSparseModel<storm::RationalInterval>(std::filesystem::path const& os,
+                                                                 std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> sparseModel,
+                                                                 std::vector<std::string> const& parameters, DirectEncodingExporterOptions const& options);
 
 template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel,
                                                 std::vector<std::string> const& parameters, DirectEncodingExporterOptions const& options);

src/storm/modelchecker/helper/conditional/ConditionalAlgorithmSetting.cpp

@@ -11,6 +11,10 @@ std::ostream& operator<<(std::ostream& stream, ConditionalAlgorithmSetting const
             return stream << "bisection";
         case ConditionalAlgorithmSetting::BisectionAdvanced:
             return stream << "bisection-advanced";
+        case ConditionalAlgorithmSetting::BisectionPolicyTracking:
+            return stream << "bisection-pt";
+        case ConditionalAlgorithmSetting::BisectionAdvancedPolicyTracking:
+            return stream << "bisection-advanced-pt";
         case ConditionalAlgorithmSetting::PolicyIteration:
             return stream << "pi";
     }
@@ -27,6 +31,10 @@ ConditionalAlgorithmSetting conditionalAlgorithmSettingFromString(std::string co
         return ConditionalAlgorithmSetting::Bisection;
     } else if (algorithm == "bisection-advanced") {
         return ConditionalAlgorithmSetting::BisectionAdvanced;
+    } else if (algorithm == "bisection-pt") {
+        return ConditionalAlgorithmSetting::BisectionPolicyTracking;
+    } else if (algorithm == "bisection-advanced-pt") {
+        return ConditionalAlgorithmSetting::BisectionAdvancedPolicyTracking;
     } else if (algorithm == "pi") {
         return ConditionalAlgorithmSetting::PolicyIteration;
     }

src/storm/modelchecker/helper/conditional/ConditionalAlgorithmSetting.h

@@ -5,7 +5,15 @@
 #include "storm/utility/macros.h"
 
 namespace storm {
-enum class ConditionalAlgorithmSetting { Default, Restart, Bisection, BisectionAdvanced, PolicyIteration };
+enum class ConditionalAlgorithmSetting {
+    Default,
+    Restart,
+    Bisection,
+    BisectionAdvanced,
+    BisectionPolicyTracking,
+    BisectionAdvancedPolicyTracking,
+    PolicyIteration
+};
 
 std::ostream& operator<<(std::ostream& stream, ConditionalAlgorithmSetting const& algorithm);
 ConditionalAlgorithmSetting conditionalAlgorithmSettingFromString(std::string const& algorithm);