split pomdp settings into toparametric settings for the UAI18 stuff

src/storm-pomdp-cli/settings/PomdpSettings.cpp

@@ -34,6 +34,7 @@
 #include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
 #include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h"
 #include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h"
+#include "storm-pomdp-cli/settings/modules/ToParametricSettings.h"
 
 
 namespace storm {
@@ -50,6 +51,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::POMDPSettings>();
             storm::settings::addModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
             storm::settings::addModule<storm::settings::modules::BeliefExplorationSettings>();
+            storm::settings::addModule<storm::settings::modules::ToParametricSettings>();
         
             storm::settings::addModule<storm::settings::modules::TransformationSettings>();
             storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();

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

@@ -19,15 +19,10 @@ namespace storm {
             std::vector<std::string> beliefExplorationModes = {"both", "discretize", "unfold"};
             const std::string qualitativeReductionOption = "qualitativereduction";
             const std::string analyzeUniqueObservationsOption = "uniqueobservations";
-            const std::string mecReductionOption = "mecreduction";
             const std::string selfloopReductionOption = "selfloopreduction";
             const std::string memoryBoundOption = "memorybound";
             const std::string memoryPatternOption = "memorypattern";
             std::vector<std::string> memoryPatterns = {"trivial", "fixedcounter", "selectivecounter", "ring", "fixedring", "settablebits", "full"};
-            const std::string fscmode = "fscmode";
-            std::vector<std::string> fscModes = {"standard", "simple-linear", "simple-linear-inverse"};
-            const std::string transformBinaryOption = "transformbinary";
-            const std::string transformSimpleOption = "transformsimple";
             const std::string checkFullyObservableOption = "check-fully-observable";
             const std::string isQualitativeOption = "qualitative-analysis";
 
@@ -36,13 +31,9 @@ namespace storm {
                 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());
                 this->addOption(storm::settings::OptionBuilder(moduleName, qualitativeReductionOption, false, "Reduces the model size by performing qualitative analysis (E.g. merge states with prob. 1.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, analyzeUniqueObservationsOption, false, "Computes the states with a unique observation").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, mecReductionOption, false, "Reduces the model size by analyzing maximal end components").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, selfloopReductionOption, false, "Reduces the model size by removing self loop actions").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, memoryBoundOption, false, "Sets the maximal number of allowed memory states (1 means memoryless schedulers).").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("bound", "The maximal number of memory states.").setDefaultValueUnsignedInteger(1).addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, memoryPatternOption, false, "Sets the pattern of the considered memory structure").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "Pattern name.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memoryPatterns)).setDefaultValueString("full").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, fscmode, false, "Sets the way the pMC is obtained").addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "type name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(fscModes)).setDefaultValueString("standard").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").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, 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());
@@ -68,10 +59,6 @@ namespace storm {
                 return this->getOption(analyzeUniqueObservationsOption).getHasOptionBeenSet();
             }
             
-            bool POMDPSettings::isMecReductionSet() const {
-                return this->getOption(mecReductionOption).getHasOptionBeenSet();
-            }
-            
             bool POMDPSettings::isSelfloopReductionSet() const {
                 return this->getOption(selfloopReductionOption).getHasOptionBeenSet();
             }
@@ -123,18 +110,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The name of the memory pattern is unknown.");
             }
 
-            std::string POMDPSettings::getFscApplicationTypeString() const {
-                return this->getOption(fscmode).getArgumentByName("type").getValueAsString();
-            }
-            
-            bool POMDPSettings::isTransformBinarySet() const {
-                return this->getOption(transformBinaryOption).getHasOptionBeenSet();
-            }
 
-            bool POMDPSettings::isTransformSimpleSet() const {
-                return this->getOption(transformSimpleOption).getHasOptionBeenSet();
-            }
-            
             void POMDPSettings::finalize() {
             }
 

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

