diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index b2a01bb7..a3f5afd2 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -31,7 +31,7 @@ import java.util.*; import jdd.JDD; import explicit.rewards.MCRewards; -import explicit.rewards.MCRewardsStateArray; +import explicit.rewards.StateRewardsArray; import parser.ast.*; import parser.type.*; import prism.*; @@ -374,7 +374,7 @@ public class CTMCModelChecker extends DTMCModelChecker DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); // Convert rewards n = dtmc.getNumStates(); - MCRewardsStateArray rewEmb = new MCRewardsStateArray(n); + StateRewardsArray rewEmb = new StateRewardsArray(n); for (i = 0; i < n; i++) { rewEmb.setStateReward(i, mcRewards.getStateReward(i) / ((CTMC) dtmc).getExitRate(i)); } diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index aa4040b2..592179e0 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -196,7 +196,7 @@ public class ProbModelChecker extends StateModelChecker switch (modelType) { case CTMC: case DTMC: - mcRewards = constructRewards.buildMCRewardStructure(model, rewStruct, constantValues); + mcRewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues); break; case MDP: mdpRewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues); diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index 9a9239cf..f7622935 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/prism/src/explicit/rewards/ConstructRewards.java @@ -35,8 +35,7 @@ import parser.ast.RewardStruct; import prism.PrismException; import prism.PrismFileLog; import prism.PrismLog; -import explicit.MDP; -import explicit.Model; +import explicit.*; public class ConstructRewards { @@ -54,17 +53,18 @@ public class ConstructRewards /** * Construct the rewards for a Markov chain (DTMC or CTMC) from a model and reward structure. - * @param model The DTMC or CTMC + * @param mc The DTMC or CTMC * @param rewStr The reward structure * @param constantValues Values for any undefined constants needed */ - public MCRewards buildMCRewardStructure(Model model, RewardStruct rewStr, Values constantValues) throws PrismException + public MCRewards buildMCRewardStructure(DTMC mc, RewardStruct rewStr, Values constantValues) throws PrismException { List statesList; Expression guard; int i, j, n, numStates; if (rewStr.getNumTransItems() > 0) { + // TODO throw new PrismException("Explicit engine does not yet handle transition rewards for D/CTMCs"); } // Special case: constant rewards @@ -73,9 +73,9 @@ public class ConstructRewards } // Normal: state rewards else { - numStates = model.getNumStates(); - statesList = model.getStatesList(); - MCRewardsStateArray rewSA = new MCRewardsStateArray(numStates); + numStates = mc.getNumStates(); + statesList = mc.getStatesList(); + StateRewardsArray rewSA = new StateRewardsArray(numStates); n = rewStr.getNumItems(); for (i = 0; i < n; i++) { guard = rewStr.getStates(i); @@ -90,8 +90,8 @@ public class ConstructRewards } /** - * Construct the rewards for a Markov chain (DTMC or CTMC) from a model and reward structure. - * @param model The DTMC or CTMC + * Construct the rewards for an MDP from a model and reward structure. + * @param model The MDP * @param rewStr The reward structure * @param constantValues Values for any undefined constants needed */ diff --git a/prism/src/explicit/rewards/MCRewardsStateConstant.java b/prism/src/explicit/rewards/MCRewardsStateConstant.java deleted file mode 100644 index b10ef683..00000000 --- a/prism/src/explicit/rewards/MCRewardsStateConstant.java +++ /dev/null @@ -1,57 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (University of Oxford) -// -//------------------------------------------------------------------------------ -// -// This file is part of PRISM. -// -// PRISM is free software; you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// PRISM is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. -// -// You should have received a copy of the GNU General Public License -// along with PRISM; if not, write to the Free Software Foundation, -// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -// -//============================================================================== - -package explicit.rewards; - -/** - * Explicit-state storage of constant state rewards for a DTMC/CTMC. - */ -public class MCRewardsStateConstant implements MCRewards, MDPRewards -{ - protected double stateReward = 0.0; - - /** - * Constructor: all rewards equal to {@code r} - */ - public MCRewardsStateConstant(double r) - { - stateReward = r; - } - - // Accessors - - @Override - public double getStateReward(int s) - { - return stateReward; - } - - @Override - public double getTransitionReward(int s, int i) - { - return 0.0; - } -} diff --git a/prism/src/explicit/rewards/MCRewardsStateArray.java b/prism/src/explicit/rewards/StateRewardsArray.java similarity index 90% rename from prism/src/explicit/rewards/MCRewardsStateArray.java rename to prism/src/explicit/rewards/StateRewardsArray.java index 8a938f29..0dc0d4af 100644 --- a/prism/src/explicit/rewards/MCRewardsStateArray.java +++ b/prism/src/explicit/rewards/StateRewardsArray.java @@ -27,9 +27,9 @@ package explicit.rewards; /** - * Explicit-state storage of just state rewards for a DTMC/CTMC (as an array). + * Explicit-state storage of just state rewards (as an array). */ -public class MCRewardsStateArray implements MCRewards, MDPRewards +public class StateRewardsArray implements MCRewards, MDPRewards { /** Array of state rewards **/ protected double stateRewards[] = null; @@ -38,7 +38,7 @@ public class MCRewardsStateArray implements MCRewards, MDPRewards * Constructor: all zero rewards. * @param numStates Number of states */ - public MCRewardsStateArray(int numStates) + public StateRewardsArray(int numStates) { stateRewards = new double[numStates]; for (int i = 0; i < numStates; i++)