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

Miscellaneous code changes/tidies - trying to align with prism-games a bit. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6881 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
c5fa220048
commit
3f56c6668f
2 changed files with 31 additions and 27 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. 21
      prism/src/explicit/MDP.java
  2. 37
      prism/src/explicit/MDPModelChecker.java

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

@ -26,12 +26,13 @@
package explicit;
import java.util.*;
import java.util.BitSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map.Entry;
import prism.PrismException;
import explicit.rewards.*;
import explicit.rewards.MDPRewards;
/**
* Interface for classes that provide (read) access to an explicit-state MDP.
@ -42,12 +43,12 @@ public interface MDP extends Model
* Get the total number of choices (distributions) over all states.
*/
public int getNumChoices();
/**
* Get the maximum number of choices (distributions) in any state.
*/
public int getMaxNumChoices();
/**
* Get the action label (if any) for choice {@code i} of state {@code s}.
*/
@ -61,7 +62,7 @@ public interface MDP extends Model
/**
* Get an iterator over the transitions from choice {@code i} of state {@code s}.
*/
public Iterator<Entry<Integer,Double>> getTransitionsIterator(int s, int i);
public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i);
/**
* Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset},
@ -74,7 +75,7 @@ public interface MDP extends Model
* @param result Store results here
*/
public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result);
/**
* Perform a single step of precomputation algorithm Prob1, i.e., for states i in {@code subset},
* set bit i of {@code result} iff, for all/some choices,
@ -87,7 +88,7 @@ public interface MDP extends Model
* @param result Store results here
*/
public void prob1step(BitSet subset, BitSet u, BitSet v, boolean forall, BitSet result);
/**
* Do a matrix-vector multiplication followed by min/max, i.e. one step of value iteration,
* i.e. for all s: result[s] = min/max_k { sum_j P_k(s,j)*vect[j] }
@ -128,7 +129,7 @@ public interface MDP extends Model
* @param vect Vector to multiply by
*/
public double mvMultSingle(int s, int k, double vect[]);
/**
* Do a Gauss-Seidel-style matrix-vector multiplication followed by min/max.
* i.e. for all s: vect[s] = min/max_k { (sum_{j!=s} P_k(s,j)*vect[j]) / P_k(s,s) }
@ -190,7 +191,7 @@ public interface MDP extends Model
* @return The maximum difference between old/new elements of {@code vect}
*/
public double mvMultRewGSMinMax(double vect[], MDPRewards mdpRewards, boolean min, BitSet subset, boolean complement, boolean absolute);
/**
* Do a single row of matrix-vector multiplication and sum of action reward followed by min/max.
* i.e. return min/max_k { rew(s) + sum_j P_k(s,j)*vect[j] }

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

@ -126,7 +126,7 @@ public class MDPModelChecker extends ProbModelChecker
res = computeNextProbs((MDP) model, target, min);
return StateValues.createFromDoubleArray(res.soln, model);
}
/**
* Compute probabilities for a bounded until operator.
*/
@ -201,7 +201,7 @@ public class MDPModelChecker extends ProbModelChecker
protected StateValues checkRewardFormula(Model model, MDPRewards modelRewards, Expression expr, boolean min) throws PrismException
{
StateValues rewards = null;
if (expr instanceof ExpressionTemporal) {
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
switch (exprTemp.getOperator()) {
@ -212,7 +212,7 @@ public class MDPModelChecker extends ProbModelChecker
throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator");
}
}
if (rewards == null)
throw new PrismException("Unrecognised operator in R operator");
@ -258,7 +258,7 @@ public class MDPModelChecker extends ProbModelChecker
long timer;
timer = System.currentTimeMillis();
// Store num states
n = mdp.getNumStates();
@ -330,12 +330,12 @@ public class MDPModelChecker extends ProbModelChecker
mdpSolnMethod = MDPSolnMethod.GAUSS_SEIDEL;
mainLog.printWarning("Switching to MDP solution method \"" + mdpSolnMethod.fullName() + "\"");
}
// Check for some unsupported combinations
if (mdpSolnMethod == MDPSolnMethod.VALUE_ITERATION && valIterDir == ValIterDir.ABOVE) {
if (!(precomp && prob0))
if (!(precomp && prob0))
throw new PrismException("Precomputation (Prob0) must be enabled for value iteration from above");
if (!min)
if (!min)
throw new PrismException("Value iteration from above only works for minimum probabilities");
}
@ -651,7 +651,7 @@ public class MDPModelChecker extends ProbModelChecker
msg += "\nConsider using a different numerical method or increasing the maximum number of iterations";
throw new PrismException(msg);
}
// Process adversary
if (genAdv) {
// Prune adversary
@ -749,7 +749,7 @@ public class MDPModelChecker extends ProbModelChecker
msg += "\nConsider using a different numerical method or increasing the maximum number of iterations";
throw new PrismException(msg);
}
// Return results
res = new ModelCheckerResult();
res.soln = soln;
@ -1027,7 +1027,7 @@ public class MDPModelChecker extends ProbModelChecker
unknown.andNot(target);
if (remain != null)
unknown.and(remain);
// Start iterations
iters = 0;
while (iters < k) {
@ -1087,7 +1087,8 @@ public class MDPModelChecker extends ProbModelChecker
* @param known Optionally, a set of states for which the exact answer is known
* Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values.
*/
public ModelCheckerResult computeReachRewards(MDP mdp, MDPRewards mdpRewards, BitSet target, boolean min, double init[], BitSet known) throws PrismException
public ModelCheckerResult computeReachRewards(MDP mdp, MDPRewards mdpRewards, BitSet target, boolean min, double init[], BitSet known)
throws PrismException
{
ModelCheckerResult res = null;
BitSet inf;
@ -1166,7 +1167,8 @@ public class MDPModelChecker extends ProbModelChecker
* @param known Optionally, a set of states for which the exact answer is known
* Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values.
*/
protected ModelCheckerResult computeReachRewardsGaussSeidel(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[], BitSet known) throws PrismException
protected ModelCheckerResult computeReachRewardsGaussSeidel(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[],
BitSet known) throws PrismException
{
ModelCheckerResult res;
BitSet unknown;
@ -1231,7 +1233,7 @@ public class MDPModelChecker extends ProbModelChecker
msg += "\nConsider using a different numerical method or increasing the maximum number of iterations";
throw new PrismException(msg);
}
// Return results
res = new ModelCheckerResult();
res.soln = soln;
@ -1251,7 +1253,8 @@ public class MDPModelChecker extends ProbModelChecker
* @param known Optionally, a set of states for which the exact answer is known
* Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values.
*/
protected ModelCheckerResult computeReachRewardsValIter(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[], BitSet known) throws PrismException
protected ModelCheckerResult computeReachRewardsValIter(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, double init[], BitSet known)
throws PrismException
{
ModelCheckerResult res;
BitSet unknown;
@ -1321,7 +1324,7 @@ public class MDPModelChecker extends ProbModelChecker
msg += "\nConsider using a different numerical method or increasing the maximum number of iterations";
throw new PrismException(msg);
}
// Return results
res = new ModelCheckerResult();
res.soln = soln;
@ -1353,7 +1356,7 @@ public class MDPModelChecker extends ProbModelChecker
* @param mdp The MDP
* @param adv The adversary
*/
public void restrictAdversaryToReachableStates(MDP mdp,int adv[])
public void restrictAdversaryToReachableStates(MDP mdp, int adv[])
{
BitSet restrict = new BitSet();
BitSet explore = new BitSet();
@ -1388,7 +1391,7 @@ public class MDPModelChecker extends ProbModelChecker
adv[s] = -1;
}
}
/**
* Simple test program.
*/

Write Preview
Loading…
Cancel
Save