From f5b7554590f2ecc765d0ed44ceda4bab3da392d9 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 29 Jan 2015 18:06:03 +0100
Subject: [PATCH] Minor bugfix for conditional probability computation.

Former-commit-id: c0b103e2aa9ae788429a98c87cd1895a6b5a3cd9
---
 .../reachability/SparseDtmcEliminationModelChecker.cpp      | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 86ca64a6b..cad821cb5 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -254,6 +254,12 @@ namespace storm {
             
             // The states we want to eliminate are those that are tagged with "maybe" but are not a phi or psi state.
             phiStates = phiStates % maybeStates;
+            
+            // If there are no phi states in the reduced model, the conditional probability is trivially zero.
+            if (phiStates.empty()) {
+                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, storm::utility::zero<ValueType>()));
+            }
+            
             psiStates = psiStates % maybeStates;
             
             // Keep only the states that we do not eliminate in the maybe states.