From ee023576126f80b2705ae5ff94b6c69eef34b64d Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 10 Apr 2019 17:51:56 +0200
Subject: [PATCH] Allow empty choices due to restrictions in state exploration
---
src/storm-dft/generator/DftNextStateGenerator.cpp | 9 ++++++++-
src/storm-dft/storage/dft/DFT.cpp | 3 ++-
2 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 495631817..1e9a53045 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -204,7 +204,14 @@ namespace storm {
return exploreState(stateToIdCallback, false);
}
} else {
- STORM_LOG_ASSERT(choice.size() > 0, "No transitions were generated");
+ if (choice.size() == 0) {
+ // No transition was generated
+ STORM_LOG_TRACE("No transitions were generated.");
+ // Add self loop
+ choice.addProbability(state->getId(), storm::utility::one<ValueType>());
+ STORM_LOG_TRACE("Added self loop for " << state->getId());
+ }
+ STORM_LOG_ASSERT(choice.size() > 0, "At least one choice should have been generated.");
// Add all rates as one choice
result.addChoice(std::move(choice));
}
diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 6a926e3a3..8ae059104 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -18,9 +18,10 @@ namespace storm {
template<typename ValueType>
DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) {
+ // Check that ids correspond to indices in the element vector
STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect.");
size_t nrRepresentatives = 0;
-
+
for (auto& elem : mElements) {
if (isRepresentative(elem->id())) {
++nrRepresentatives;