From 20f5cf158bacd2459fb0180e4781f80ae0f25034 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 5 Mar 2020 14:51:51 +0100 Subject: [PATCH] storm-dft: Using symmetry reduction by default. --- CHANGELOG.md | 1 + src/storm-dft-cli/storm-dft.cpp | 8 ++++++-- src/storm-dft/settings/modules/FaultTreeSettings.cpp | 10 +++++----- src/storm-dft/settings/modules/FaultTreeSettings.h | 4 ++-- 4 files changed, 14 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index dc6cf6827..eb6ba34a6 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 130e32765..5d835b4c7 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -21,8 +21,6 @@ */ template void processOptions() { - // Start by setting some urgent options (log levels, resources, etc.) - storm::cli::setUrgentOptions(); auto const& dftIOSettings = storm::settings::getModule(); auto const& faultTreeSettings = storm::settings::getModule(); @@ -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(); if (generalSettings.isParametricSet()) { processOptions(); + } else if (generalSettings.isExactSet()) { + STORM_LOG_WARN("Exact solving over rational numbers is not implemented. Performing exact solving using rational functions instead."); + processOptions(); } else { processOptions(); } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index 3fa4d6529..f6e2517c6 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/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 { diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 6c5298f7b..3099f4b8b 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/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;