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

@@ -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
 
 	/**

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));
+							}
 						}
 					}
 				}