From 6935798edf632c440a87448096765af87c652010 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 7 Sep 2016 14:13:05 +0000
Subject: [PATCH] explicit.ProbModelChecker: provide constructRewards(model,
 rewardStructureIndex)

Deprecate the previous methods using RewardStruct, as those don't work with
arbitrary model generators.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11784 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/ProbModelChecker.java | 37 ++++++++++++++++++++++--
 1 file changed, 35 insertions(+), 2 deletions(-)

diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index 3d4c7f79..4ed031a4 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -851,8 +851,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		// Build rewards
 		int r = expr.getRewardStructIndexByIndexObject(modelInfo, constantValues);
 		mainLog.println("Building reward structure...");
-		ConstructRewards constructRewards = new ConstructRewards(mainLog);
-		Rewards rewards = constructRewards.buildRewardStructure(model, modelGen, r);
+		Rewards rewards = constructRewards(model, r);
 
 		// Compute rewards
 		StateValues rews = checkRewardFormula(model, rewards, expr.getExpression(), minMax, statesOfInterest);
@@ -875,9 +874,39 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 	}
 
+	/**
+	 * Construct rewards for the reward structure with index r of the model generator and a model.
+	 * Ensures non-negative rewards.
+	 * <br>
+	 * Note: Relies on the stored ModelGenerator for constructing the reward structure.
+	 */
+	protected Rewards constructRewards(Model model, int r) throws PrismException
+	{
+		return constructRewards(model, r, false);
+	}
+
+	/**
+	 * Construct rewards for the reward structure with index r of the model generator and a model.
+	 * <br>
+	 * If {@code allowNegativeRewards} is true, the rewards may be positive and negative, i.e., weights.
+	 * <br>
+	 * Note: Relies on the stored ModelGenerator for constructing the reward structure.
+	 */
+	protected Rewards constructRewards(Model model, int r, boolean allowNegativeRewards) throws PrismException
+	{
+		ConstructRewards constructRewards = new ConstructRewards(mainLog);
+		if (allowNegativeRewards)
+			constructRewards.allowNegativeRewards();
+		return constructRewards.buildRewardStructure(model, modelGen, r);
+	}
+
 	/**
 	 * Construct rewards from a (non-negative) reward structure and a model.
+	 * <br>
+	 * Note: Deprecated, use the methods with reward structure index r instead
+	 * to allow construction from model generators.
 	 */
+	@Deprecated
 	protected Rewards constructRewards(Model model, RewardStruct rewStruct) throws PrismException
 	{
 		return constructRewards(model, rewStruct, false);
@@ -887,7 +916,11 @@ public class ProbModelChecker extends NonProbModelChecker
 	 * Construct rewards from a reward structure and a model.
 	 * <br>
 	 * If {@code allowNegativeRewards} is true, the rewards may be positive and negative, i.e., weights.
+	 * <br>
+	 * Note: Deprecated, use the methods with reward structure index r instead
+	 * to allow construction from model generators.
 	 */
+	@Deprecated
 	protected Rewards constructRewards(Model model, RewardStruct rewStruct, boolean allowNegativeRewards) throws PrismException
 	{
 		Rewards rewards;