From 08859bd3e6c07f4cddfa786f6da0ff06add34089 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 29 May 2019 18:34:05 +0200 Subject: [PATCH] Fixed bug in computation of symmetry groups. Thanks to Enno Ruijters for pointing out this issue. --- src/storm-dft/storage/dft/DFTStateGenerationInfo.h | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h index 626591768..eb345d0a0 100644 --- a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h +++ b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h @@ -124,16 +124,20 @@ namespace storm { size_t parentLength = mSymmetries[j].first; // Check if child lies in parent if (parentStart <= childStart && childStart + childLength < parentStart + parentLength) { + // We add the symmetry of the child to all symmetric elements in the parent std::vector> newSymmetries; + // Start iteration at 1, because symmetry for child at 0 is already included for (size_t index = 1; index < mSymmetries[j].second.size(); ++index) { - // Get symmetric start by applying the bijection std::vector newStarts; + // Apply child symmetry to all symmetric elements of parent for (size_t symmetryStarts : mSymmetries[i].second) { - newStarts.push_back(symmetryStarts + mSymmetries[j].second[index]); + // Get symmetric element by applying the bijection + size_t symmetryOffset = symmetryStarts - parentStart; + newStarts.push_back(mSymmetries[j].second[index] + symmetryOffset); } newSymmetries.push_back(newStarts); } - // Insert after child + // Insert new symmetry after child for (size_t index = 0; index < newSymmetries.size(); ++index) { mSymmetries.insert(mSymmetries.begin() + i + 1 + index, std::make_pair(childLength, newSymmetries[index])); }