From 8a74be1b72f429c0959aa351578438792f86d9ed Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 11 Oct 2017 17:57:15 +0200 Subject: [PATCH] Refactored DFT settings --- src/storm-dft-cli/storm-dft.cpp | 124 ++++-------- .../builder/ExplicitDFTModelBuilder.cpp | 2 - .../builder/ExplicitDFTModelBuilderApprox.cpp | 4 +- .../generator/DftNextStateGenerator.cpp | 4 +- .../modelchecker/dft/DFTModelChecker.cpp | 4 +- src/storm-dft/settings/DftSettings.cpp | 51 +++++ src/storm-dft/settings/DftSettings.h | 11 + .../settings/modules/DFTSettings.cpp | 189 ------------------ .../settings/modules/DftIOSettings.cpp | 123 ++++++++++++ .../{DFTSettings.h => DftIOSettings.h} | 80 +------- .../settings/modules/FaultTreeSettings.cpp | 93 +++++++++ .../settings/modules/FaultTreeSettings.h | 104 ++++++++++ 12 files changed, 432 insertions(+), 357 deletions(-) create mode 100644 src/storm-dft/settings/DftSettings.cpp create mode 100644 src/storm-dft/settings/DftSettings.h delete mode 100644 src/storm-dft/settings/modules/DFTSettings.cpp create mode 100644 src/storm-dft/settings/modules/DftIOSettings.cpp rename src/storm-dft/settings/modules/{DFTSettings.h => DftIOSettings.h} (63%) create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.cpp create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.h diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index b6fb0c751..3e69fb217 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -1,20 +1,14 @@ -#include "storm/logic/Formula.h" -#include "storm/utility/initialize.h" -#include "storm/api/storm.h" -#include "storm-cli-utilities/cli.h" -#include "storm/exceptions/BaseException.h" - -#include "storm/logic/Formula.h" +#include "storm-dft/settings/DftSettings.h" +#include "storm-dft/settings/modules/DftIOSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" -#include "storm/settings/modules/MinMaxEquationSolverSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/settings/modules/EliminationSettings.h" #include "storm/settings/modules/ResourceSettings.h" +#include "storm/utility/initialize.h" +#include "storm/api/storm.h" +#include "storm-cli-utilities/cli.h" + #include "storm-dft/parser/DFTGalileoParser.h" #include "storm-dft/parser/DFTJsonParser.h" #include "storm-dft/modelchecker/dft/DFTModelChecker.h" @@ -22,12 +16,8 @@ #include "storm-dft/transformations/DftToGspnTransformator.h" #include "storm-dft/storage/dft/DftJsonExporter.h" -#include "storm-dft/settings/modules/DFTSettings.h" - #include "storm-gspn/storage/gspn/GSPN.h" #include "storm-gspn/storm-gspn.h" -#include "storm/settings/modules/GSPNSettings.h" -#include "storm/settings/modules/GSPNExportSettings.h" #include #include @@ -44,18 +34,18 @@ */ template void analyzeDFT(std::vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { - storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); std::shared_ptr> dft; // Build DFT from given file. - if (dftSettings.isDftJsonFileSet()) { + if (dftIOSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl; - dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + std::cout << "Loading DFT from file " << dftIOSettings.getDftJsonFilename() << std::endl; + dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser; - std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl; - dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + std::cout << "Loading DFT from file " << dftIOSettings.getDftFilename() << std::endl; + dft = std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); } // Build properties @@ -91,72 +81,39 @@ void analyzeWithSMT(std::string filename) { //std::cout << "SMT result: " << sat << std::endl; } - -/*! - * Initialize the settings manager. - */ -void initializeSettings() { - storm::settings::mutableManager().setName("Storm-DyFTeE", "storm-dft"); - - // Register all known settings modules. - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - - // For translation into JANI via GSPN. - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); -} - - void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); storm::cli::processOptions(); - storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); + storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); - if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) { + if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } - if (dftSettings.isExportToJson()) { - STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); + if (dftIOSettings.isExportToJson()) { + STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); + storm::storage::DFT dft = parser.parseDFT(dftIOSettings.getDftFilename()); // Export to json - storm::storage::DftJsonExporter::toFile(dft, dftSettings.getExportJsonFilename()); + storm::storage::DftJsonExporter::toFile(dft, dftIOSettings.getExportJsonFilename()); storm::utility::cleanUp(); return; } - if (dftSettings.isTransformToGspn()) { + if (dftIOSettings.isTransformToGspn()) { std::shared_ptr> dft; - if (dftSettings.isDftJsonFileSet()) { + if (dftIOSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser(true, false); - dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + dft = std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); } storm::transformations::dft::DftToGspnTransformator gspnTransformator(*dft); gspnTransformator.transform(); @@ -196,12 +153,12 @@ void processOptions() { #endif #ifdef STORM_HAVE_Z3 - if (dftSettings.solveWithSMT()) { + if (faultTreeSettings.solveWithSMT()) { // Solve with SMT if (parametric) { // analyzeWithSMT(dftSettings.getDftFilename()); } else { - analyzeWithSMT(dftSettings.getDftFilename()); + analyzeWithSMT(dftIOSettings.getDftFilename()); } storm::utility::cleanUp(); return; @@ -210,8 +167,8 @@ void processOptions() { // Set min or max std::string optimizationDirection = "min"; - if (dftSettings.isComputeMaximalValue()) { - STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); + if (dftIOSettings.isComputeMaximalValue()) { + STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); optimizationDirection = "max"; } @@ -221,19 +178,19 @@ void processOptions() { if (ioSettings.isPropertySet()) { properties.push_back(ioSettings.getProperty()); } - if (dftSettings.usePropExpectedTime()) { + if (dftIOSettings.usePropExpectedTime()) { properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); } - if (dftSettings.usePropProbability()) { + if (dftIOSettings.usePropProbability()) { properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); } - if (dftSettings.usePropTimebound()) { + if (dftIOSettings.usePropTimebound()) { std::stringstream stream; - stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]"; + stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]"; properties.push_back(stream.str()); } - if (dftSettings.usePropTimepoints()) { - for (double timepoint : dftSettings.getPropTimepoints()) { + if (dftIOSettings.usePropTimepoints()) { + for (double timepoint : dftIOSettings.getPropTimepoints()) { std::stringstream stream; stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; properties.push_back(stream.str()); @@ -246,19 +203,19 @@ void processOptions() { // Set possible approximation error double approximationError = 0.0; - if (dftSettings.isApproximationErrorSet()) { - approximationError = dftSettings.getApproximationError(); + if (faultTreeSettings.isApproximationErrorSet()) { + approximationError = faultTreeSettings.getApproximationError(); } // From this point on we are ready to carry out the actual computations. if (parametric) { #ifdef STORM_HAVE_CARL - analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); #endif } else { - analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); } } @@ -275,9 +232,8 @@ void processOptions() { int main(const int argc, const char** argv) { try { storm::utility::setUp(); - storm::cli::printHeader("Storm-DyFTeE", argc, argv); - //storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); - initializeSettings(); + storm::cli::printHeader("Storm-dft", argc, argv); + storm::settings::initializeDftSettings("Storm-dft", "storm-dft"); storm::utility::Stopwatch totalTimer(true); if (!storm::cli::parseOptions(argc, argv)) { diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 4a29b0652..5ef6bd07e 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -9,8 +9,6 @@ #include "storm/exceptions/UnexpectedException.h" #include "storm/settings/SettingsManager.h" -#include "storm-dft/settings/modules/DFTSettings.h" - namespace storm { namespace builder { diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 0c7d69628..f035b0a55 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -10,7 +10,7 @@ #include "storm/exceptions/UnexpectedException.h" #include "storm/settings/SettingsManager.h" #include "storm/logic/AtomicLabelFormula.h" -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { @@ -55,7 +55,7 @@ namespace storm { dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), - usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), + usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 7b86d1faa..0002cd6a3 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -4,7 +4,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/settings/SettingsManager.h" -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { namespace generator { @@ -71,7 +71,7 @@ namespace storm { // Let BE fail while (currentFailable < failableCount) { - if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { + if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { // We discard further exploration as we already chose one dependent event break; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index d6b7e9138..45d97baa6 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -8,7 +8,7 @@ #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { @@ -344,7 +344,7 @@ namespace storm { STORM_LOG_INFO("Building Model..."); std::shared_ptr> model; // TODO Matthias: use only one builder if everything works again - if (storm::settings::getModule().isApproximationErrorSet()) { + if (storm::settings::getModule().isApproximationErrorSet()) { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp new file mode 100644 index 000000000..ce48c6fd9 --- /dev/null +++ b/src/storm-dft/settings/DftSettings.cpp @@ -0,0 +1,51 @@ +#include "storm-dft/settings/DftSettings.h" + +#include "storm-dft/settings/modules/DftIOSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/EigenEquationSolverSettings.h" +#include "storm/settings/modules/GmmxxEquationSolverSettings.h" +#include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/MinMaxEquationSolverSettings.h" +#include "storm/settings/modules/BisimulationSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" +#include "storm/settings/modules/GSPNSettings.h" +#include "storm/settings/modules/GSPNExportSettings.h" + + +namespace storm { + namespace settings { + void initializeDftSettings(std::string const& name, std::string const& executableName) { + storm::settings::mutableManager().setName(name, executableName); + + // Register relevant settings modules. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + // storm::settings::addModule(); + storm::settings::addModule(); + + // For translation into JANI via GSPN. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + } + + } +} diff --git a/src/storm-dft/settings/DftSettings.h b/src/storm-dft/settings/DftSettings.h new file mode 100644 index 000000000..8f67ec0b7 --- /dev/null +++ b/src/storm-dft/settings/DftSettings.h @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace storm { + namespace settings { + + void initializeDftSettings(std::string const& name, std::string const& executableName); + + } +} diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp deleted file mode 100644 index 1a8d59d70..000000000 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ /dev/null @@ -1,189 +0,0 @@ -#include "DFTSettings.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/SettingMemento.h" -#include "storm/settings/Option.h" -#include "storm/settings/OptionBuilder.h" -#include "storm/settings/ArgumentBuilder.h" -#include "storm/settings/Argument.h" - -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/IllegalArgumentValueException.h" - -namespace storm { - namespace settings { - namespace modules { - - const std::string DFTSettings::moduleName = "dft"; - const std::string DFTSettings::dftFileOptionName = "dftfile"; - const std::string DFTSettings::dftFileOptionShortName = "dft"; - const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json"; - const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson"; - const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction"; - const std::string DFTSettings::symmetryReductionOptionShortName = "symred"; - const std::string DFTSettings::modularisationOptionName = "modularisation"; - const std::string DFTSettings::disableDCOptionName = "disabledc"; - const std::string DFTSettings::approximationErrorOptionName = "approximation"; - const std::string DFTSettings::approximationErrorOptionShortName = "approx"; - const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic"; - const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime"; - const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf"; - const std::string DFTSettings::propProbabilityOptionName = "probability"; - const std::string DFTSettings::propTimeboundOptionName = "timebound"; - const std::string DFTSettings::propTimepointsOptionName = "timepoints"; - const std::string DFTSettings::minValueOptionName = "min"; - const std::string DFTSettings::maxValueOptionName = "max"; - const std::string DFTSettings::firstDependencyOptionName = "firstdep"; - const std::string DFTSettings::transformToGspnOptionName = "gspn"; - const std::string DFTSettings::exportToJsonOptionName = "export-json"; -#ifdef STORM_HAVE_Z3 - const std::string DFTSettings::solveWithSmtOptionName = "smt"; -#endif - - DFTSettings::DFTSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).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 Dont Care propagation.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); -#ifdef STORM_HAVE_Z3 - this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); -#endif - this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); - } - - bool DFTSettings::isDftFileSet() const { - return this->getOption(dftFileOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getDftFilename() const { - return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool DFTSettings::isDftJsonFileSet() const { - return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getDftJsonFilename() const { - return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool DFTSettings::useSymmetryReduction() const { - return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::useModularisation() const { - return this->getOption(modularisationOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isDisableDC() const { - return this->getOption(disableDCOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isApproximationErrorSet() const { - return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); - } - - double DFTSettings::getApproximationError() const { - return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); - } - - storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const { - if (!isApproximationErrorSet() || getApproximationError() == 0.0) { - // No approximation is done - return storm::builder::ApproximationHeuristic::NONE; - } - std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); - if (heuristicAsString == "depth") { - return storm::builder::ApproximationHeuristic::DEPTH; - } else if (heuristicAsString == "probability") { - return storm::builder::ApproximationHeuristic::PROBABILITY; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); - } - - bool DFTSettings::usePropExpectedTime() const { - return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::usePropProbability() const { - return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::usePropTimebound() const { - return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); - } - - double DFTSettings::getPropTimebound() const { - return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); - } - - bool DFTSettings::usePropTimepoints() const { - return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); - } - - std::vector DFTSettings::getPropTimepoints() const { - double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); - double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); - double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); - std::vector timepoints; - for (double time = starttime; time <= endtime; time += inc) { - timepoints.push_back(time); - } - return timepoints; - } - - bool DFTSettings::isComputeMinimalValue() const { - return this->getOption(minValueOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isComputeMaximalValue() const { - return this->getOption(maxValueOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isTakeFirstDependency() const { - return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); - } - -#ifdef STORM_HAVE_Z3 - bool DFTSettings::solveWithSMT() const { - return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); - } -#endif - - bool DFTSettings::isTransformToGspn() const { - return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isExportToJson() const { - return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getExportJsonFilename() const { - return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); - } - - void DFTSettings::finalize() { - } - - bool DFTSettings::check() const { - // Ensure that at most one of min or max is set - STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); - return true; - } - - } // namespace modules - } // namespace settings -} // namespace storm diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp new file mode 100644 index 000000000..cf656333d --- /dev/null +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -0,0 +1,123 @@ +#include "DftIOSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string DftIOSettings::moduleName = "dftIO"; + const std::string DftIOSettings::dftFileOptionName = "dftfile"; + const std::string DftIOSettings::dftFileOptionShortName = "dft"; + const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json"; + const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson"; + const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime"; + const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf"; + const std::string DftIOSettings::propProbabilityOptionName = "probability"; + const std::string DftIOSettings::propTimeboundOptionName = "timebound"; + const std::string DftIOSettings::propTimepointsOptionName = "timepoints"; + const std::string DftIOSettings::minValueOptionName = "min"; + const std::string DftIOSettings::maxValueOptionName = "max"; + const std::string DftIOSettings::transformToGspnOptionName = "gspn"; + const std::string DftIOSettings::exportToJsonOptionName = "export-json"; + + DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); + } + + bool DftIOSettings::isDftFileSet() const { + return this->getOption(dftFileOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getDftFilename() const { + return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool DftIOSettings::isDftJsonFileSet() const { + return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getDftJsonFilename() const { + return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool DftIOSettings::usePropExpectedTime() const { + return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::usePropProbability() const { + return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::usePropTimebound() const { + return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); + } + + double DftIOSettings::getPropTimebound() const { + return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); + } + + bool DftIOSettings::usePropTimepoints() const { + return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); + } + + std::vector DftIOSettings::getPropTimepoints() const { + double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); + double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); + double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); + std::vector timepoints; + for (double time = starttime; time <= endtime; time += inc) { + timepoints.push_back(time); + } + return timepoints; + } + + bool DftIOSettings::isComputeMinimalValue() const { + return this->getOption(minValueOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isComputeMaximalValue() const { + return this->getOption(maxValueOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isTransformToGspn() const { + return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isExportToJson() const { + return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getExportJsonFilename() const { + return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); + } + + void DftIOSettings::finalize() { + } + + bool DftIOSettings::check() const { + // Ensure that at most one of min or max is set + STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h similarity index 63% rename from src/storm-dft/settings/modules/DFTSettings.h rename to src/storm-dft/settings/modules/DftIOSettings.h index c04ef1a23..8a8fbcdd1 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -1,24 +1,21 @@ #pragma once -#include "storm-config.h" #include "storm/settings/modules/ModuleSettings.h" -#include "storm-dft/builder/DftExplorationHeuristic.h" - namespace storm { namespace settings { namespace modules { /*! - * This class represents the settings for DFT model checking. + * This class represents the settings for IO operations concerning DFTs. */ - class DFTSettings : public ModuleSettings { + class DftIOSettings : public ModuleSettings { public: /*! - * Creates a new set of DFT settings. + * Creates a new set of IO settings for DFTs. */ - DFTSettings(); + DftIOSettings(); /*! * Retrieves whether the dft file option was set. @@ -48,48 +45,6 @@ namespace storm { */ std::string getDftJsonFilename() const; - /*! - * Retrieves whether the option to use symmetry reduction is set. - * - * @return True iff the option was set. - */ - bool useSymmetryReduction() const; - - /*! - * Retrieves whether the option to use modularisation is set. - * - * @return True iff the option was set. - */ - bool useModularisation() const; - - /*! - * Retrieves whether the option to disable Dont Care propagation is set. - * - * @return True iff the option was set. - */ - bool isDisableDC() const; - - /*! - * Retrieves whether the option to compute an approximation is set. - * - * @return True iff the option was set. - */ - bool isApproximationErrorSet() const; - - /*! - * Retrieves the relative error allowed for approximating the model checking result. - * - * @return The allowed errorbound. - */ - double getApproximationError() const; - - /*! - * Retrieves the heuristic used for approximation. - * - * @return The heuristic to use. - */ - storm::builder::ApproximationHeuristic getApproximationHeuristic() const; - /*! * Retrieves whether the property expected time should be used. * @@ -146,13 +101,6 @@ namespace storm { */ bool isComputeMaximalValue() const; - /*! - * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. - * - * @return True iff the option was set. - */ - bool isTakeFirstDependency() const; - /*! * Retrieves whether the DFT should be transformed into a GSPN. * @@ -174,15 +122,6 @@ namespace storm { */ std::string getExportJsonFilename() const; -#ifdef STORM_HAVE_Z3 - /*! - * Retrieves whether the DFT should be checked via SMT. - * - * @return True iff the option was set. - */ - bool solveWithSMT() const; -#endif - bool check() const override; void finalize() override; @@ -195,13 +134,6 @@ namespace storm { static const std::string dftFileOptionShortName; static const std::string dftJsonFileOptionName; static const std::string dftJsonFileOptionShortName; - static const std::string symmetryReductionOptionName; - static const std::string symmetryReductionOptionShortName; - static const std::string modularisationOptionName; - static const std::string disableDCOptionName; - static const std::string approximationErrorOptionName; - static const std::string approximationErrorOptionShortName; - static const std::string approximationHeuristicOptionName; static const std::string propExpectedTimeOptionName; static const std::string propExpectedTimeOptionShortName; static const std::string propProbabilityOptionName; @@ -209,10 +141,6 @@ namespace storm { static const std::string propTimepointsOptionName; static const std::string minValueOptionName; static const std::string maxValueOptionName; - static const std::string firstDependencyOptionName; -#ifdef STORM_HAVE_Z3 - static const std::string solveWithSmtOptionName; -#endif static const std::string transformToGspnOptionName; static const std::string exportToJsonOptionName; diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp new file mode 100644 index 000000000..7c9ef14af --- /dev/null +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -0,0 +1,93 @@ +#include "FaultTreeSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string FaultTreeSettings::moduleName = "dft"; + const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction"; + const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred"; + const std::string FaultTreeSettings::modularisationOptionName = "modularisation"; + const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; + const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; + const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; + const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; + const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep"; +#ifdef STORM_HAVE_Z3 + const std::string FaultTreeSettings::solveWithSmtOptionName = "smt"; +#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, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); +#ifdef STORM_HAVE_Z3 + this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); +#endif + } + + bool FaultTreeSettings::useSymmetryReduction() const { + return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::useModularisation() const { + return this->getOption(modularisationOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::isDisableDC() const { + return this->getOption(disableDCOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::isApproximationErrorSet() const { + return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); + } + + double FaultTreeSettings::getApproximationError() const { + return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); + } + + storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const { + if (!isApproximationErrorSet() || getApproximationError() == 0.0) { + // No approximation is done + return storm::builder::ApproximationHeuristic::NONE; + } + std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); + if (heuristicAsString == "depth") { + return storm::builder::ApproximationHeuristic::DEPTH; + } else if (heuristicAsString == "probability") { + return storm::builder::ApproximationHeuristic::PROBABILITY; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); + } + + bool FaultTreeSettings::isTakeFirstDependency() const { + return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); + } + +#ifdef STORM_HAVE_Z3 + bool FaultTreeSettings::solveWithSMT() const { + return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); + } +#endif + + void FaultTreeSettings::finalize() { + } + + bool FaultTreeSettings::check() const { + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h new file mode 100644 index 000000000..171d5c38e --- /dev/null +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -0,0 +1,104 @@ +#pragma once + +#include "storm/settings/modules/ModuleSettings.h" +#include "storm-dft/builder/DftExplorationHeuristic.h" +#include "storm-config.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for DFT model checking. + */ + class FaultTreeSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of DFT settings. + */ + FaultTreeSettings(); + + /*! + * Retrieves whether the option to use symmetry reduction is set. + * + * @return True iff the option was set. + */ + bool useSymmetryReduction() const; + + /*! + * Retrieves whether the option to use modularisation is set. + * + * @return True iff the option was set. + */ + bool useModularisation() const; + + /*! + * Retrieves whether the option to disable Dont Care propagation is set. + * + * @return True iff the option was set. + */ + bool isDisableDC() const; + + /*! + * Retrieves whether the option to compute an approximation is set. + * + * @return True iff the option was set. + */ + bool isApproximationErrorSet() const; + + /*! + * Retrieves the relative error allowed for approximating the model checking result. + * + * @return The allowed errorbound. + */ + double getApproximationError() const; + + /*! + * Retrieves the heuristic used for approximation. + * + * @return The heuristic to use. + */ + storm::builder::ApproximationHeuristic getApproximationHeuristic() const; + + /*! + * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. + * + * @return True iff the option was set. + */ + bool isTakeFirstDependency() const; + +#ifdef STORM_HAVE_Z3 + /*! + * Retrieves whether the DFT should be checked via SMT. + * + * @return True iff the option was set. + */ + bool solveWithSMT() const; +#endif + + bool check() const override; + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string symmetryReductionOptionName; + static const std::string symmetryReductionOptionShortName; + static const std::string modularisationOptionName; + static const std::string disableDCOptionName; + static const std::string approximationErrorOptionName; + static const std::string approximationErrorOptionShortName; + static const std::string approximationHeuristicOptionName; + static const std::string firstDependencyOptionName; +#ifdef STORM_HAVE_Z3 + static const std::string solveWithSmtOptionName; +#endif + + }; + + } // namespace modules + } // namespace settings +} // namespace storm