From 892ecc31e4824828bcf98eb258b2ea83a241d23f Mon Sep 17 00:00:00 2001
From: Ernst Moritz Hahn <emhahn@cs.ox.ac.uk>
Date: Sat, 10 Jan 2015 00:55:58 +0000
Subject: [PATCH] fix for dtmcs with overlapping commands

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9516 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/param/ModelBuilder.java | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java
index f13b41f9..50866b02 100644
--- a/prism/src/param/ModelBuilder.java
+++ b/prism/src/param/ModelBuilder.java
@@ -333,6 +333,7 @@ public final class ModelBuilder extends PrismComponent
 		}
 
 		boolean isNonDet = modelType == ModelType.MDP;
+		boolean isContinuous = modelType == ModelType.CTMC;
 		StateStorage<State> states = new IndexedSet<State>(true);
 		reserveMemoryAndExploreStates(modulesFile, model, modelType, engine, states);
 		int[] permut = states.buildSortingPermutation();
@@ -381,7 +382,7 @@ public final class ModelBuilder extends PrismComponent
 					model.addTransition(permut[states.get(stateNew)], probFn, action);
 				}
 				if (isNonDet) {
-					model.setSumLeaving(sumOut);
+					model.setSumLeaving(isContinuous ? sumOut : functionFactory.getOne());
 					model.finishChoice();
 				}
 			}
@@ -389,12 +390,12 @@ public final class ModelBuilder extends PrismComponent
 				model.addDeadlockState(stateNr);
 				model.addTransition(stateNr, functionFactory.getOne(), null);
 				if (isNonDet) {
-					model.setSumLeaving(sumOut);
+					model.setSumLeaving(isContinuous ? sumOut : functionFactory.getOne());
 					model.finishChoice();
 				}
 			}
 			if (!isNonDet) {
-				model.setSumLeaving(sumOut);
+				model.setSumLeaving(isContinuous ? sumOut : functionFactory.getOne());
 				model.finishChoice();
 			}
 			model.finishState();