|
|
|
@ -703,18 +703,7 @@ public class ProbModelChecker extends NonProbModelChecker |
|
|
|
|
|
|
|
// Build rewards |
|
|
|
mainLog.println("Building reward structure..."); |
|
|
|
ConstructRewards constructRewards = new ConstructRewards(mainLog); |
|
|
|
switch (model.getModelType()) { |
|
|
|
case CTMC: |
|
|
|
case DTMC: |
|
|
|
rewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues); |
|
|
|
break; |
|
|
|
case MDP: |
|
|
|
rewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues); |
|
|
|
break; |
|
|
|
default: |
|
|
|
throw new PrismException("Cannot build rewards for " + model.getModelType() + "s"); |
|
|
|
} |
|
|
|
rewards = constructRewards(model, rewStruct); |
|
|
|
|
|
|
|
// Compute rewards |
|
|
|
MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); |
|
|
|
@ -738,6 +727,27 @@ public class ProbModelChecker extends NonProbModelChecker |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
/** |
|
|
|
* Construct rewards from a reward structure and a model. |
|
|
|
*/ |
|
|
|
protected Rewards constructRewards(Model model, RewardStruct rewStruct) throws PrismException |
|
|
|
{ |
|
|
|
Rewards rewards; |
|
|
|
ConstructRewards constructRewards = new ConstructRewards(mainLog); |
|
|
|
switch (model.getModelType()) { |
|
|
|
case CTMC: |
|
|
|
case DTMC: |
|
|
|
rewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues); |
|
|
|
break; |
|
|
|
case MDP: |
|
|
|
rewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues); |
|
|
|
break; |
|
|
|
default: |
|
|
|
throw new PrismException("Cannot build rewards for " + model.getModelType() + "s"); |
|
|
|
} |
|
|
|
return rewards; |
|
|
|
} |
|
|
|
|
|
|
|
/** |
|
|
|
* Compute rewards for the contents of an R operator. |
|
|
|
*/ |
|
|
|
|