From 8f7e21c108d3ca2de2dc703bee5a019521cb9e9f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 Jan 2015 09:52:22 +0100
Subject: [PATCH] Small hack that prevents creating atomic propositions like
'true'. This will be solved differently in master soon.
Former-commit-id: e99010a4853844e1081a21956bb1c9ac38eaa97b
---
.../DeterministicModelBisimulationDecomposition.cpp | 7 +++++++
1 file changed, 7 insertions(+)
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<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded);
+ std::set<std::string> atomicPropositions;
+ if (phiLabel != "true" && phiLabel != "false") {
+ atomicPropositions.insert(phiLabel);
+ }
+ if (psiLabel != "true" && phiLabel != "false") {
+ atomicPropositions.insert(psiLabel);
+ }
partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient);
}