From d0c153da8df7d2aed3e348f2c70fc7b74c26f220 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 23 Oct 2020 17:41:05 +0200
Subject: [PATCH] Added switch `--no-simplify` to disable simplification of
 PRISM programs (which sometimes costs a bit of time on extremely large
 inputs)

---
 CHANGELOG.md                                 | 1 +
 src/storm-cli-utilities/model-handling.h     | 3 ++-
 src/storm/settings/modules/BuildSettings.cpp | 6 ++++++
 src/storm/settings/modules/BuildSettings.h   | 6 +++++-
 4 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f3b2e2a87..42c9feec6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,7 @@ Version 1.6.x
 - Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives.
 - Added support for generating optimal schedulers for globally formulae
 - Simulator supports exact arithmetic
+- Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)
 - `storm-pomdp`: States can be labelled with values for observable predicates
 - `storm-pomdp`: (Only API) Track state estimates
 - `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 9fc3cc772..db1581e49 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -67,10 +67,11 @@ namespace storm {
         };
         
         void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) {
+            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             if (ioSettings.isPrismOrJaniInputSet()) {
                 storm::utility::Stopwatch modelParsingWatch(true);
                 if (ioSettings.isPrismInputSet()) {
-                    input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule<storm::settings::modules::BuildSettings>().isPrismCompatibilityEnabled());
+                    input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), buildSettings.isPrismCompatibilityEnabled(), !buildSettings.isNoSimplifySet());
                 } else {
                     boost::optional<std::vector<std::string>> propertyFilter;
                     if (ioSettings.isJaniPropertiesSet()) {
diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp
index 83c4b19d4..d0c2cbbc3 100644
--- a/src/storm/settings/modules/BuildSettings.cpp
+++ b/src/storm/settings/modules/BuildSettings.cpp
@@ -35,6 +35,7 @@ namespace storm {
             const std::string buildAllLabelsOptionName = "build-all-labels";
             const std::string buildOutOfBoundsStateOptionName = "build-out-of-bounds-state";
             const std::string buildOverlappingGuardsLabelOptionName = "build-overlapping-guards-label";
+            const std::string noSimplifyOptionName = "no-simplify";
             const std::string bitsForUnboundedVariablesOptionName = "int-bits";
 
             BuildSettings::BuildSettings() : ModuleSettings(moduleName) {
@@ -55,6 +56,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, buildOverlappingGuardsLabelOptionName, false, "For states where multiple guards are enabled, we add a label (for debugging DTMCs)").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, noSimplifyOptionName, false, "If set, simplification PRISM input is disabled.").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.").setIsAdvanced()
                                         .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build());
             }
@@ -124,6 +126,10 @@ namespace storm {
             bool BuildSettings::isExplorationChecksSet() const {
                 return this->getOption(explorationChecksOptionName).getHasOptionBeenSet();
             }
+            
+            bool BuildSettings::isNoSimplifySet() const {
+                return this->getOption(noSimplifyOptionName).getHasOptionBeenSet();
+            }
 
             uint64_t BuildSettings::getBitsForUnboundedVariables() const {
                 return this->getOption(bitsForUnboundedVariablesOptionName).getArgumentByName("number").getValueAsUnsignedInteger();
diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h
index 9c81859c3..de73140f5 100644
--- a/src/storm/settings/modules/BuildSettings.h
+++ b/src/storm/settings/modules/BuildSettings.h
@@ -115,7 +115,11 @@ namespace storm {
                  * @return
                  */
                 uint64_t getBitsForUnboundedVariables() const;
-
+                
+                /*!
+                 * Retrieves whether simplification of symbolic inputs through static analysis shall be disabled
+                 */
+                 bool isNoSimplifySet() const;
 
                 // The name of the module.
                 static const std::string moduleName;