Check for transition reward consistency when importing from .trew files.

It is assumed that rewards are the same for all successor states from
the same state-choice pair, since we don't support state-choice-state
rewards yet. So the explicit engine now checks that this is the case
when importing a .trew file.

In fact, the symbolic engines _can_ import these (and a check is actually
a bit tricky), so we don't check for the symbolic engines.

prism/src/explicit/ExplicitFiles2Rewards.java

@@ -30,6 +30,7 @@
 import explicit.rewards.Rewards;
 import explicit.rewards.RewardsSimple;
 import io.ExplicitModelImporter;
+import io.IOUtils;
 import parser.State;
 import prism.Evaluator;
 import prism.PrismComponent;
@@ -201,7 +202,36 @@ public Rewards<Value> getRewardObject(int r) throws PrismException
 			if (!model.getModelType().nondeterministic()) {
 				importer.extractMCTransitionRewards(r, (s, s2, v) -> storeMCTransitionReward(r, s, s2, v), eval);
 			} else {
-				importer.extractMDPTransitionRewards(r, (s, i, s2, v) -> storeMDPTransitionReward(r, s, i, s2, v), eval);
+				importer.extractMDPTransitionRewards(r,
+					new IOUtils.TransitionStateRewardConsumer<Value>() {
+						int sLast = -1;
+						int iLast = -1;
+						Value vLast = null;
+						int count = 0;
+						public void accept(int s, int i, int s2, Value v) throws PrismException
+						{
+							count++;
+							// Check that transition rewards for the same state/choice are the same
+							// (currently no support for state-choice-state rewards)
+							if (s == sLast && i == iLast) {
+								if (!eval.equals(vLast, v)) {
+									throw new PrismException("mismatching transition rewards " + vLast + " and " + v + " in choice " + i + " of state " + s);
+								}
+							}
+							// And check that were rewards on all successors for each choice
+							// (for speed, we just check that the right number were present)
+							else {
+								if (sLast != -1 && count != ((NondetModel<?>) model).getNumTransitions(sLast, iLast)) {
+									throw new PrismException("wrong number of transition rewards in choice " + iLast + " of state " + sLast);
+								}
+								sLast = s;
+								iLast = i;
+								vLast = v;
+								count = 0;
+							}
+							storeMDPTransitionReward(r, s, i, s2, v);
+						}
+					}, eval);
 			}
 		}
 		return rewards[r];

prism/src/io/IOUtils.java

@@ -66,7 +66,7 @@ public interface MDPTransitionConsumer<V> {
 	 */
 	@FunctionalInterface
 	public interface LTSTransitionConsumer {
-		void accept(int s, int i, int s2, Object a) throws PrismException;;
+		void accept(int s, int i, int s2, Object a) throws PrismException;
 	}
 
 	/**
@@ -75,7 +75,7 @@ public interface LTSTransitionConsumer {
 	 */
 	@FunctionalInterface
 	public interface TransitionRewardConsumer<V> {
-		void accept(int s, int i, V v);
+		void accept(int s, int i, V v) throws PrismException;
 	}
 
 	/**
@@ -84,6 +84,6 @@ public interface TransitionRewardConsumer<V> {
 	 */
 	@FunctionalInterface
 	public interface TransitionStateRewardConsumer<V> {
-		void accept(int s, int i, int s2, V v);
+		void accept(int s, int i, int s2, V v) throws PrismException;
 	}
 }