From 40212bb7e6ad3de6e6c6dee4f28ca19dc988afd2 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 17 Feb 2017 20:22:44 +0100
Subject: [PATCH] Added possibility to avoid non-determinism by only taking the
 first dependency

---
 src/storm-dft/generator/DftNextStateGenerator.cpp | 6 ++++++
 src/storm-dft/settings/modules/DFTSettings.cpp    | 6 ++++++
 src/storm-dft/settings/modules/DFTSettings.h      | 8 ++++++++
 3 files changed, 20 insertions(+)

diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index c89368099..9e9aa7056 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -3,6 +3,8 @@
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotImplementedException.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm-dft/settings/modules/DFTSettings.h"
 
 namespace storm {
     namespace generator {
@@ -69,6 +71,10 @@ namespace storm {
 
             // Let BE fail
             while (currentFailable < failableCount) {
+                if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
+                    // We discard further exploration as we already chose one dependent event
+                    break;
+                }
                 STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
 
                 // Construct new state as copy from original one
diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp
index e20df83ec..1a8d59d70 100644
--- a/src/storm-dft/settings/modules/DFTSettings.cpp
+++ b/src/storm-dft/settings/modules/DFTSettings.cpp
@@ -33,6 +33,7 @@ namespace storm {
             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
@@ -47,6 +48,7 @@ namespace storm {
                 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());
@@ -151,6 +153,10 @@ namespace storm {
                 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();
diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h
index 662039e0f..c04ef1a23 100644
--- a/src/storm-dft/settings/modules/DFTSettings.h
+++ b/src/storm-dft/settings/modules/DFTSettings.h
@@ -146,6 +146,13 @@ 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.
                  *
@@ -202,6 +209,7 @@ 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