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

Next operator for explicit model checker. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5629 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
4413259325
commit
433c3a3414
3 changed files with 151 additions and 4 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. 52
      prism/src/explicit/DTMCModelChecker.java
  2. 51
      prism/src/explicit/MDPModelChecker.java
  3. 52
      prism/src/explicit/STPGModelChecker.java

52
prism/src/explicit/DTMCModelChecker.java
View File

@ -84,10 +84,10 @@ public class DTMCModelChecker extends ProbModelChecker
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
// Next
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
throw new PrismException("The explicit engine does not yet handle the next operator");
probs = checkProbNext(model, exprTemp);
}
// Until
if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
if (exprTemp.hasBounds()) {
probs = checkProbBoundedUntil(model, exprTemp);
} else {
@ -106,6 +106,21 @@ public class DTMCModelChecker extends ProbModelChecker
return probs;
}
/**
* Compute probabilities for a next operator.
*/
protected StateValues checkProbNext(Model model, ExpressionTemporal expr) throws PrismException
{
BitSet target = null;
ModelCheckerResult res = null;
// Model check the operand
target = checkExpression(model, expr.getOperand2()).getBitSet();
res = computeNextProbs((DTMC) model, target);
return StateValues.createFromDoubleArray(res.soln, model);
}
/**
* Compute probabilities for a bounded until operator.
*/
@ -330,6 +345,39 @@ public class DTMCModelChecker extends ProbModelChecker
// Numerical computation functions
/**
* Compute next=state probabilities.
* i.e. compute the probability of being in a state in {@code target} in the next step.
* @param dtmc The DTMC
* @param target Target states
*/
public ModelCheckerResult computeNextProbs(DTMC dtmc, BitSet target) throws PrismException
{
ModelCheckerResult res = null;
int n;
double soln[], soln2[];
long timer;
timer = System.currentTimeMillis();
// Store num states
n = dtmc.getNumStates();
// Create/initialise solution vector(s)
soln = Utils.bitsetToDoubleArray(target, n);
soln2 = new double[n];
// Next-step probabilities
dtmc.mvMult(soln, soln2, null, false);
// Return results
res = new ModelCheckerResult();
res.soln = soln2;
res.numIters = 1;
res.timeTaken = timer / 1000.0;
return res;
}
/**
* Compute reachability probabilities.
* i.e. compute the probability of reaching a state in {@code target}.

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

@ -90,7 +90,7 @@ public class MDPModelChecker extends ProbModelChecker
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
// Next
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
throw new PrismException("The explicit engine does not yet handle the next operator");
probs = checkProbNext(model, exprTemp, min);
}
// Until
else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
@ -112,6 +112,21 @@ public class MDPModelChecker extends ProbModelChecker
return probs;
}
/**
* Compute probabilities for a next operator.
*/
protected StateValues checkProbNext(Model model, ExpressionTemporal expr, boolean min) throws PrismException
{
BitSet target = null;
ModelCheckerResult res = null;
// Model check the operand
target = checkExpression(model, expr.getOperand2()).getBitSet();
res = computeNextProbs((MDP) model, target, min);
return StateValues.createFromDoubleArray(res.soln, model);
}
/**
* Compute probabilities for a bounded until operator.
*/
@ -228,6 +243,40 @@ public class MDPModelChecker extends ProbModelChecker
// Numerical computation functions
/**
* Compute next=state probabilities.
* i.e. compute the probability of being in a state in {@code target} in the next step.
* @param mdp The MDP
* @param target Target states
* @param min Min or max probabilities (true=min, false=max)
*/
public ModelCheckerResult computeNextProbs(MDP mdp, BitSet target, boolean min) throws PrismException
{
ModelCheckerResult res = null;
int n;
double soln[], soln2[];
long timer;
timer = System.currentTimeMillis();
// Store num states
n = mdp.getNumStates();
// Create/initialise solution vector(s)
soln = Utils.bitsetToDoubleArray(target, n);
soln2 = new double[n];
// Next-step probabilities
mdp.mvMultMinMax(soln, min, soln2, null, false, null);
// Return results
res = new ModelCheckerResult();
res.soln = soln2;
res.numIters = 1;
res.timeTaken = timer / 1000.0;
return res;
}
/**
* Compute reachability probabilities.
* i.e. compute the min/max probability of reaching a state in {@code target}.

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

@ -84,7 +84,7 @@ public class STPGModelChecker extends ProbModelChecker
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
// Next
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
throw new PrismException("The explicit engine does not yet handle the next operator");
probs = checkProbNext(model, exprTemp, min1, min2);
}
// Until
else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
@ -106,6 +106,21 @@ public class STPGModelChecker extends ProbModelChecker
return probs;
}
/**
* Compute probabilities for a next operator.
*/
protected StateValues checkProbNext(Model model, ExpressionTemporal expr, boolean min1, boolean min2) throws PrismException
{
BitSet target = null;
ModelCheckerResult res = null;
// Model check the operand
target = checkExpression(model, expr.getOperand2()).getBitSet();
res = computeNextProbs((STPG) model, target, min1, min2);
return StateValues.createFromDoubleArray(res.soln, model);
}
/**
* Compute probabilities for a bounded until operator.
*/
@ -196,6 +211,41 @@ public class STPGModelChecker extends ProbModelChecker
// Numerical computation functions
/**
* Compute next=state probabilities.
* i.e. compute the probability of being in a state in {@code target} in the next step.
* @param stpg The STPG
* @param target Target states
* @param min1 Min or max probabilities for player 1 (true=lower bound, false=upper bound)
* @param min2 Min or max probabilities for player 2 (true=min, false=max)
*/
public ModelCheckerResult computeNextProbs(STPG stpg, BitSet target, boolean min1, boolean min2) throws PrismException
{
ModelCheckerResult res = null;
int n;
double soln[], soln2[];
long timer;
timer = System.currentTimeMillis();
// Store num states
n = stpg.getNumStates();
// Create/initialise solution vector(s)
soln = Utils.bitsetToDoubleArray(target, n);
soln2 = new double[n];
// Next-step probabilities
stpg.mvMultMinMax(soln, min1, min2, soln2, null, false, null);
// Return results
res = new ModelCheckerResult();
res.soln = soln2;
res.numIters = 1;
res.timeTaken = timer / 1000.0;
return res;
}
/**
* Compute reachability probabilities.
* i.e. compute the min/max probability of reaching a state in {@code target}.

Write Preview
Loading…
Cancel
Save