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

Changes to DTMC/MDP/STPG interface. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1424 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
3614b2d562
commit
67c7429531
7 changed files with 202 additions and 86 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. 24
      prism/src/explicit/DTMC.java
  2. 128
      prism/src/explicit/MDP.java
  3. 2
      prism/src/explicit/MDPModelChecker.java
  4. 12
      prism/src/explicit/PrismSTPGAbstractRefine.java
  5. 114
      prism/src/explicit/STPG.java
  6. 4
      prism/src/explicit/STPGAbstractRefine.java
  7. 4
      prism/src/explicit/STPGModelChecker.java

24
prism/src/explicit/DTMC.java
View File

@ -41,14 +41,14 @@ public class DTMC extends Model
public static ModelType modelType = ModelType.DTMC;
// Transition matrix (distribution list)
public List<Distribution> trans;
protected List<Distribution> trans;
// Rewards
private List<Double> transRewards;
private Double transRewardsConstant;
protected List<Double> transRewards;
protected Double transRewardsConstant;
// Other statistics
public int numTransitions;
protected int numTransitions;
/**
* Constructor: empty DTMC.
@ -171,6 +171,14 @@ public class DTMC extends Model
return 1;
}
/**
* Get the transitions (a distribution) for state s.
*/
public Distribution getTransitions(int s)
{
return trans.get(s);
}
/**
* Get the transition reward (if any) for the transitions in state s.
*/
@ -191,6 +199,14 @@ public class DTMC extends Model
return trans.get(s1).contains(s2);
}
/**
* Get the total number of transitions in the model.
*/
public int getNumTransitions()
{
return numTransitions;
}
/**
* Checks for deadlocks (states with no transitions) and throws an exception if any exist.
* States in 'except' (If non-null) are excluded from the check.

128
prism/src/explicit/MDP.java
View File

@ -42,22 +42,20 @@ public class MDP extends Model
public static ModelType modelType = ModelType.MDP;
// Transition function (Steps)
public List<ArrayList<Distribution>> steps;
protected List<List<Distribution>> trans;
// Rewards
private List<List<Double>> transRewards;
private Double transRewardsConstant;
protected List<List<Double>> transRewards;
protected Double transRewardsConstant;
// Flag: allow dupes in distribution sets?
public boolean allowDupes = false;
// Flag: allow duplicates in distribution sets?
protected boolean allowDupes = false;
// Other statistics
public int numDistrs;
public int numTransitions;
public int maxNumDistrs;
public boolean maxNumDistrsOk;
// TODO: add accessor for maxNumDistrs that recomputes if necessary
protected int numDistrs;
protected int numTransitions;
protected int maxNumDistrs;
protected boolean maxNumDistrsOk;
/**
* Constructor: empty MDP.
@ -83,9 +81,9 @@ public class MDP extends Model
super.initialise(numStates);
numDistrs = numTransitions = maxNumDistrs = 0;
maxNumDistrsOk = true;
steps = new ArrayList<ArrayList<Distribution>>(numStates);
trans = new ArrayList<List<Distribution>>(numStates);
for (int i = 0; i < numStates; i++) {
steps.add(new ArrayList<Distribution>());
trans.add(new ArrayList<Distribution>());
}
clearAllRewards();
}
@ -99,13 +97,13 @@ public class MDP extends Model
if (s >= numStates || s < 0)
return;
// Clear data structures and update stats
List<Distribution> list = steps.get(s);
List<Distribution> list = trans.get(s);
numDistrs -= list.size();
for (Distribution distr : list) {
numTransitions -= distr.size();
}
//TODO: recompute maxNumDistrs (reset maxNumDistrsOk flag)
steps.get(s).clear();
maxNumDistrsOk = false;
trans.get(s).clear();
if (transRewards != null && transRewards.get(s) != null)
transRewards.get(s).clear();
}
@ -125,7 +123,7 @@ public class MDP extends Model
public void addStates(int numToAdd)
{
for (int i = 0; i < numToAdd; i++) {
steps.add(new ArrayList<Distribution>());
trans.add(new ArrayList<Distribution>());
if (transRewards != null)
transRewards.add(null);
numStates++;
@ -133,20 +131,20 @@ public class MDP extends Model
}
/**
* Add distribution 'distr' to state s (which must exist).
* Add a choice (distribution 'distr') to state s (which must exist).
* Distribution is only actually added if it does not already exists for state s.
* (Assuming 'allowDupes' flag is not enabled.)
* Returns the index of the (existing or newly added) distribution.
* Returns -1 in case of error.
*/
public int addDistribution(int s, Distribution distr) throws PrismException
public int addChoice(int s, Distribution distr)
{
ArrayList<Distribution> set;
List<Distribution> set;
// Check state exists
if (s >= numStates || s < 0)
return -1;
// Add distribution (if new)
set = steps.get(s);
set = trans.get(s);
if (!allowDupes) {
int i = set.indexOf(distr);
if (i != -1)
@ -198,7 +196,7 @@ public class MDP extends Model
}
// If no rewards for state i yet, create list
if (transRewards.get(s) == null) {
int n = steps.get(s).size();
int n = trans.get(s).size();
List<Double> list = new ArrayList<Double>(n);
for (int j = 0; j < n; j++) {
list.add(0.0);
@ -214,9 +212,25 @@ public class MDP extends Model
*/
public int getNumChoices(int s)
{
return steps.get(s).size();
return trans.get(s).size();
}
/**
* Get the list of choices (distributions) for state s.
*/
public List<Distribution> getChoices(int s)
{
return trans.get(s);
}
/**
* Get the ith choice (distribution) for state s.
*/
public Distribution getChoice(int s, int i)
{
return trans.get(s).get(i);
}
/**
* Get the transition reward (if any) for choice i of state s.
*/
@ -235,13 +249,43 @@ public class MDP extends Model
*/
public boolean isSuccessor(int s1, int s2)
{
for (Distribution distr : steps.get(s1)) {
for (Distribution distr : trans.get(s1)) {
if (distr.contains(s2))
return true;
}
return false;
}
/**
* Get the total number of choices (distributions) over all states.
*/
public int getNumChoices()
{
return numDistrs;
}
/**
* Get the total number of transitions in the model.
*/
public int getNumTransitions()
{
return numTransitions;
}
/**
* Get the maximum number of choices (distributions) in any state.
*/
public int getMaxNumChoices()
{
// Recompute if necessary
if (!maxNumDistrsOk) {
maxNumDistrs = 0;
for (int s = 0; s < numStates; s++)
maxNumDistrs = Math.max(maxNumDistrs, getNumChoices(s));
}
return maxNumDistrs;
}
/**
* Checks for deadlocks (states with no choices) and throws an exception if any exist.
* States in 'except' (If non-null) are excluded from the check.
@ -249,7 +293,7 @@ public class MDP extends Model
public void checkForDeadlocks(BitSet except) throws PrismException
{
for (int i = 0; i < numStates; i++) {
if (steps.get(i).isEmpty() && (except == null || !except.get(i)))
if (trans.get(i).isEmpty() && (except == null || !except.get(i)))
throw new PrismException("MDP has a deadlock in state " + i);
}
// TODO: Check for empty distributions too?
@ -292,7 +336,7 @@ public class MDP extends Model
if (i != iLast || k != kLast) {
// Add any previous distribution to the last state, create new one
if (distr != null) {
addDistribution(iLast, distr);
addChoice(iLast, distr);
}
distr = new Distribution();
}
@ -304,7 +348,7 @@ public class MDP extends Model
s = in.readLine();
}
// Add previous distribution to the last state
addDistribution(iLast, distr);
addChoice(iLast, distr);
// Close file
in.close();
} catch (IOException e) {
@ -349,11 +393,11 @@ public class MDP extends Model
int k;
double d, prob, minmax;
boolean first;
ArrayList<Distribution> step;
List<Distribution> step;
minmax = 0;
first = true;
step = steps.get(s);
step = trans.get(s);
for (Distribution distr : step) {
// Compute sum for this distribution
d = 0.0;
@ -383,13 +427,13 @@ public class MDP extends Model
int j, k;
double d, prob;
List<Integer> res;
ArrayList<Distribution> step;
List<Distribution> step;
// Create data structures to store strategy
res = new ArrayList<Integer>();
// One row of matrix-vector operation
j = -1;
step = steps.get(s);
step = trans.get(s);
for (Distribution distr : step) {
j++;
// Compute sum for this distribution
@ -442,12 +486,12 @@ public class MDP extends Model
int j, k;
double d, prob, minmax;
boolean first;
ArrayList<Distribution> step;
List<Distribution> step;
minmax = 0;
first = true;
j = -1;
step = steps.get(s);
step = trans.get(s);
for (Distribution distr : step) {
j++;
// Compute sum for this distribution
@ -478,13 +522,13 @@ public class MDP extends Model
int j, k;
double d, prob;
List<Integer> res;
ArrayList<Distribution> step;
List<Distribution> step;
// Create data structures to store strategy
res = new ArrayList<Integer>();
// One row of matrix-vector operation
j = -1;
step = steps.get(s);
step = trans.get(s);
for (Distribution distr : step) {
j++;
// Compute sum for this distribution
@ -528,7 +572,7 @@ public class MDP extends Model
out.write(numStates + " " + numDistrs + " " + numTransitions + "\n");
for (i = 0; i < numStates; i++) {
j = -1;
for (Distribution distr : steps.get(i)) {
for (Distribution distr : trans.get(i)) {
j++;
for (Map.Entry<Integer, Double> e : distr) {
out.write(i + " " + j + " " + e.getKey() + " " + e.getValue() + "\n");
@ -543,7 +587,7 @@ public class MDP extends Model
out.write(numStates + " " + "?" + " " + "?" + "\n");
for (i = 0; i < numStates; i++) {
j = -1;
for (Distribution distr : steps.get(i)) {
for (Distribution distr : trans.get(i)) {
j++;
for (Map.Entry<Integer, Double> e : distr) {
out.write(i + " " + j + " " + e.getKey() + " " + "1.0" + "\n");
@ -569,7 +613,7 @@ public class MDP extends Model
if (mark != null && mark.get(i))
out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n");
j = -1;
for (Distribution distr : steps.get(i)) {
for (Distribution distr : trans.get(i)) {
j++;
for (Map.Entry<Integer, Double> e : distr) {
out.write(i + " -> " + e.getKey() + " [ label=\"");
@ -593,7 +637,7 @@ public class MDP extends Model
s += numStates + " states";
s += ", " + numDistrs + " distributions";
s += ", " + numTransitions + " transitions";
s += ", dist max/avg = " + maxNumDistrs + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates);
s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates);
return s;
}
@ -612,7 +656,7 @@ public class MDP extends Model
first = false;
else
s += ", ";
s += i + ": " + steps.get(i) + transRewards.get(i);
s += i + ": " + trans.get(i) + transRewards.get(i);
}
s += " ]";
return s;
@ -630,7 +674,7 @@ public class MDP extends Model
return false;
if (!initialStates.equals(mdp.initialStates))
return false;
if (!steps.equals(mdp.steps))
if (!trans.equals(mdp.trans))
return false;
// TODO: compare rewards (complicated: null = 0,0,0,0)
return true;

2
prism/src/explicit/MDPModelChecker.java
View File

@ -80,7 +80,7 @@ public class MDPModelChecker extends ModelChecker
b2 = target.get(i);
if (!b2) {
b2 = min; // there exists or for all choices
for (Distribution distr : mdp.steps.get(i)) {
for (Distribution distr : mdp.getChoices(i)) {
b3 = true; // all transitions are to u states
b4 = false; // some transition goes to v
for (Map.Entry<Integer, Double> e : distr) {

12
prism/src/explicit/PrismSTPGAbstractRefine.java
View File

@ -154,12 +154,12 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
switch (modelType) {
case DTMC:
distr = buildAbstractDistribution(c, (DTMC) modelConcrete);
j = ((MDP) abstraction).addDistribution(a, distr);
j = ((MDP) abstraction).addChoice(a, distr);
((MDP) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c));
break;
case CTMC:
distr = buildAbstractDistribution(c, (CTMC) modelConcrete);
j = ((CTMDP) abstraction).addDistribution(a, distr);
j = ((CTMDP) abstraction).addChoice(a, distr);
break;
case MDP:
set = buildAbstractDistributionSet(c, (MDP) modelConcrete, (STPG) abstraction);
@ -181,7 +181,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
*/
protected Distribution buildAbstractDistribution(int c, DTMC dtmc)
{
return dtmc.trans.get(c).map(concreteToAbstract);
return dtmc.getTransitions(c).map(concreteToAbstract);
}
/**
@ -190,7 +190,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
protected DistributionSet buildAbstractDistributionSet(int c, MDP mdp, STPG stpg)
{
DistributionSet set = ((STPG) stpg).newDistributionSet(null);
for (Distribution distr : mdp.steps.get(c)) {
for (Distribution distr : mdp.getChoices(c)) {
set.add(distr.map(concreteToAbstract));
}
return set;
@ -305,12 +305,12 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
switch (modelType) {
case DTMC:
distr = buildAbstractDistribution(c, (DTMC) modelConcrete);
j = ((MDP) abstraction).addDistribution(a, distr);
j = ((MDP) abstraction).addChoice(a, distr);
((MDP) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c));
break;
case CTMC:
distr = buildAbstractDistribution(c, (CTMC) modelConcrete);
j = ((CTMDP) abstraction).addDistribution(a, distr);
j = ((CTMDP) abstraction).addChoice(a, distr);
// TODO: recompute unif?
break;
case MDP:

114
prism/src/explicit/STPG.java
View File

@ -41,22 +41,22 @@ public class STPG extends Model
// Model type
public static ModelType modelType = ModelType.STPG;
// Transitions function (Steps)
public List<ArrayList<DistributionSet>> steps;
// Transition function (Steps)
protected List<ArrayList<DistributionSet>> trans;
// Rewards
private List<List<Double>> transRewards;
private Double transRewardsConstant;
protected List<List<Double>> transRewards;
protected Double transRewardsConstant;
// Flag: allow dupes in distribution sets?
public boolean allowDupes = false;
// Other statistics
public int numDistrSets;
public int numDistrs;
public int numTransitions;
public int maxNumDistrSets;
public int maxNumDistrs;
protected int numDistrSets;
protected int numDistrs;
protected int numTransitions;
protected int maxNumDistrSets;
protected int maxNumDistrs;
/**
* Constructor: empty STPG.
@ -82,12 +82,10 @@ public class STPG extends Model
DistributionSet set;
int i;
initialise(m.numStates);
i = 0;
for (ArrayList<Distribution> distrs : m.steps) {
for (i = 0; i < numStates; i++) {
set = newDistributionSet(null);
set.addAll(distrs);
set.addAll(m.getChoices(i));
addDistributionSet(i, set);
i++;
}
}
@ -99,9 +97,9 @@ public class STPG extends Model
super.initialise(numStates);
numDistrSets = numDistrs = numTransitions = 0;
maxNumDistrSets = maxNumDistrs = 0;
steps = new ArrayList<ArrayList<DistributionSet>>(numStates);
trans = new ArrayList<ArrayList<DistributionSet>>(numStates);
for (int i = 0; i < numStates; i++) {
steps.add(new ArrayList<DistributionSet>());
trans.add(new ArrayList<DistributionSet>());
}
clearAllRewards();
}
@ -115,7 +113,7 @@ public class STPG extends Model
if (i >= numStates || i < 0)
return;
// Clear data structures and update stats
List<DistributionSet> list = steps.get(i);
List<DistributionSet> list = trans.get(i);
numDistrSets -= list.size();
for (DistributionSet set : list) {
numDistrs -= set.size();
@ -125,7 +123,7 @@ public class STPG extends Model
//TODO: recompute maxNumDistrSets
//TODO: recompute maxNumDistrs
// Remove all distribution sets
steps.set(i, new ArrayList<DistributionSet>(0));
trans.set(i, new ArrayList<DistributionSet>(0));
}
/**
@ -143,7 +141,7 @@ public class STPG extends Model
public void addStates(int numToAdd)
{
for (int i = 0; i < numToAdd; i++) {
steps.add(new ArrayList<DistributionSet>());
trans.add(new ArrayList<DistributionSet>());
}
numStates += numToAdd;
}
@ -172,7 +170,7 @@ public class STPG extends Model
if (s >= numStates || s < 0)
return -1;
// Add distribution set (if new)
set = steps.get(s);
set = trans.get(s);
if (!allowDupes) {
int i = set.indexOf(newSet);
if (i != -1)
@ -224,7 +222,7 @@ public class STPG extends Model
}
// If no rewards for state i yet, create list
if (transRewards.get(s) == null) {
int n = steps.get(s).size();
int n = trans.get(s).size();
List<Double> list = new ArrayList<Double>(n);
for (int j = 0; j < n; j++) {
list.add(0.0);
@ -240,9 +238,25 @@ public class STPG extends Model
*/
public int getNumChoices(int s)
{
return steps.get(s).size();
return trans.get(s).size();
}
/**
* Get the list of choices (distribution sets) for state s.
*/
public List<DistributionSet> getChoices(int s)
{
return trans.get(s);
}
/**
* Get the ith choice (distribution set) for state s.
*/
public DistributionSet getChoice(int s, int i)
{
return trans.get(s).get(i);
}
/**
* Get the transition reward (if any) for choice i of state s.
*/
@ -261,7 +275,7 @@ public class STPG extends Model
*/
public boolean isSuccessor(int s1, int s2)
{
for (DistributionSet distrs : steps.get(s1)) {
for (DistributionSet distrs : trans.get(s1)) {
for (Distribution distr : distrs) {
if (distr.contains(s2))
return true;
@ -277,7 +291,7 @@ public class STPG extends Model
*/
public boolean allSuccessorsInSet(int s, BitSet set)
{
for (DistributionSet distrs : steps.get(s)) {
for (DistributionSet distrs : trans.get(s)) {
for (Distribution distr : distrs) {
if (!distr.isSubsetOf(set))
return false;
@ -286,6 +300,48 @@ public class STPG extends Model
return true;
}
/**
* Get the total number of player 1 choices (distribution sets) over all states.
*/
public int getNumP1Choices()
{
return numDistrSets;
}
/**
* Get the total number of player 2 choices (distributions) over all states.
*/
public int getNumP2Choices()
{
return numDistrs;
}
/**
* Get the total number of transitions in the model.
*/
public int getNumTransitions()
{
return numTransitions;
}
/**
* Get the maximum number of player 1 choices (distribution sets) in any state.
*/
public int getMaxNumP1Choices()
{
// TODO: Recompute if necessary
return maxNumDistrSets;
}
/**
* Get the maximum number of player 2 choices (distributions) in any state.
*/
public int getMaxNumP2Choices()
{
// TODO: Recompute if necessary
return maxNumDistrs;
}
/**
* Checks for deadlocks (states with no choices) and throws an exception if any exist.
* States in 'except' (If non-null) are excluded from the check.
@ -293,7 +349,7 @@ public class STPG extends Model
public void checkForDeadlocks(BitSet except) throws PrismException
{
for (int i = 0; i < numStates; i++) {
if (steps.get(i).isEmpty() && (except == null || !except.get(i)))
if (trans.get(i).isEmpty() && (except == null || !except.get(i)))
throw new PrismException("STPG has a deadlock in state " + i);
}
// TODO: Check for empty distributions sets too?
@ -347,7 +403,7 @@ public class STPG extends Model
minmax1 = 0;
first1 = true;
step = steps.get(s);
step = trans.get(s);
for (DistributionSet distrs : step) {
minmax2 = 0;
first2 = true;
@ -393,7 +449,7 @@ public class STPG extends Model
res = new ArrayList<Integer>();
// One row of matrix-vector operation
j = -1;
step = steps.get(s);
step = trans.get(s);
for (DistributionSet distrs : step) {
j++;
minmax2 = 0;
@ -451,7 +507,7 @@ public class STPG extends Model
if (mark != null && mark.get(i))
out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n");
j = -1;
for (DistributionSet distrs : steps.get(i)) {
for (DistributionSet distrs : trans.get(i)) {
j++;
k = -1;
for (Distribution distr : distrs) {
@ -500,7 +556,7 @@ public class STPG extends Model
first = false;
else
s += ", ";
s += i + ": " + steps.get(i);
s += i + ": " + trans.get(i);
}
s += " ]";
return s;
@ -518,7 +574,7 @@ public class STPG extends Model
return false;
if (!initialStates.equals(stpg.initialStates))
return false;
if (!steps.equals(stpg.steps))
if (!trans.equals(stpg.trans))
return false;
return true;
}

4
prism/src/explicit/STPGAbstractRefine.java
View File

@ -473,7 +473,7 @@ public abstract class STPGAbstractRefine
// Compute... note lbsoln for both is ok sinec = ubsoln
lb = ((STPG) abstraction).mvMultMinMaxSingle(i, lbSoln, true, min);
ub = ((STPG) abstraction).mvMultMinMaxSingle(i, lbSoln, false, min);
mainLog.println(((STPG) abstraction).steps.get(i));
mainLog.println(((STPG) abstraction).getChoices(i));
mainLog.println("XX " + i + ": old=[" + lbSoln[i] + "," + ubSoln[i] + "], new=[" + lb + "," + ub + "]");
if (PrismUtils.doublesAreClose(ub, lb, refineTermCritParam, refineTermCrit == RefineTermCrit.ABSOLUTE)) {
lbSoln[i] = ubSoln[i] = lb;
@ -1177,7 +1177,7 @@ public abstract class STPGAbstractRefine
//out.write(i + " [label=\"" + i + " [" + (ubSoln[i]) + "-" + (lbSoln[i]) + "=" + (ubSoln[i] - lbSoln[i]) + "]" + "\"");
out.write("]\n");
j = 0;
for (DistributionSet distrs : stpg.steps.get(i)) {
for (DistributionSet distrs : stpg.getChoices(i)) {
k = 0;
for (Distribution distr : distrs) {
for (Map.Entry<Integer, Double> e : distr) {

4
prism/src/explicit/STPGModelChecker.java
View File

@ -77,7 +77,7 @@ public class STPGModelChecker extends ModelChecker
b1 = target.get(i);
if (!b1) {
b1 = min1; // there exists or for all player 1 choices
for (DistributionSet distrs : stpg.steps.get(i)) {
for (DistributionSet distrs : stpg.getChoices(i)) {
b2 = min2; // there exists or for all player 2 choices
for (Distribution distr : distrs) {
b3 = false; // some transition goes to u
@ -170,7 +170,7 @@ public class STPGModelChecker extends ModelChecker
b1 = target.get(i);
if (!b1) {
b1 = min1; // there exists or for all player 1 choices
for (DistributionSet distrs : stpg.steps.get(i)) {
for (DistributionSet distrs : stpg.getChoices(i)) {
b2 = min2; // there exists or for all player 2 choices
for (Distribution distr : distrs) {
b3 = true; // all transitions are to u states

Write Preview
Loading…
Cancel
Save