pmc simplifications are disabled by default, can be switched on via option

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

@@ -19,12 +19,15 @@ namespace storm {
             std::vector<std::string> fscModes = {"standard", "simple-linear", "simple-linear-inverse"};
             const std::string transformBinaryOption = "transformbinary";
             const std::string transformSimpleOption = "transformsimple";
+            const std::string allowSimplificationOption = "simplify-pmc";
 
             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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, allowSimplificationOption, false, "After obtaining a pMC, should further simplifications be applied?.").build());
+
             }
 
 
@@ -44,6 +47,10 @@ namespace storm {
                 return this->getOption(transformSimpleOption).getHasOptionBeenSet();
             }
 
+            bool ToParametricSettings::allowPostSimplifications() const {
+                return this->getOption(allowSimplificationOption).getHasOptionBeenSet();
+            }
+
             void ToParametricSettings::finalize() {
             }
 

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

@@ -31,6 +31,7 @@ namespace storm {
                 bool isMecReductionSet() const;
                 bool isTransformSimpleSet() const;
                 bool isTransformBinarySet() const;
+                bool allowPostSimplifications() const;
                 std::string getFscApplicationTypeString() const;
 
                 bool check() const override;

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

@@ -319,12 +319,12 @@ namespace storm {
                     auto pmc = toPMCTransformer.transform(storm::transformer::parsePomdpFscApplicationMode(transformMode));
                     STORM_PRINT_AND_LOG(" done." << std::endl);
                     pmc->printModelInformationToStream(std::cout);
-                    //if (transformSettings.isSimplificationSet()) {
+                    if (transformSettings.allowPostSimplifications()) {
                         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("Exporting pMC...");
                     storm::analysis::ConstraintCollector<storm::RationalFunction> constraints(*pmc);
                     auto const& parameterSet = constraints.getVariables();

src/storm/settings/modules/IOSettings.cpp

@@ -51,7 +51,7 @@ namespace storm {
             const std::string IOSettings::qvbsInputOptionShortName = "qvbs";
             const std::string IOSettings::qvbsRootOptionName = "qvbsroot";
 
-            std::string preventDRNPlaceholderOptionName = "nodrnplaceholders";
+            std::string preventDRNPlaceholderOptionName = "no-drn-placeholders";
             
             IOSettings::IOSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, false, "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced()