From 18d3c06f1268af5879fc3caf0cc9653a3cb255bc Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 11 Jun 2016 00:39:47 +0200 Subject: [PATCH] fix in state duplicator Former-commit-id: 255e6c430cd0c618f96bd887ccc3ce9d12b540a8 --- src/transformer/StateDuplicator.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/transformer/StateDuplicator.h b/src/transformer/StateDuplicator.h index 708663270..6733fd424 100644 --- a/src/transformer/StateDuplicator.h +++ b/src/transformer/StateDuplicator.h @@ -170,9 +170,14 @@ namespace storm { for(auto const& entry : originalMatrix.getRow(oldRow)){ if(result.firstCopy.get(newState) && !result.gateStates.get(entry.getColumn())){ builder.addNextValue(newRow, result.firstCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); - } else { + } else if (!result.duplicatedStates.get(entry.getColumn())){ + builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); + } + } + //To add values in the right order, transitions to duplicated states have to be added in a second run. + for(auto const& entry : originalMatrix.getRow(oldRow)){ + if (result.secondCopy.get(newState) && result.duplicatedStates.get(entry.getColumn())){ builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); - } } ++newRow;