Fixed smaller bugs

Former-commit-id: 4c9c22bca1

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -441,17 +441,22 @@ namespace storm {
             if (stateStorage.stateToId.contains(state->status())) {
                 // State already exists
                 stateId = stateStorage.stateToId.getValue(state->status());
-                STORM_LOG_TRACE("State " << dft.getStateString(state) << " already exists");
-
-                if (!changed && statesNotExplored.at(stateId)->isPseudoState()) {
-                    // Create pseudo state now
-                    STORM_LOG_ASSERT(statesNotExplored.at(stateId)->getId() == stateId, "Ids do not match.");
-                    STORM_LOG_ASSERT(statesNotExplored.at(stateId)->status() == state->status(), "Pseudo states do not coincide.");
-                    state->setId(stateId);
-                    // Update mapping to map to concrete state now
-                    statesNotExplored[stateId] = state;
-                    // We do not push the new state on the exploration queue as the pseudo state was already pushed
-                    STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state));
+                STORM_LOG_TRACE("State " << dft.getStateString(state) << " with id " << stateId << " already exists");
+                if (!changed) {
+                    // Check if state is pseudo state
+                    // If state is explored already the possible pseudo state was already constructed
+                    auto iter = statesNotExplored.find(stateId);
+                    if (iter != statesNotExplored.end() && iter->second->isPseudoState()) {
+                        // Create pseudo state now
+                        STORM_LOG_ASSERT(iter->second->getId() == stateId, "Ids do not match.");
+                        STORM_LOG_ASSERT(iter->second->status() == state->status(), "Pseudo states do not coincide.");
+                        state->setId(stateId);
+                        // Update mapping to map to concrete state now
+                        statesNotExplored[stateId] = state;
+                        // TODO Matthias: copy explorationHeuristic
+                        // We do not push the new state on the exploration queue as the pseudo state was already pushed
+                        STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state));
+                    }
                 }
             } else {
                 // State does not exist yet

src/storage/DynamicPriorityQueue.h

@@ -60,6 +60,10 @@ namespace storm {
                 return item;
             }
 
+            Container getContainer() const {
+                return container;
+            }
+
         };
     }
 }

src/storage/dft/DFT.cpp

@@ -481,8 +481,7 @@ namespace storm {
                         } else {
                             useId = getChild(elem->id(), nrUsedChild);
                         }
-                        bool isActive = status[stateGenerationInfo.getSpareActivationIndex(useId)];
-                        if(useId == elem->id() || isActive) {
+                        if(useId == elem->id() || status[stateGenerationInfo.getSpareActivationIndex(useId)]) {
                             stream << "actively ";
                         }
                         stream << "using " << useId << "]";

src/storage/dft/DFTState.cpp

@@ -44,6 +44,11 @@ namespace storm {
         template<typename ValueType>
         void DFTState<ValueType>::construct() {
             STORM_LOG_TRACE("Construct concrete state from pseudo state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId));
+            // Clear information from pseudo state
+            mCurrentlyFailableBE.clear();
+            mCurrentlyNotFailableBE.clear();
+            mFailableDependencies.clear();
+            mUsedRepresentants.clear();
             STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed.");
             for(size_t index = 0; index < mDft.nrElements(); ++index) {
                 // Initialize currently failable BE