From 79ce4075b38e58b0b3d08d75f58d7f19f8ad5c04 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 12 Sep 2016 14:17:38 +0000
Subject: [PATCH] Add a default implementation of
 ModelInfo.rewardStructHasTransitionRewards in DefaultModelGenerator (which
 returns true), plus some notes about this in the JavaDoc for related methods.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11806 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/DefaultModelGenerator.java |  7 +++++++
 prism/src/prism/ModelGenerator.java        | 11 +++++++----
 prism/src/prism/ModelInfo.java             |  6 ++++--
 3 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/prism/src/prism/DefaultModelGenerator.java b/prism/src/prism/DefaultModelGenerator.java
index 0184f450..bfb7705b 100644
--- a/prism/src/prism/DefaultModelGenerator.java
+++ b/prism/src/prism/DefaultModelGenerator.java
@@ -138,6 +138,13 @@ public abstract class DefaultModelGenerator implements ModelGenerator
 		return null;
 	}
 	
+	@Override
+	public boolean rewardStructHasTransitionRewards(int i)
+	{
+		// By default, assume that any reward structures that do exist may have transition rewards
+		return true;
+	}
+	
 	// Methods for ModelGenerator interface
 	
 	public boolean hasSingleInitialState() throws PrismException
diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java
index 00d910c2..7d341300 100644
--- a/prism/src/prism/ModelGenerator.java
+++ b/prism/src/prism/ModelGenerator.java
@@ -30,7 +30,6 @@ package prism;
 import java.util.List;
 
 import parser.State;
-import parser.VarList;
 
 /**
  * Interface for classes that generate a probabilistic model:
@@ -143,15 +142,19 @@ public interface ModelGenerator extends ModelInfo
 	public boolean isLabelTrue(int i) throws PrismException;
 	
 	/**
-	 * Get the state reward of the {@code r}th reward structure for state {@code state}.
+	 * Get the state reward of the {@code r}th reward structure for state {@code state}
+	 * ({@code r} is indexed from 0, not from 1 like at the user (property language) level).
 	 * @param r The index of the reward structure to use
 	 * @param state The state in which to evaluate the rewards 
 	 */
 	public double getStateReward(int r, State state) throws PrismException;
 	
 	/**
-	 * Get the state-action reward of the {@code r}th reward structure for state {@code state}
-	 * and action {@code action{.
+	 * Get the state-action reward of the {@code r}th reward structure for state {@code state} and action {@code action}
+	 * ({@code r} is indexed from 0, not from 1 like at the user (property language) level).
+	 * If a reward structure has no transition rewards, you can indicate this by implementing
+	 * the method {@link #rewardStructHasTransitionRewards(int)}, which may improve efficiency
+	 * and/or allow use of algorithms/implementations that do not support transition rewards rewards.
 	 * @param r The index of the reward structure to use
 	 * @param state The state in which to evaluate the rewards 
 	 * @param action The outgoing action label 
diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java
index c826737b..ba9a9565 100644
--- a/prism/src/prism/ModelInfo.java
+++ b/prism/src/prism/ModelInfo.java
@@ -140,9 +140,11 @@ public interface ModelInfo
 	public RewardStruct getRewardStruct(int i);
 
 	/**
-	 * Returns true if the reward structure with index i
+	 * Returns true if the reward structure with index i defines transition rewards.
 	 * (indexed from 0, not from 1 like at the user (property language) level)
-	 * defines transition rewards.
+	 * If this returns false, the model checker is allowed to ignore them (which may be more efficient).
+	 * If using an algorithm or implementation that does not support transition rewards,
+	 * you may need to return false here (as well as not defining transition rewards).
 	 */
 	public boolean rewardStructHasTransitionRewards(int i);