Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)

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

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()) {

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();

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;