From f30da8e7287fb260c94a640e1760aecc0b0ce1ec Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 28 Aug 2017 12:45:48 +0200
Subject: [PATCH] param / exact: perform initial scheduler computation for
 policy iteration independently of the regions

---
 prism/src/param/Scheduler.java     | 14 +++++++++++++-
 prism/src/param/ValueComputer.java | 10 ++++++----
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/prism/src/param/Scheduler.java b/prism/src/param/Scheduler.java
index 5d856cb5..22fc895b 100644
--- a/prism/src/param/Scheduler.java
+++ b/prism/src/param/Scheduler.java
@@ -49,7 +49,19 @@ final class Scheduler {
 			choices[state] = model.stateEnd(state) - 1;
 		}
 	}
-	
+
+	/** Copy constructor */
+	Scheduler(Scheduler other)
+	{
+		choices = other.choices.clone();
+	}
+
+	@Override
+	public Scheduler clone()
+	{
+		return new Scheduler(this);
+	}
+
 	/**
 	 * Set choice for given state.
 	 * 
diff --git a/prism/src/param/ValueComputer.java b/prism/src/param/ValueComputer.java
index 8c1f45dc..1582edf5 100644
--- a/prism/src/param/ValueComputer.java
+++ b/prism/src/param/ValueComputer.java
@@ -286,10 +286,13 @@ final class ValueComputer extends PrismComponent
 			}
 		}
 
+		Scheduler initialScheduler = new Scheduler(model);
+		precomputeScheduler(model, initialScheduler, b1, b2, rew, min);
+
 		while (volume.compareTo(requiredVolume) == -1) {
 			Region currentRegion = todo.poll();
 			Point midPoint = ((BoxRegion)currentRegion).getMidPoint();
-			Scheduler scheduler = computeOptConcreteReachScheduler(midPoint, model, b1, b2, min, rew);
+			Scheduler scheduler = computeOptConcreteReachScheduler(midPoint, model, b1, b2, min, rew, initialScheduler);
 			ResultCacheEntry resultCacheEntry = lookupValues(PropType.REACH, b1, b2, rew, scheduler, min);
 			Function[] compare;
 			StateValues values;
@@ -360,7 +363,7 @@ final class ValueComputer extends PrismComponent
 		return resultCacheEntry;
 	}
 
-	Scheduler computeOptConcreteReachScheduler(Point point, ParamModel model, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew) throws PrismException
+	Scheduler computeOptConcreteReachScheduler(Point point, ParamModel model, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew, Scheduler initialScheduler) throws PrismException
 	{
 		ParamModel concrete = model.instantiate(point);
 		ParamRewardStruct rewConcrete = null;
@@ -372,8 +375,7 @@ final class ValueComputer extends PrismComponent
 		if (scheduler != null) {
 			return scheduler;
 		}
-		scheduler = new Scheduler(concrete);
-		precomputeScheduler(concrete, scheduler, b1, b2, rew, min);
+		scheduler = initialScheduler.clone();
 		boolean changed = true;
 		while (changed) {
 			MutablePMC pmc = buildAlterablePMCForReach(concrete, b1, b2, scheduler, rew);