@@ -31,13 +31,9 @@ namespace storm {
                 bool isBeliefExplorationDiscretizeSet() const;
                 bool isBeliefExplorationUnfoldSet() const;
                 bool isAnalyzeUniqueObservationsSet() const;
-                bool isMecReductionSet() const;
                 bool isSelfloopReductionSet() const;
-                bool isTransformSimpleSet() const;
-                bool isTransformBinarySet() const;
                 bool isCheckFullyObservableSet() const;
                 bool isQualitativeAnalysisSet() const;
-                std::string getFscApplicationTypeString() const;
                 uint64_t getMemoryBound() const;
 
                 storm::storage::PomdpMemoryPattern getMemoryPattern() const;

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

@@ -0,0 +1,56 @@
+#include "storm-pomdp-cli/settings/modules/ToParametricSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            const std::string ToParametricSettings::moduleName = "toparametric";
+            const std::string mecReductionOption = "mecreduction";
+            const std::string selfloopReductionOption = "selfloopreduction";
+            const std::string fscmode = "fscmode";
+            std::vector<std::string> fscModes = {"standard", "simple-linear", "simple-linear-inverse"};
+            const std::string transformBinaryOption = "transformbinary";
+            const std::string transformSimpleOption = "transformsimple";
+
+            ToParametricSettings::ToParametricSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, mecReductionOption, false, "Reduces the model size by analyzing maximal end components").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, fscmode, false, "Sets the way the pMC is obtained").addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "type name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(fscModes)).setDefaultValueString("standard").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").build());
+            }
+
+
+            bool ToParametricSettings::isMecReductionSet() const {
+                return this->getOption(mecReductionOption).getHasOptionBeenSet();
+            }
+
+            std::string ToParametricSettings::getFscApplicationTypeString() const {
+                return this->getOption(fscmode).getArgumentByName("type").getValueAsString();
+            }
+
+            bool ToParametricSettings::isTransformBinarySet() const {
+                return this->getOption(transformBinaryOption).getHasOptionBeenSet();
+            }
+
+            bool ToParametricSettings::isTransformSimpleSet() const {
+                return this->getOption(transformSimpleOption).getHasOptionBeenSet();
+            }
+
+            void ToParametricSettings::finalize() {
+            }
+
+            bool ToParametricSettings::check() const {
+                return true;
+            }
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

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

@@ -0,0 +1,49 @@
+#pragma once
+
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+#include "storm-pomdp/storage/PomdpMemory.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for POMDP model checking.
+             */
+            class ToParametricSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of POMDP settings.
+                 */
+                ToParametricSettings();
+
+                virtual ~ToParametricSettings() = default;
+
+                bool isExportToParametricSet() const;
+                std::string getExportToParametricFilename() const;
+
+                bool isQualitativeReductionSet() const;
+
+                bool isMecReductionSet() const;
+                bool isTransformSimpleSet() const;
+                bool isTransformBinarySet() const;
+                std::string getFscApplicationTypeString() const;
+
+                bool check() const override;
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+
+
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-pomdp-cli/storm-pomdp.cpp

@@ -5,6 +5,7 @@
 #include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
 #include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h"
 #include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h"
+#include "storm-pomdp-cli/settings/modules/ToParametricSettings.h"
 
 #include "storm-pomdp-cli/settings/PomdpSettings.h"
 #include "storm/analysis/GraphConditions.h"
@@ -268,6 +269,8 @@ namespace storm {
             template<typename ValueType, storm::dd::DdType DdType>
             bool performTransformation(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>>& pomdp, storm::logic::Formula const& formula) {
                 auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
+                auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+                auto const& transformSettings = storm::settings::getModule<storm::settings::modules::ToParametricSettings>();
                 bool transformationPerformed = false;
                 bool memoryUnfolded = false;
                 if (pomdpSettings.getMemoryBound() > 1) {
@@ -284,7 +287,7 @@ namespace storm {
         
                 // From now on the pomdp is considered memoryless
         
-                if (pomdpSettings.isMecReductionSet()) {
+                if (transformSettings.isMecReductionSet()) {
                     STORM_PRINT_AND_LOG("Eliminating mec choices ...");
                     // Note: Elimination of mec choices only preserves memoryless schedulers.
                     uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
@@ -296,8 +299,8 @@ namespace storm {
                     transformationPerformed = true;
                 }
         
-                if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) {
-                    if (pomdpSettings.isTransformSimpleSet()) {
+                if (transformSettings.isTransformBinarySet() || transformSettings.isTransformSimpleSet()) {
+                    if (transformSettings.isTransformSimpleSet()) {
                         STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP.");
                         pomdp = storm::transformer::BinaryPomdpTransformer<ValueType>().transform(*pomdp, true);
                     } else {
@@ -312,17 +315,16 @@ namespace storm {
                 if (pomdpSettings.isExportToParametricSet()) {
                     STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC...");
                     storm::transformer::ApplyFiniteSchedulerToPomdp<ValueType> toPMCTransformer(*pomdp);
-                    std::string transformMode = pomdpSettings.getFscApplicationTypeString();
+                    std::string transformMode = transformSettings.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<storm::RationalFunction>(pmc->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(),{formula.asSharedPointer()}, storm::storage::BisimulationType::Strong)->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-        
+                    //if (transformSettings.isSimplificationSet()) {
+                        STORM_PRINT_AND_LOG("Simplifying pMC...");
+                        pmc = storm::api::performBisimulationMinimization<storm::RationalFunction>(pmc->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(),{formula.asSharedPointer()}, storm::storage::BisimulationType::Strong)->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+                        STORM_PRINT_AND_LOG(" done." << std::endl);
+                        pmc->printModelInformationToStream(std::cout);
                     //}
-                    STORM_PRINT_AND_LOG(" done." << std::endl);
-                    pmc->printModelInformationToStream(std::cout);
                     STORM_PRINT_AND_LOG("Exporting pMC...");
                     storm::analysis::ConstraintCollector<storm::RationalFunction> constraints(*pmc);
                     auto const& parameterSet = constraints.getVariables();