Browse Source
Updates to explicit engine from prism-qar (Vojta):
Updates to explicit engine from prism-qar (Vojta):
* new rewards code for STPGs * additional utility methods * strip out some old reward stuff git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3323 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
15 years ago
16 changed files with 535 additions and 104 deletions
-
6prism/src/explicit/Distribution.java
-
19prism/src/explicit/DistributionSet.java
-
5prism/src/explicit/MDP.java
-
139prism/src/explicit/MDPSimple.java
-
16prism/src/explicit/MDPSparse.java
-
9prism/src/explicit/STPG.java
-
91prism/src/explicit/STPGAbstrSimple.java
-
17prism/src/explicit/STPGModelChecker.java
-
2prism/src/explicit/rewards/MCRewards.java
-
2prism/src/explicit/rewards/MDPRewards.java
-
6prism/src/explicit/rewards/MDPRewardsSimple.java
-
9prism/src/explicit/rewards/Rewards.java
-
78prism/src/explicit/rewards/STPGRewards.java
-
42prism/src/explicit/rewards/STPGRewardsConstant.java
-
132prism/src/explicit/rewards/STPGRewardsSimple.java
-
66prism/src/explicit/rewards/StateTransitionRewardsSimple.java
@ -0,0 +1,9 @@ |
|||
package explicit.rewards; |
|||
|
|||
/** |
|||
* A dummy interface implemented by all reward classes. |
|||
*/ |
|||
public interface Rewards |
|||
{ |
|||
|
|||
} |
|||
@ -0,0 +1,78 @@ |
|||
//============================================================================== |
|||
// |
|||
// 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; |
|||
|
|||
/** |
|||
* Class that provide access to explicit-state rewards for an abstraction STPG. |
|||
* |
|||
* There are two type of rewards. Ones are on distribution sets and correspond |
|||
* to state rewards in the MDP (SUPPORT FOR THESE IS CURRENTLY NOT IMPLEMENTED). |
|||
* The others are on Distributions and correspond to transition rewards. Because |
|||
* each of the distributions may abstract several concrete distributions, it can |
|||
* have multiple rewards. The number of different rewards for each distribution |
|||
* can be obtained using {@link #getTransitionRewardCount(int, int, int)}, |
|||
* the rewards itself are then obtained using {@link #getTransitionReward(int, int, int, int)} |
|||
* |
|||
* |
|||
* |
|||
*/ |
|||
public interface STPGRewards extends Rewards |
|||
{ |
|||
/** |
|||
* Returns the reward associated with {@code ds}th distribution for the state {@code s}. |
|||
*/ |
|||
public double getDistributionSetReward(int s, int ds); |
|||
|
|||
/** |
|||
* Removes all rewards for DistributionSets and Distributions associated with state {@code s}. |
|||
*/ |
|||
public void clearRewards(int s); |
|||
|
|||
/** |
|||
* Returns the number of different rewards associated with {@code d}th distribution of |
|||
* {@code ds}th distribution set of state {@code s} |
|||
* |
|||
* @param s State |
|||
* @param ds Distribution set |
|||
* @param d Distribution |
|||
* @return Number of different rewards associated with the distribution |
|||
*/ |
|||
public int getTransitionRewardCount(int s, int ds, int d); |
|||
|
|||
/** |
|||
* |
|||
* Returns {@code i}th reward of {@code d}th distribution of |
|||
* {@code ds}th distribution set of state {@code s} |
|||
* |
|||
* @param s State |
|||
* @param ds Distribution set |
|||
* @param d Distribution |
|||
* @param i Index of the reward to return |
|||
* @return The reward. |
|||
*/ |
|||
public double getTransitionReward(int s, int ds, int d, int i); |
|||
} |
|||
@ -0,0 +1,42 @@ |
|||
package explicit.rewards; |
|||
|
|||
/** |
|||
* Explicit storage of constant game rewards. |
|||
*/ |
|||
public class STPGRewardsConstant implements STPGRewards |
|||
{ |
|||
private double dsReward; |
|||
private double transReward; |
|||
|
|||
public STPGRewardsConstant(double dsReward, double transReward) |
|||
{ |
|||
this.dsReward = dsReward; |
|||
this.transReward = transReward; |
|||
} |
|||
|
|||
@Override |
|||
public double getDistributionSetReward(int s, int d) |
|||
{ |
|||
return this.dsReward; |
|||
} |
|||
|
|||
@Override |
|||
public int getTransitionRewardCount(int s, int ds, int d) |
|||
{ |
|||
return 1; |
|||
} |
|||
|
|||
@Override |
|||
public double getTransitionReward(int s, int d, int t, int i) |
|||
{ |
|||
return this.transReward; |
|||
} |
|||
|
|||
@Override |
|||
public void clearRewards(int s) |
|||
{ |
|||
//do nothing |
|||
return; |
|||
} |
|||
|
|||
} |
|||
@ -0,0 +1,132 @@ |
|||
package explicit.rewards; |
|||
|
|||
import java.util.ArrayList; |
|||
import java.util.List; |
|||
|
|||
public class STPGRewardsSimple implements STPGRewards |
|||
{ |
|||
/** Number of states */ |
|||
protected int numStates; |
|||
|
|||
protected List<List<Double>> distributionSetRewards; |
|||
|
|||
protected List<List<List<List<Double>>>> transRewards; |
|||
|
|||
public STPGRewardsSimple(int numStates) |
|||
{ |
|||
this.numStates = numStates; |
|||
// Initially lists are just null (denoting all 0) |
|||
distributionSetRewards = new ArrayList<List<Double>>(); |
|||
|
|||
transRewards = new ArrayList<List<List<List<Double>>>>(numStates); |
|||
for (int j = 0; j < numStates; j++) |
|||
{ |
|||
transRewards.add(null); |
|||
distributionSetRewards.add(null); |
|||
} |
|||
} |
|||
|
|||
/** |
|||
* NOT IMPLEMENTED |
|||
*/ |
|||
@Override |
|||
public double getDistributionSetReward(int s, int ds) |
|||
{ |
|||
return 0; |
|||
} |
|||
|
|||
@Override |
|||
public int getTransitionRewardCount(int s, int ds, int d) |
|||
{ |
|||
if (transRewards.get(s) == null || transRewards.get(s).get(ds) == null || transRewards.get(s).get(ds).get(d) == null) |
|||
return 0; |
|||
else |
|||
return transRewards.get(s).get(ds).get(d).size(); |
|||
} |
|||
|
|||
/** |
|||
* Adds rewards specified by {@code newRewards} to the rewards associated |
|||
* with {@code ds}th distribution of state {@code s}. |
|||
* |
|||
* The rewards are given as a list of lists of doubles, where the |
|||
* i-th element of {@code newRewards} specifies the rewards to be added |
|||
* to the (possibly empty) list of rewards associated with |
|||
* i-th distribution associated with {@code s} and {@code ds}. |
|||
* |
|||
* @param s |
|||
* @param ds |
|||
* @param newRewards |
|||
*/ |
|||
public void addTransitionRewards(int s, int ds, List<List<Double>> newRewards) |
|||
{ |
|||
if (transRewards.get(s) == null) { |
|||
List<List<List<Double>>> distTransRewards = new ArrayList<List<List<Double>>>(); |
|||
transRewards.set(s, distTransRewards); |
|||
} |
|||
|
|||
if (transRewards.get(s).size() <= ds) { |
|||
List<List<Double>> lTransRewards = new ArrayList<List<Double>>(); |
|||
transRewards.get(s).add(lTransRewards); |
|||
} |
|||
|
|||
List<List<Double>> dsRewards = transRewards.get(s).get(ds); |
|||
if (dsRewards.size() < newRewards.size()) |
|||
{ |
|||
for (int i = dsRewards.size(); i < newRewards.size(); i++) |
|||
{ |
|||
dsRewards.add(new ArrayList<Double>()); |
|||
} |
|||
} |
|||
|
|||
|
|||
for (int i = 0; i < dsRewards.size(); i++) |
|||
{ |
|||
dsRewards.get(i).addAll(newRewards.get(i)); |
|||
} |
|||
} |
|||
|
|||
|
|||
@Override |
|||
public double getTransitionReward(int s, int ds, int d, int i) |
|||
{ |
|||
return this.transRewards.get(s).get(ds).get(d).get(i); |
|||
} |
|||
|
|||
@Override |
|||
public void clearRewards(int s) |
|||
{ |
|||
if(this.distributionSetRewards.get(s) != null) |
|||
this.distributionSetRewards.get(s).clear(); |
|||
if(this.transRewards.get(s) != null) |
|||
this.transRewards.get(s).clear(); |
|||
} |
|||
|
|||
public void addStates(int n) |
|||
{ |
|||
this.numStates += n; |
|||
for (int i=0; i<n; i++) |
|||
{ |
|||
this.distributionSetRewards.add(null); |
|||
this.transRewards.add(null); |
|||
} |
|||
} |
|||
|
|||
@Override |
|||
public String toString() |
|||
{ |
|||
int i; |
|||
boolean first; |
|||
String s = ""; |
|||
first = true; |
|||
s = "[ "; |
|||
for (i = 0; i < numStates; i++) { |
|||
if (first) |
|||
first = false; |
|||
else |
|||
s += ", "; |
|||
s += i + ": " + transRewards.get(i); |
|||
} |
|||
s += " ]"; |
|||
return s; |
|||
} |
|||
} |
|||
@ -0,0 +1,66 @@ |
|||
package explicit.rewards; |
|||
|
|||
import java.util.ArrayList; |
|||
import java.util.List; |
|||
|
|||
/** |
|||
* Explicit-state storage of state and transition rewards (mutable). |
|||
*/ |
|||
public class StateTransitionRewardsSimple extends StateRewardsSimple |
|||
{ |
|||
private List<List<Double>> transRewards; |
|||
|
|||
public StateTransitionRewardsSimple(int numStates) |
|||
{ |
|||
super(numStates); |
|||
this.transRewards = new ArrayList<List<Double>>(); |
|||
for(int i = 0; i < numStates; i++) |
|||
{ |
|||
this.transRewards.add(new ArrayList<Double>()); |
|||
} |
|||
} |
|||
|
|||
/** |
|||
* Increase the number of states by {@code numStates} |
|||
* |
|||
* @param numStates Number of newly added states |
|||
*/ |
|||
public void addStates(int numStates) |
|||
{ |
|||
for(int i = 0; i < numStates; i++) |
|||
{ |
|||
this.transRewards.add(new ArrayList<Double>()); |
|||
} |
|||
} |
|||
|
|||
/** |
|||
* Set the reward of choice {@code c} of state {@code s} to {@code r}. |
|||
* |
|||
* The number of states added so far must be at least {@code s+1}. |
|||
* |
|||
* @param s State |
|||
* @param c Choice (Transition) |
|||
* @param r Reward |
|||
*/ |
|||
public void setTransitionReward(int s, int c, double r) |
|||
{ |
|||
int n = s - transRewards.get(s).size() + 1; |
|||
if (n > 0) { |
|||
for (int j = 0; j < n; j++) { |
|||
transRewards.get(s).add(0.0); |
|||
} |
|||
} |
|||
transRewards.get(s).set(c, r); |
|||
} |
|||
|
|||
@Override |
|||
public double getTransitionReward(int s, int i) |
|||
{ |
|||
return transRewards.get(s).get(i); |
|||
} |
|||
|
|||
public String toString() |
|||
{ |
|||
return "rews: " + stateRewards + "; rewt: " + transRewards; |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue