diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 6259da13..4efb9410 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -30,8 +30,7 @@ import java.util.*; import java.util.Map.Entry; import java.io.*; -import explicit.rewards.MCRewards; - +import explicit.rewards.*; import prism.ModelType; import prism.PrismException; import prism.PrismUtils; diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index f27d9556..4909381b 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -26,9 +26,11 @@ package explicit; -import explicit.rewards.MCRewards; -import explicit.rewards.MCRewardsStateConstant; -import jdd.JDDNode; +import java.util.BitSet; +import java.util.List; + +import explicit.rewards.*; +import parser.State; import parser.ast.*; import prism.*; @@ -192,14 +194,14 @@ public class ProbModelChecker extends StateModelChecker switch (modelType) { case CTMC: case DTMC: - //modelRewards = new MCRewardsStateArray(model.getNumStates()); - modelRewards = new MCRewardsStateConstant(1); + modelRewards = buildMCRewardStructure(model, rewStruct); break; default: - throw new PrismException("Cannot build rewards " + expr + " for " + modelType + "s"); + throw new PrismException("Cannot build rewards for " + modelType + "s"); } // Compute rewards + mainLog.println("Building reward structure..."); switch (modelType) { case CTMC: rews = ((CTMCModelChecker) this).checkRewardFormula(model, modelRewards, expr.getExpression()); @@ -223,4 +225,43 @@ public class ProbModelChecker extends StateModelChecker // For =? properties, just return values return rews; } + + private MCRewards buildMCRewardStructure(Model model, RewardStruct rewStr) throws PrismException + { + //MCRewards modelRewards = null; + List statesList; + Expression guard; + int i, j, n, numStates; + + switch (model.getModelType()) { + case CTMC: + case DTMC: + if (rewStr.getNumTransItems() > 0) { + throw new PrismException("Explicit engine does not yet handle transition rewards"); + } + // Special case: constant rewards + if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) { + return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble()); + } + // Normal: state rewards + else { + MCRewardsStateArray rewSA = new MCRewardsStateArray(model.getNumStates()); + numStates = model.getNumStates(); + statesList = model.getStatesList(); + n = rewStr.getNumItems(); + for (i = 0; i < n; i++) { + guard = rewStr.getStates(i); + for (j = 0; j < numStates; j++) { + if (guard.evaluateBoolean(statesList.get(j))) { + rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(statesList.get(j))); + } + } + } + return rewSA; + } + //break; + default: + throw new PrismException("Cannot build rewards for " + model.getModelType() + "s"); + } + } }