Maximal exploration depth can be specified for state space generation

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

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<storm::settings::modules::FaultTreeSettings>();
+            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<typename ValueType, typename StateType>
         std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModel() {
-            STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states");
+            if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().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);
         }
 

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<std::string> 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;
             }
 

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;