diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index f4af34ed1..bbfe99dd6 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -12,6 +12,7 @@ namespace storm { template DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), uniqueFailedState(false) { deterministicModel = !mDft.canHaveNondeterminism(); + mTakeFirstDependency = storm::settings::getModule().isTakeFirstDependency(); } template @@ -48,11 +49,11 @@ namespace storm { STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state)); // Initialization bool hasDependencies = state->getFailableElements().hasDependencies(); - return exploreState(stateToIdCallback, hasDependencies); + return exploreState(stateToIdCallback, hasDependencies, mTakeFirstDependency); } template - StateBehavior DftNextStateGenerator::exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies) { + StateBehavior DftNextStateGenerator::exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies, bool takeFirstDependency) { // Prepare the result, in case we return early. StateBehavior result; @@ -78,8 +79,7 @@ namespace storm { // Let BE fail bool isFirst = true; while (!state->getFailableElements().isEnd()) { - //TODO outside - if (storm::settings::getModule().isTakeFirstDependency() && exploreDependencies && !isFirst) { + if (takeFirstDependency && exploreDependencies && !isFirst) { // We discard further exploration as we already chose one dependent event break; } @@ -208,7 +208,7 @@ namespace storm { if (result.empty()) { // Dependencies might have been prevented from sequence enforcer // -> explore BEs now - return exploreState(stateToIdCallback, false); + return exploreState(stateToIdCallback, false, takeFirstDependency); } } else { if (choice.size() == 0) { diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index 9fab2ee1f..fc7580a13 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -31,6 +31,12 @@ namespace storm { void load(storm::storage::BitVector const& state); void load(DFTStatePointer const& state); + + /*! + * Expand and explore current state. + * @param stateToIdCallback Callback function which adds new state and returns the corresponding id. + * @return StateBehavior containing successor choices and distributions. + */ StateBehavior expand(StateToIdCallback const& stateToIdCallback); /*! @@ -44,7 +50,14 @@ namespace storm { private: - StateBehavior exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies); + /*! + * Explore current state and generate all successor states. + * @param stateToIdCallback Callback function which adds new state and returns the corresponding id. + * @param exploreDependencies Flag indicating whether failures due to dependencies or due to BEs should be explored. + * @param takeFirstDependency If true, instead of exploring all possible orders of dependency failures, a fixed order is explored where always the first dependency is considered. + * @return StateBehavior containing successor choices and distributions. + */ + StateBehavior exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies, bool takeFirstDependency); // The dft used for the generation of next states. storm::storage::DFT const& mDft; @@ -55,12 +68,15 @@ namespace storm { // Current state DFTStatePointer state; - // Flag indication if all failed states should be merged into one unique failed state. + // Flag indicating whether all failed states should be merged into one unique failed state. bool uniqueFailedState; - // Flag indicating if the model is deterministic. + // Flag indicating whether the model is deterministic. bool deterministicModel = false; + // Flag indicating whether only the first dependency (instead of all) should be explored. + bool mTakeFirstDependency = false; + }; }