diff --git a/prism/src/explicit/ExplicitFiles2Rewards.java b/prism/src/explicit/ExplicitFiles2Rewards.java index 7ad3dc53e..f0ab2292d 100644 --- a/prism/src/explicit/ExplicitFiles2Rewards.java +++ b/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 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() { + 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]; diff --git a/prism/src/io/IOUtils.java b/prism/src/io/IOUtils.java index 5d4847b3e..c4244627e 100644 --- a/prism/src/io/IOUtils.java +++ b/prism/src/io/IOUtils.java @@ -66,7 +66,7 @@ public interface MDPTransitionConsumer { */ @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 { - 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 { */ @FunctionalInterface public interface TransitionStateRewardConsumer { - void accept(int s, int i, int s2, V v); + void accept(int s, int i, int s2, V v) throws PrismException; } }