diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 533da8bf3..1f7359b7f 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -148,8 +148,8 @@ void processOptions() { // Add relevant event names from properties for (auto atomic : atomicLabels) { std::string label = atomic->getLabel(); - if (label == "failed") { - // Ignore as this label will always be added + if (label == "failed" or label == "skipped") { + // Ignore as these label will always be added if necessary } else { // Get name of event if (boost::ends_with(label, "_failed")) { diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index ca9415e48..efc51d89f 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -202,6 +202,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known."); } } + + auto ftSettings = storm::settings::getModule(); + if (ftSettings.isMaxDepthSet()) { + STORM_LOG_ASSERT(usedHeuristic == storm::builder::ApproximationHeuristic::DEPTH, "MaxDepth requires 'depth' exploration heuristic."); + approximationThreshold = ftSettings.getMaxDepth(); + } + exploreStateSpace(approximationThreshold); size_t stateSize = stateStorage.getNumberOfStates() + (this->uniqueFailedState ? 1 : 0); @@ -519,7 +526,16 @@ namespace storm { template std::shared_ptr> ExplicitDFTModelBuilder::getModel() { - STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); + if (storm::settings::getModule().isMaxDepthSet() && skippedStates.size() > 0) { + // Give skipped states separate label "skipped" + modelComponents.stateLabeling.addLabel("skipped"); + for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { + modelComponents.stateLabeling.addLabelToState("skipped", it->first); + } + } else{ + STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); + } + return createModel(false); } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index 140b0f175..b45c37498 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -24,24 +24,35 @@ namespace storm { const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; + const std::string FaultTreeSettings::maxDepthOptionName = "maxdepth"; 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, 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 Don't 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, firstDependencyOptionName, false, + "Avoid non-determinism by always taking the first possible dependency.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, relevantEventsOptionName, false, "Specifies the relevant events from the DFT.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString("").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", + "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString( + "").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, allowDCRelevantOptionName, false, "Allow Don't Care propagation for relevant events.").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, 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", "The name of the heuristic used for approximation.") - .setDefaultValueString("depth") - .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "probability", "bounddifference"})).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "The name of the heuristic used for approximation.") + .setDefaultValueString("depth") + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator( + {"depth", "probability", "bounddifference"})).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxDepthOptionName, false, "Maximal depth for state space exploration.").addArgument( + storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("depth", "The maximal depth.").build()).build()); #ifdef STORM_HAVE_Z3 this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); #endif @@ -64,7 +75,8 @@ namespace storm { } bool FaultTreeSettings::areRelevantEventsSet() const { - return this->getOption(relevantEventsOptionName).getHasOptionBeenSet() && (this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString() != ""); + return this->getOption(relevantEventsOptionName).getHasOptionBeenSet() && + (this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString() != ""); } std::vector FaultTreeSettings::getRelevantEvents() const { @@ -91,14 +103,24 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); } + bool FaultTreeSettings::isMaxDepthSet() const { + return this->getOption(maxDepthOptionName).getHasOptionBeenSet(); + } + + uint_fast64_t FaultTreeSettings::getMaxDepth() const { + return this->getOption(maxDepthOptionName).getArgumentByName("depth").getValueAsUnsignedInteger(); + } + 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() { @@ -107,6 +129,8 @@ namespace storm { bool FaultTreeSettings::check() const { // Ensure that disableDC and relevantEvents are not set at the same time STORM_LOG_THROW(!isDisableDC() || !areRelevantEventsSet(), storm::exceptions::InvalidSettingsException, "DisableDC and relevantSets can not both be set."); + STORM_LOG_THROW(!isMaxDepthSet() || getApproximationHeuristic() == storm::builder::ApproximationHeuristic::DEPTH, storm::exceptions::InvalidSettingsException, + "Maximal depth requires approximation heuristic depth."); return true; } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 16a726e04..5ed230bfb 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -82,6 +82,20 @@ namespace storm { */ storm::builder::ApproximationHeuristic getApproximationHeuristic() const; + /*! + * Retrieves whether the option to set a maximal exploration depth is set. + * + * @return True iff the option was set. + */ + bool isMaxDepthSet() const; + + /*! + * Retrieves the maximal exploration depth. + * + * @return The maximal exploration depth. + */ + uint_fast64_t getMaxDepth() const; + /*! * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. * @@ -118,6 +132,7 @@ namespace storm { static const std::string approximationErrorOptionName; static const std::string approximationErrorOptionShortName; static const std::string approximationHeuristicOptionName; + static const std::string maxDepthOptionName; static const std::string firstDependencyOptionName; #ifdef STORM_HAVE_Z3 static const std::string solveWithSmtOptionName;