diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index f41582ef9..5b4339e78 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -614,6 +614,13 @@ namespace storm { storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded); + std::set atomicPropositions; + if (phiLabel != "true" && phiLabel != "false") { + atomicPropositions.insert(phiLabel); + } + if (psiLabel != "true" && phiLabel != "false") { + atomicPropositions.insert(psiLabel); + } partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient); }