From 69e2aac5c948e1b05b5cabcf11a8be1f02133e6d Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 7 Feb 2017 19:00:10 +0100
Subject: [PATCH] Fixed labeling when using multiple failed states

---
 src/storm-dft/builder/ExplicitDFTModelBuilder.h    |  2 +-
 .../builder/ExplicitDFTModelBuilderApprox.cpp      |  7 ++++---
 .../builder/ExplicitDFTModelBuilderApprox.h        | 14 +++++++++++++-
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
index d3d191a8a..d61043368 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -60,7 +60,7 @@ namespace storm {
             storm::storage::BitVectorHashMap<uint_fast64_t> mStates;
             std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
             size_t newIndex = 0;
-            bool mergeFailedStates = true;
+            bool mergeFailedStates = false;
             bool enableDC = true;
             size_t failedIndex = 0;
             size_t initialStateIndex = 0;
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index 194372a30..48e564af0 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -169,7 +169,7 @@ namespace storm {
             modelComponents.deterministicModel = generator.isDeterministicModel();
 
             // Fix the entries in the transition matrix according to the mapping of ids to row group indices
-            STORM_LOG_ASSERT(matrixBuilder.stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped.");
+            STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
             // TODO Matthias: do not consider all rows?
             STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset);
             matrixBuilder.remap();
@@ -230,7 +230,7 @@ namespace storm {
             StateType skippedIndex = nrExpandedStates;
             std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStatesNew;
             for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) {
-                StateType index = matrixBuilder.stateRemapping[id];
+                StateType index = matrixBuilder.getRemapping(id);
                 auto itFind = skippedStates.find(index);
                 if (itFind != skippedStates.end()) {
                     // Set new mapping for skipped state
@@ -405,6 +405,7 @@ namespace storm {
             modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount());
             // Initial state
             modelComponents.stateLabeling.addLabel("init");
+            STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
             modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
             // Label all states corresponding to their status (failed, failsafe, failed BE)
             if(labelOpts.buildFailLabel) {
@@ -428,7 +429,7 @@ namespace storm {
             }
             for (auto const& stateIdPair : stateStorage.stateToId) {
                 storm::storage::BitVector state = stateIdPair.first;
-                size_t stateId = stateIdPair.second;
+                size_t stateId = matrixBuilder.getRemapping(stateIdPair.second);
                 if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) {
                     modelComponents.stateLabeling.addLabelToState("failed", stateId);
                 }
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
index 52bcbf2c9..6cf765d40 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
@@ -116,6 +116,18 @@ namespace storm {
                     return currentRowGroup;
                 }
 
+                /*!
+                 * Get the remapped state for the given id.
+                 *
+                 * @param id State.
+                 *
+                 * @return Remapped index.
+                 */
+                StateType getRemapping(StateType id) {
+                    STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
+                    return stateRemapping[id];
+                }
+
                 // Matrix builder.
                 storm::storage::SparseMatrixBuilder<ValueType> builder;
 
@@ -287,7 +299,7 @@ namespace storm {
             bool enableDC = true;
 
             //TODO Matthias: make changeable
-            const bool mergeFailedStates = true;
+            const bool mergeFailedStates = false;
 
             // Heuristic used for approximation
             storm::builder::ApproximationHeuristic usedHeuristic;