diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 5ad54a0f5..08d0f8786 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1584,8 +1584,10 @@ namespace storm { */ static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet) { + bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp); + std::vector> resultLabelSet; - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, model.getTransitionMatrix().getColumnCount(), 0, true, true, model.getTransitionMatrix().getRowGroupCount()); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, model.getTransitionMatrix().getColumnCount(), 0, true, customRowGrouping, model.getTransitionMatrix().getRowGroupCount()); // Check for each choice of each state, whether the choice commands are fully contained in the given command set. uint_fast64_t currentRow = 0; @@ -1611,7 +1613,9 @@ namespace storm { // If no choice of the current state may be taken, we insert a self-loop to the state instead. if (!stateHasValidChoice) { - transitionMatrixBuilder.newRowGroup(currentRow); + if (customRowGrouping) { + transitionMatrixBuilder.newRowGroup(currentRow); + } transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::one()); // Insert an empty label set for this choice resultLabelSet.emplace_back();