From 2768d15f4f898772e61b63f8186f657c4180e653 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 29 Dec 2018 19:33:49 +0100
Subject: [PATCH] fixing minor issue in symboiic bisimulation relation pointed
 out by Tim

---
 .../NondeterministicModelPartitionRefiner.cpp            | 7 +++++--
 .../bisimulation/NondeterministicModelPartitionRefiner.h | 9 ++++++---
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
index d047acfde..c5860ba9a 100644
--- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
+++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
@@ -8,7 +8,7 @@ namespace storm {
         namespace bisimulation {
             
             template<storm::dd::DdType DdType, typename ValueType>
-            NondeterministicModelPartitionRefiner<DdType, ValueType>::NondeterministicModelPartitionRefiner(storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(model, initialStatePartition), model(model), choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(model, initialStatePartition.getBlockVariables())), stateSignatureRefiner(model.getManager(), this->statePartition.getBlockVariable(), model.getRowVariables(), model.getColumnVariables(), true) {
+            NondeterministicModelPartitionRefiner<DdType, ValueType>::NondeterministicModelPartitionRefiner(storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(model, initialStatePartition), model(model), choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(model, initialStatePartition.getBlockVariables())), stateSignatureRefiner(model.getManager(), this->statePartition.getBlockVariable(), model.getRowVariables(), model.getColumnVariables(), true), statePartitonHasBeenRefinedOnce(false) {
 
                 // For Markov automata, we refine the state partition wrt. to their exit rates.
                 if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
@@ -29,7 +29,9 @@ namespace storm {
                 STORM_LOG_TRACE("Refining choice partition.");
                 Partition<DdType, ValueType> newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, this->choicePartition, this->statePartition, mode);
                 
-                if (newChoicePartition.getNumberOfBlocks() == choicePartition.getNumberOfBlocks()) {
+                // If the choice partition has become stable in an iteration that is not the starting one, we have
+                // reached a fixed point and can return.
+                if (newChoicePartition.getNumberOfBlocks() == choicePartition.getNumberOfBlocks() && statePartitonHasBeenRefinedOnce) {
                     this->status = Status::FixedPoint;
                     return false;
                 } else {
@@ -52,6 +54,7 @@ namespace storm {
                     STORM_LOG_TRACE("Refining state partition.");
                     auto refinementStart = std::chrono::high_resolution_clock::now();
                     Partition<DdType, ValueType> newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition);
+                    statePartitonHasBeenRefinedOnce = true;
                     auto refinementEnd = std::chrono::high_resolution_clock::now();
                     
                     auto signatureTime = std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h
index 0dae7f90e..d6c6d6274 100644
--- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h
+++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h
@@ -36,14 +36,17 @@ namespace storm {
                 
                 virtual bool refineWrtStateRewards(storm::dd::Add<DdType, ValueType> const& stateRewards) override;
                 
-                // The model to refine.
+                /// The model to refine.
                 storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model;
                 
-                // The choice partition in the refinement process.
+                /// The choice partition in the refinement process.
                 Partition<DdType, ValueType> choicePartition;
 
-                // The object used to refine the state partition based on the signatures.
+                /// The object used to refine the state partition based on the signatures.
                 SignatureRefiner<DdType, ValueType> stateSignatureRefiner;
+                
+                /// A flag indicating whether the state partition has been refined at least once.
+                bool statePartitonHasBeenRefinedOnce;
             };
             
         }