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

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

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 

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