From 4bcb541866e69fe802b626a51a06aebbd373885f Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Mon, 25 May 2020 21:32:01 -0700
Subject: [PATCH] pmc simplifications are disabled by default, can be switched
 on via option

---
 .../settings/modules/ToParametricSettings.cpp              | 7 +++++++
 .../settings/modules/ToParametricSettings.h                | 1 +
 src/storm-pomdp-cli/storm-pomdp.cpp                        | 4 ++--
 src/storm/settings/modules/IOSettings.cpp                  | 2 +-
 4 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/storm-pomdp-cli/settings/modules/ToParametricSettings.cpp b/src/storm-pomdp-cli/settings/modules/ToParametricSettings.cpp
index 66abc3ee7..0a0e657a8 100644
--- a/src/storm-pomdp-cli/settings/modules/ToParametricSettings.cpp
+++ b/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() {
             }
 
diff --git a/src/storm-pomdp-cli/settings/modules/ToParametricSettings.h b/src/storm-pomdp-cli/settings/modules/ToParametricSettings.h
index e29586709..959b57851 100644
--- a/src/storm-pomdp-cli/settings/modules/ToParametricSettings.h
+++ b/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;
diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index 1ccc0cd56..eaa20c010 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/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();
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index 95c67a19e..dc438f231 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/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()