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

Explicit evaluation of missing functions (pow, mod, log). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@734 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
539c794980
commit
f1dc23ec35
1 changed files with 117 additions and 108 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. 225
      prism/src/prism/StateModelChecker.java

225
prism/src/prism/StateModelChecker.java
View File

@ -32,7 +32,7 @@ import odd.*;
import parser.*;
import parser.ast.*;
// Model checker for DTMCs
// Base class for model checkers - does state-based evaluations (no temporal/probabilistic)
public class StateModelChecker implements ModelChecker
{
@ -718,83 +718,26 @@ public class StateModelChecker implements ModelChecker
{
switch (expr.getNameCode()) {
case ExpressionFunc.MIN:
return checkExpressionFuncMinMax(expr, true);
case ExpressionFunc.MAX:
return checkExpressionFuncMinMax(expr, false);
return checkExpressionFuncNary(expr);
case ExpressionFunc.FLOOR:
return checkExpressionFuncFloor(expr);
case ExpressionFunc.CEIL:
return checkExpressionFuncCeil(expr);
return checkExpressionFuncUnary(expr);
case ExpressionFunc.POW:
return checkExpressionFuncPow(expr);
case ExpressionFunc.MOD:
return checkExpressionFuncMod(expr);
case ExpressionFunc.LOG:
return checkExpressionFuncLog(expr);
return checkExpressionFuncBinary(expr);
default:
throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
}
}
private StateProbs checkExpressionFuncMinMax(ExpressionFunc expr, boolean min) throws PrismException
{
StateProbs res1 = null, res2 = null;
JDDNode dd1, dd2;
DoubleVector dv1, dv2;
int i, i2, n, n2;
boolean symbolic;
// Check first operand recursively
try {
res1 = checkExpression(expr.getOperand(0));
} catch (PrismException e) {
if (res1 != null)
res1.clear();
throw e;
}
// Go through remaining operands
// Switch to explicit as soon as an operand is explicit
n = expr.getNumOperands();
symbolic = (res1 instanceof StateProbsMTBDD);
for (i = 1; i < n; i++) {
try {
res2 = checkExpression(expr.getOperand(i));
} catch (PrismException e) {
if (res2 != null)
res2.clear();
throw e;
}
// Explicit
if (!symbolic || !(res2 instanceof StateProbsMTBDD)) {
symbolic = false;
dv1 = res1.convertToStateProbsDV().getDoubleVector();
dv2 = res2.convertToStateProbsDV().getDoubleVector();
n2 = dv1.getSize();
for (i2 = 0; i2 < n2; i2++) {
if (min) dv1.setElement(i2, Math.min(dv1.getElement(i2), dv2.getElement(i2)));
else dv1.setElement(i2, Math.max(dv1.getElement(i2), dv2.getElement(i2)));
}
dv2.clear();
res1 = new StateProbsDV(dv1, model);
}
// Symbolic
else {
dd1 = ((StateProbsMTBDD) res1).getJDDNode();
dd2 = ((StateProbsMTBDD) res2).getJDDNode();
dd1 = JDD.Apply(min ? JDD.MIN : JDD.MAX, dd1, dd2);
res1 = new StateProbsMTBDD(dd1, model);
}
}
return res1;
}
private StateProbs checkExpressionFuncFloor(ExpressionFunc expr) throws PrismException
private StateProbs checkExpressionFuncUnary(ExpressionFunc expr) throws PrismException
{
StateProbs res1 = null;
JDDNode dd1;
DoubleVector dv1;
int i, n;
int i, n, op = expr.getNameCode();
// Check operand recursively
try {
@ -807,81 +750,147 @@ public class StateModelChecker implements ModelChecker
// Symbolic
if (res1 instanceof StateProbsMTBDD) {
dd1 = ((StateProbsMTBDD) res1).getJDDNode();
dd1 = JDD.MonadicApply(JDD.FLOOR, dd1);
switch (op) {
case ExpressionFunc.FLOOR: dd1 = JDD.MonadicApply(JDD.FLOOR, dd1); break;
case ExpressionFunc.CEIL: dd1 = JDD.MonadicApply(JDD.CEIL, dd1); break;
}
return new StateProbsMTBDD(dd1, model);
}
// Explicit
else {
dv1 = res1.convertToStateProbsDV().getDoubleVector();
n = dv1.getSize();
for (i = 0; i < n; i++)
dv1.setElement(i, Math.floor(dv1.getElement(i)));
switch (op) {
case ExpressionFunc.FLOOR:
for (i = 0; i < n; i++) dv1.setElement(i, Math.floor(dv1.getElement(i)));
break;
case ExpressionFunc.CEIL:
for (i = 0; i < n; i++) dv1.setElement(i, Math.ceil(dv1.getElement(i)));
break;
}
return new StateProbsDV(dv1, model);
}
}
private StateProbs checkExpressionFuncCeil(ExpressionFunc expr) throws PrismException
private StateProbs checkExpressionFuncBinary(ExpressionFunc expr) throws PrismException
{
StateProbs res1 = null;
JDDNode dd1;
DoubleVector dv1;
int i, n;
StateProbs res1 = null, res2 = null;
JDDNode dd = null, dd1, dd2;
DoubleVector dv1, dv2;
int i, n, op = expr.getNameCode();
// Check operand recursively
// Check operands recursively
try {
res1 = checkExpression(expr.getOperand(0));
res2 = checkExpression(expr.getOperand(1));
} catch (PrismException e) {
if (res1 != null)
res1.clear();
if (res2 != null)
res2.clear();
throw e;
}
// Symbolic
if (res1 instanceof StateProbsMTBDD) {
// If both operands are symbolic, result will be symbolic
if (res1 instanceof StateProbsMTBDD && res2 instanceof StateProbsMTBDD) {
dd1 = ((StateProbsMTBDD) res1).getJDDNode();
dd1 = JDD.MonadicApply(JDD.CEIL, dd1);
return new StateProbsMTBDD(dd1, model);
dd2 = ((StateProbsMTBDD) res2).getJDDNode();
switch (op) {
case ExpressionFunc.POW:
dd = JDD.Apply(JDD.POW, dd1, dd2);
break;
case ExpressionFunc.MOD:
dd = JDD.Apply(JDD.MOD, dd1, dd2);
break;
case ExpressionFunc.LOG:
dd = JDD.Apply(JDD.LOGXY, dd1, dd2);
break;
}
return new StateProbsMTBDD(dd, model);
}
// Explicit
// Otherwise result will be explicit
else {
dv1 = res1.convertToStateProbsDV().getDoubleVector();
dv2 = res2.convertToStateProbsDV().getDoubleVector();
n = dv1.getSize();
for (i = 0; i < n; i++)
dv1.setElement(i, Math.ceil(dv1.getElement(i)));
switch (op) {
case ExpressionFunc.POW:
for (i = 0; i < n; i++)
dv1.setElement(i, Math.pow(dv1.getElement(i), dv2.getElement(i)));
break;
case ExpressionFunc.MOD:
for (i = 0; i < n; i++)
dv1.setElement(i, (int)dv1.getElement(i) % (int)dv2.getElement(i));
break;
case ExpressionFunc.LOG:
for (i = 0; i < n; i++)
dv1.setElement(i, PrismUtils.log(dv1.getElement(i), dv2.getElement(i)));
break;
}
dv2.clear();
return new StateProbsDV(dv1, model);
}
}
private StateProbs checkExpressionFuncPow(ExpressionFunc expr) throws PrismException
{
JDDNode dd1, dd2, dd;
dd1 = checkExpressionDD(expr.getOperand(0));
dd2 = checkExpressionDD(expr.getOperand(1));
dd = JDD.Apply(JDD.POW, dd1, dd2);
return new StateProbsMTBDD(dd, model);
}
private StateProbs checkExpressionFuncMod(ExpressionFunc expr) throws PrismException
private StateProbs checkExpressionFuncNary(ExpressionFunc expr) throws PrismException
{
JDDNode dd1, dd2, dd;
dd1 = checkExpressionDD(expr.getOperand(0));
dd2 = checkExpressionDD(expr.getOperand(1));
dd = JDD.Apply(JDD.MOD, dd1, dd2);
return new StateProbsMTBDD(dd, model);
}
private StateProbs checkExpressionFuncLog(ExpressionFunc expr) throws PrismException
{
JDDNode dd1, dd2, dd;
dd1 = checkExpressionDD(expr.getOperand(0));
dd2 = checkExpressionDD(expr.getOperand(1));
dd = JDD.Apply(JDD.LOGXY, dd1, dd2);
StateProbs res1 = null, res2 = null;
JDDNode dd1, dd2;
DoubleVector dv1, dv2;
int i, i2, n, n2, op = expr.getNameCode();
boolean symbolic;
// Check first operand recursively
try {
res1 = checkExpression(expr.getOperand(0));
} catch (PrismException e) {
if (res1 != null)
res1.clear();
throw e;
}
// Go through remaining operands
// Switch to explicit as soon as an operand is explicit
n = expr.getNumOperands();
symbolic = (res1 instanceof StateProbsMTBDD);
for (i = 1; i < n; i++) {
try {
res2 = checkExpression(expr.getOperand(i));
} catch (PrismException e) {
if (res2 != null)
res2.clear();
throw e;
}
// Explicit
if (!symbolic || !(res2 instanceof StateProbsMTBDD)) {
symbolic = false;
dv1 = res1.convertToStateProbsDV().getDoubleVector();
dv2 = res2.convertToStateProbsDV().getDoubleVector();
n2 = dv1.getSize();
switch (op) {
case ExpressionFunc.MIN:
for (i2 = 0; i2 < n2; i2++)
dv1.setElement(i2, Math.min(dv1.getElement(i), dv2.getElement(i)));
break;
case ExpressionFunc.MAX:
for (i2 = 0; i2 < n2; i2++)
dv1.setElement(i2, Math.max(dv1.getElement(i), dv2.getElement(i)));
break;
}
dv2.clear();
res1 = new StateProbsDV(dv1, model);
}
// Symbolic
else {
dd1 = ((StateProbsMTBDD) res1).getJDDNode();
dd2 = ((StateProbsMTBDD) res2).getJDDNode();
switch (op) {
case ExpressionFunc.MIN: dd1 = JDD.Apply(JDD.MIN, dd1, dd2); break;
case ExpressionFunc.MAX: dd1 = JDD.Apply(JDD.MAX, dd1, dd2); break;
}
res1 = new StateProbsMTBDD(dd1, model);
}
}
return new StateProbsMTBDD(dd, model);
return res1;
}
// Check a literal

Write Preview
Loading…
Cancel
Save