s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Reward constrcution for explicit engine pushed into separate class, and added state rewards for MDPs. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3370 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
a539e72e57
commit
075822347e
3 changed files with 162 additions and 85 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 88
      prism/src/explicit/ProbModelChecker.java
  2. 142
      prism/src/explicit/rewards/ConstructRewards.java
  3. 17
      prism/src/explicit/rewards/MDPRewardsSimple.java

88
prism/src/explicit/ProbModelChecker.java
View File

@ -191,14 +191,15 @@ public class ProbModelChecker extends StateModelChecker
if (rewStruct == null)
throw new PrismException("Invalid reward structure index \"" + rs + "\"");
// Build rewards (just MCs for now)
// Build rewards
ConstructRewards constructRewards = new ConstructRewards(mainLog);
switch (modelType) {
case CTMC:
case DTMC:
mcRewards = buildMCRewardStructure(model, rewStruct);
mcRewards = constructRewards.buildMCRewardStructure(model, rewStruct, constantValues);
break;
case MDP:
mdpRewards = buildMDPRewardStructure((MDP) model, rewStruct);
mdpRewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues);
break;
default:
throw new PrismException("Cannot build rewards for " + modelType + "s");
@ -229,85 +230,4 @@ 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<State> 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 for D/CTMCs");
}
// Special case: constant rewards
if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) {
return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble(constantValues));
}
// Normal: state rewards
else {
numStates = model.getNumStates();
statesList = model.getStatesList();
MCRewardsStateArray rewSA = new MCRewardsStateArray(numStates);
n = rewStr.getNumItems();
for (i = 0; i < n; i++) {
guard = rewStr.getStates(i);
for (j = 0; j < numStates; j++) {
if (guard.evaluateBoolean(constantValues, statesList.get(j))) {
rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
}
}
}
return rewSA;
}
//break;
default:
throw new PrismException("Cannot build rewards for " + model.getModelType() + "s");
}
}
private MDPRewards buildMDPRewardStructure(MDP mdp, RewardStruct rewStr) throws PrismException
{
//MCRewards modelRewards = null;
List<State> statesList;
Expression guard;
String action;
Object mdpAction;
int i, j, k, n, numStates, numChoices;
if (rewStr.getNumStateItems() > 0) {
throw new PrismException("Explicit engine does not yet handle state rewards for MDPs");
}
// Special case: constant rewards
// TODO
/*if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) {
return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble(constantValues));
}*/
// Normal: transition rewards
else {
numStates = mdp.getNumStates();
statesList = mdp.getStatesList();
MDPRewardsSimple rewSimple = new MDPRewardsSimple(numStates);
n = rewStr.getNumItems();
for (i = 0; i < n; i++) {
guard = rewStr.getStates(i);
action = rewStr.getSynch(i);
for (j = 0; j < numStates; j++) {
if (guard.evaluateBoolean(constantValues, statesList.get(j))) {
numChoices = mdp.getNumChoices(j);
for (k = 0; k < numChoices; k++) {
mdpAction = mdp.getAction(j, k);
if (mdpAction == null ? (action == null) : mdpAction.equals(action)) {
rewSimple.setTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
}
}
}
}
}
return rewSimple;
}
}
}

142
prism/src/explicit/rewards/ConstructRewards.java
View File

@ -0,0 +1,142 @@
//==============================================================================
//
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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;
import java.util.List;
import parser.State;
import parser.Values;
import parser.ast.Expression;
import parser.ast.RewardStruct;
import prism.PrismException;
import prism.PrismFileLog;
import prism.PrismLog;
import explicit.MDP;
import explicit.Model;
public class ConstructRewards
{
protected PrismLog mainLog;
public ConstructRewards()
{
this(new PrismFileLog("stdout"));
}
public ConstructRewards(PrismLog mainLog)
{
this.mainLog = mainLog;
}
/**
* Construct the rewards for a Markov chain (DTMC or CTMC) from a model and reward structure.
* @param model 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
{
List<State> statesList;
Expression guard;
int i, j, n, numStates;
if (rewStr.getNumTransItems() > 0) {
throw new PrismException("Explicit engine does not yet handle transition rewards for D/CTMCs");
}
// Special case: constant rewards
if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) {
return new StateRewardsConstant(rewStr.getReward(0).evaluateDouble(constantValues));
}
// Normal: state rewards
else {
numStates = model.getNumStates();
statesList = model.getStatesList();
MCRewardsStateArray rewSA = new MCRewardsStateArray(numStates);
n = rewStr.getNumItems();
for (i = 0; i < n; i++) {
guard = rewStr.getStates(i);
for (j = 0; j < numStates; j++) {
if (guard.evaluateBoolean(constantValues, statesList.get(j))) {
rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
}
}
}
return rewSA;
}
}
/**
* Construct the rewards for a Markov chain (DTMC or CTMC) from a model and reward structure.
* @param model The DTMC or CTMC
* @param rewStr The reward structure
* @param constantValues Values for any undefined constants needed
*/
public MDPRewards buildMDPRewardStructure(MDP mdp, RewardStruct rewStr, Values constantValues) throws PrismException
{
List<State> statesList;
Expression guard;
String action;
Object mdpAction;
int i, j, k, n, numStates, numChoices;
// Special case: constant state rewards
if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) {
return new StateRewardsConstant(rewStr.getReward(0).evaluateDouble(constantValues));
}
// Normal: state and transition rewards
else {
numStates = mdp.getNumStates();
statesList = mdp.getStatesList();
MDPRewardsSimple rewSimple = new MDPRewardsSimple(numStates);
n = rewStr.getNumItems();
for (i = 0; i < n; i++) {
guard = rewStr.getStates(i);
action = rewStr.getSynch(i);
for (j = 0; j < numStates; j++) {
// Is guard satisfied?
if (guard.evaluateBoolean(constantValues, statesList.get(j))) {
// Transition reward
if (rewStr.getRewardStructItem(i).isTransitionReward()) {
numChoices = mdp.getNumChoices(j);
for (k = 0; k < numChoices; k++) {
mdpAction = mdp.getAction(j, k);
if (mdpAction == null ? (action == null) : mdpAction.equals(action)) {
rewSimple.setTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
}
}
}
// State reward
else {
rewSimple.setStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
}
}
}
}
return rewSimple;
}
}
}

17
prism/src/explicit/rewards/MDPRewardsSimple.java
View File

@ -57,7 +57,22 @@ public class MDPRewardsSimple implements MDPRewards
// Mutators
/**
* Set the reward for choice {@code i} of state {@code s} to {@code r}.
* Set the state reward for state {@code s} to {@code r}.
*/
public void setStateReward(int s, double r)
{
// If no rewards array created yet, create it
if (stateRewards == null) {
stateRewards = new ArrayList<Double>(numStates);
for (int j = 0; j < numStates; j++)
stateRewards.add(0.0);
}
// Set reward
stateRewards.set(s, r);
}
/**
* Set the transition reward for choice {@code i} of state {@code s} to {@code r}.
*/
public void setTransitionReward(int s, int i, double r)
{

Write Preview
Loading…
Cancel
Save