From 9833da842aba309381eb939536d1145e58ac5b06 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 28 Feb 2011 18:22:32 +0000
Subject: [PATCH] Simulator bugfix: local nondeterminism handled incorrectly.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2486 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/simulator/ChoiceListFlexi.java | 21 +++++++++++++++++++++
 prism/src/simulator/Updater.java         |  5 +++--
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/prism/src/simulator/ChoiceListFlexi.java b/prism/src/simulator/ChoiceListFlexi.java
index 7ec0fa0e..2aa4ced2 100644
--- a/prism/src/simulator/ChoiceListFlexi.java
+++ b/prism/src/simulator/ChoiceListFlexi.java
@@ -58,6 +58,27 @@ public class ChoiceListFlexi implements Choice
 		probability = new ArrayList<Double>();
 	}
 
+	/**
+	 * Copy constructor.
+	 * NB: Does a shallow, not deep, copy with respect to references to Update objects.
+	 */
+	public ChoiceListFlexi(ChoiceListFlexi ch)
+	{
+		moduleOrActionIndex = ch.moduleOrActionIndex;
+		updates = new ArrayList<List<Update>>(ch.updates.size());
+		for (List<Update> list : ch.updates) {
+			List<Update> listNew = new ArrayList<Update>(list.size()); 
+			updates.add(listNew);
+			for (Update up : list) {
+				listNew.add(up);
+			}
+		}
+		probability = new ArrayList<Double>(ch.size());
+		for (double p : ch.probability) {
+			probability.add(p);
+		}
+	}
+
 	// Set methods
 
 	/**
diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java
index a0ae0e65..78c159fb 100644
--- a/prism/src/simulator/Updater.java
+++ b/prism/src/simulator/Updater.java
@@ -178,12 +178,13 @@ public class Updater
 						n = chs.size();
 						for (k = 0; k < count - 1; k++)
 							for (l = 0; l < n; l++)
-								chs.add(chs.get(l));
+								chs.add(new ChoiceListFlexi(chs.get(l)));
 						// Products with existing choices
 						for (k = 0; k < count; k++) {
 							Updates ups = updateLists.get(j).get(i).get(k);
-							for (l = 0; l < n; l++)
+							for (l = 0; l < n; l++) {
 								processUpdatesAndAddToProduct(ups, state, chs.get(k * n + l));
+							}
 						}
 					}
 				}