storm-dft: Using symmetry reduction by default.

CHANGELOG.md

@@ -15,6 +15,7 @@ Version 1.4.x
 - Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`).
 - Apply the maximum progress assumption while building a Markov automata with the Dd engine.
 - Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata)
+- `storm-dft`: Symmetry reduction is now enabled by default and can be disabled via `--nosymmetryreduction`
 - `storm-pomdp`: Only accept POMDPs that are canonical
 - `storm-pomdp`: Prism language extended with observable expressions
 - `storm-pomdp`: Various fixes that prevented usage.

src/storm-dft-cli/storm-dft.cpp

@@ -21,8 +21,6 @@
  */
 template<typename ValueType>
 void processOptions() {
-    // Start by setting some urgent options (log levels, resources, etc.)
-    storm::cli::setUrgentOptions();
 
     auto const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
     auto const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
@@ -265,10 +263,16 @@ int main(const int argc, const char** argv) {
         if (!storm::cli::parseOptions(argc, argv)) {
             return -1;
         }
+        
+        // Start by setting some urgent options (log levels, resources, etc.)
+        storm::cli::setUrgentOptions();
 
         storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
         if (generalSettings.isParametricSet()) {
             processOptions<storm::RationalFunction>();
+        } else if (generalSettings.isExactSet()) {
+            STORM_LOG_WARN("Exact solving over rational numbers is not implemented. Performing exact solving using rational functions instead.");
+            processOptions<storm::RationalFunction>();
         } else {
             processOptions<double>();
         }

src/storm-dft/settings/modules/FaultTreeSettings.cpp

@@ -15,8 +15,8 @@ namespace storm {
         namespace modules {
 
             const std::string FaultTreeSettings::moduleName = "dft";
-            const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction";
-            const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred";
+            const std::string FaultTreeSettings::noSymmetryReductionOptionName = "nosymmetryreduction";
+            const std::string FaultTreeSettings::noSymmetryReductionOptionShortName = "nosymred";
             const std::string FaultTreeSettings::modularisationOptionName = "modularisation";
             const std::string FaultTreeSettings::disableDCOptionName = "disabledc";
             const std::string FaultTreeSettings::allowDCRelevantOptionName = "allowdcrelevant";
@@ -32,8 +32,8 @@ namespace storm {
 #endif
 
             FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(
-                        symmetryReductionOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, noSymmetryReductionOptionName, false, "Do not exploit symmetric structure of model.").setShortName(
+                        noSymmetryReductionOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Don't Care propagation.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false,
@@ -62,7 +62,7 @@ namespace storm {
             }
 
             bool FaultTreeSettings::useSymmetryReduction() const {
-                return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
+                return !this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
             }
 
             bool FaultTreeSettings::useModularisation() const {

src/storm-dft/settings/modules/FaultTreeSettings.h

@@ -130,8 +130,8 @@ namespace storm {
 
             private:
                 // Define the string names of the options as constants.
-                static const std::string symmetryReductionOptionName;
-                static const std::string symmetryReductionOptionShortName;
+                static const std::string noSymmetryReductionOptionName;
+                static const std::string noSymmetryReductionOptionShortName;
                 static const std::string modularisationOptionName;
                 static const std::string disableDCOptionName;
                 static const std::string allowDCRelevantOptionName;