vector was initialized wrong

moves-rwth · Jan 24, 2025 · bc5f461 · bc5f461
1 parent 541f17b
commit bc5f461
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 6 deletions.
diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
@@ -108,7 +108,7 @@ storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeA
 
         for (uint64_t i = 0; i < transitionMatrix.getRowGroupCount(); i++) {
             uint64_t mec_index = state_to_mec[i];
-            if (mec_index != MAX && is_amec[mec_index]) {
+            if (mec_index == MAX || is_amec[mec_index]) {
                 allowed.set(i, false);
             }
         }

diff --git a/src/storm/storage/MaximalEndComponentDecomposition.cpp b/src/storm/storage/MaximalEndComponentDecomposition.cpp
@@ -147,18 +147,14 @@ void MaximalEndComponentDecomposition<ValueType>::performMaximalEndComponentDeco
         }
         std::vector<uint64_t> offset(sccDecRes.sccCount);
 
-        for (auto state: remainingEcCandidates) {
-            auto const sccIndex = sccDecRes.stateToSccMapping[state];
-            ecSccStates[ecSccIndexToStateIndex[sccIndex] + offset[sccIndex]++] = state;
-        }
-
         remainingEcCandidates = sccDecRes.nonTrivialStates;
         storm::storage::BitVector ecSccIndices(sccDecRes.sccCount, true);
         storm::storage::BitVector nonTrivSccIndices(sccDecRes.sccCount, false);
         // find the choices that do not stay in their SCC
         for (auto state : remainingEcCandidates) {
             auto const sccIndex = sccDecRes.stateToSccMapping[state];
             nonTrivSccIndices.set(sccIndex, true);
+            ecSccStates[ecSccIndexToStateIndex[sccIndex] + offset[sccIndex]++] = state;
             bool stateCanStayInScc = false;
             for (auto const choice : transitionMatrix.getRowGroupIndices(state)) {
                 if (!ecChoices.get(choice)) {