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

Functions handled properly by explicit model checker. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4642 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
4a20773172
commit
955e3c9aaa
2 changed files with 365 additions and 2 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. 116
      prism/src/explicit/StateModelChecker.java
  2. 251
      prism/src/explicit/StateValues.java

116
prism/src/explicit/StateModelChecker.java
View File

@ -35,6 +35,7 @@ import parser.ast.*;
import parser.ast.ExpressionFilter.FilterOperator;
import parser.type.*;
import prism.PrismException;
import prism.PrismLangException;
import prism.PrismLog;
import prism.PrismPrintStreamLog;
import prism.PrismSettings;
@ -254,6 +255,10 @@ public class StateModelChecker
if (expr instanceof ExpressionUnaryOp) {
res = checkExpressionUnaryOp(model, (ExpressionUnaryOp) expr);
}
// Functions
else if (expr instanceof ExpressionFunc) {
res = checkExpressionFunc(model, (ExpressionFunc) expr);
}
// Literals
else if (expr instanceof ExpressionLiteral) {
res = checkExpressionLiteral(model, (ExpressionLiteral) expr);
@ -347,6 +352,117 @@ public class StateModelChecker
return res1;
}
/**
* Model check a function.
*/
protected StateValues checkExpressionFunc(Model model, ExpressionFunc expr) throws PrismException
{
switch (expr.getNameCode()) {
case ExpressionFunc.MIN:
case ExpressionFunc.MAX:
return checkExpressionFuncNary(model, expr);
case ExpressionFunc.FLOOR:
case ExpressionFunc.CEIL:
return checkExpressionFuncUnary(model, expr);
case ExpressionFunc.POW:
case ExpressionFunc.MOD:
case ExpressionFunc.LOG:
return checkExpressionFuncBinary(model, expr);
default:
throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
}
}
protected StateValues checkExpressionFuncUnary(Model model, ExpressionFunc expr) throws PrismException
{
StateValues res1 = null;
int op = expr.getNameCode();
// Check operand recursively
res1 = checkExpression(model, expr.getOperand(0));
// Apply operation
try {
res1.applyFunctionUnary(op);
} catch (PrismException e) {
if (res1 != null)
res1.clear();
if (e instanceof PrismLangException)
((PrismLangException) e).setASTElement(expr);
throw e;
}
return res1;
}
protected StateValues checkExpressionFuncBinary(Model model, ExpressionFunc expr) throws PrismException
{
StateValues res1 = null, res2 = null;
int op = expr.getNameCode();
// Check operands recursively
try {
res1 = checkExpression(model, expr.getOperand(0));
res2 = checkExpression(model, expr.getOperand(1));
} catch (PrismException e) {
if (res1 != null)
res1.clear();
throw e;
}
// Apply operation
try {
res1.applyFunctionBinary(op, res2);
res2.clear();
} catch (PrismException e) {
if (res1 != null)
res1.clear();
if (res2 != null)
res2.clear();
if (e instanceof PrismLangException)
((PrismLangException) e).setASTElement(expr);
throw e;
}
return res1;
}
protected StateValues checkExpressionFuncNary(Model model, ExpressionFunc expr) throws PrismException
{
StateValues res1 = null, res2 = null;
int i, n, op = expr.getNameCode();
// Check first operand recursively
res1 = checkExpression(model, expr.getOperand(0));
// Go through remaining operands
n = expr.getNumOperands();
for (i = 1; i < n; i++) {
// Check next operand recursively
try {
res2 = checkExpression(model, expr.getOperand(i));
} catch (PrismException e) {
if (res2 != null)
res2.clear();
throw e;
}
// Apply operation
try {
res1.applyFunctionBinary(op, res2);
res2.clear();
} catch (PrismException e) {
if (res1 != null)
res1.clear();
if (res2 != null)
res2.clear();
if (e instanceof PrismLangException)
((PrismLangException) e).setASTElement(expr);
throw e;
}
}
return res1;
}
/**
* Model check a literal.
*/

251
prism/src/explicit/StateValues.java
View File

@ -35,6 +35,7 @@ import java.util.List;
import parser.State;
import parser.ast.ExpressionBinaryOp;
import parser.ast.ExpressionFunc;
import parser.ast.ExpressionUnaryOp;
import parser.type.Type;
import parser.type.TypeBool;
@ -291,7 +292,8 @@ public class StateValues
}
/**
* Modify the vector by applying binary operator {@code op} with second operand {@code sv}.
* Modify the vector by applying binary operator {@code op} with second operand {@code sv},
* where {@code op} refers to the codes in {@link ExpressionBinaryOp}.
*/
public void applyBinaryOp(int op, StateValues sv) throws PrismException
{
@ -769,7 +771,8 @@ public class StateValues
}
/**
* Modify the vector by applying unary operator {@code op}.
* Modify the vector by applying unary operator {@code op},
* where {@code op} refers to the codes in {@link ExpressionUnaryOp}.
*/
public void applyUnaryOp(int op) throws PrismException
{
@ -814,6 +817,250 @@ public class StateValues
}
}
/**
* Modify the vector by applying (unary) function {@code op},
* where {@code op} refers to the codes in {@link parser.ast.ExpressionFunc}.
*/
public void applyFunctionUnary(int op) throws PrismException
{
switch (op) {
case ExpressionFunc.FLOOR:
floor();
break;
case ExpressionFunc.CEIL:
ceil();
break;
default:
throw new PrismException("Unknown unary function");
}
}
/**
* Modify the vector by applying 'floor'.
*/
public void floor() throws PrismException
{
if (type instanceof TypeInt) {
// Nothing to do
} else if (type instanceof TypeDouble) {
valuesI = new int[size];
type = TypeInt.getInstance();
for (int i = 0; i < size; i++) {
valuesI[i] = ExpressionFunc.evaluateFloor(valuesD[i]);
}
valuesD = null;
} else {
throw new PrismException("Function floor can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying 'ceil'.
*/
public void ceil() throws PrismException
{
if (type instanceof TypeInt) {
// Nothing to do
} else if (type instanceof TypeDouble) {
valuesI = new int[size];
type = TypeInt.getInstance();
for (int i = 0; i < size; i++) {
valuesI[i] = ExpressionFunc.evaluateCeil(valuesD[i]);
}
valuesD = null;
} else {
throw new PrismException("Function ceil can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying (binary or N-ary) function {@code op} with second operand {@code sv},
* where {@code op} refers to the codes in {@link parser.ast.ExpressionFunc}.
*/
public void applyFunctionBinary(int op, StateValues sv) throws PrismException
{
switch (op) {
case ExpressionFunc.POW:
pow(sv);
break;
case ExpressionFunc.MOD:
mod(sv);
break;
case ExpressionFunc.LOG:
log(sv);
break;
case ExpressionFunc.MIN:
min(sv);
break;
case ExpressionFunc.MAX:
max(sv);
break;
default:
throw new PrismException("Unknown binary function");
}
}
/**
* Modify the vector by applying 'pow' with second operand {@code sv}.
*/
public void pow(StateValues sv) throws PrismException
{
if (type instanceof TypeInt) {
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesI[i] = ExpressionFunc.evaluatePowInt(valuesI[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
valuesD = new double[size];
type = TypeDouble.getInstance();
for (int i = 0; i < size; i++) {
valuesD[i] = ExpressionFunc.evaluatePowDouble(valuesI[i], sv.valuesD[i]);
}
valuesI = null;
} else {
throw new PrismException("Function pow() can not be applied to Boolean vectors");
}
} else if (type instanceof TypeDouble) {
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesD[i] = ExpressionFunc.evaluatePowDouble(valuesD[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
for (int i = 0; i < size; i++) {
valuesD[i] = ExpressionFunc.evaluatePowDouble(valuesD[i], sv.valuesD[i]);
}
} else {
throw new PrismException("Function pow() can not be applied to Boolean vectors");
}
} else {
throw new PrismException("Function pow() can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying 'mod' with second operand {@code sv}.
*/
public void mod(StateValues sv) throws PrismException
{
if (!(type instanceof TypeInt && sv.type instanceof TypeInt)) {
throw new PrismException("Function mod() can only be applied to integer vectors");
}
for (int i = 0; i < size; i++) {
valuesI[i] = ExpressionFunc.evaluateMod(valuesI[i], sv.valuesI[i]);
}
}
/**
* Modify the vector by applying 'log' with operand {@code sv}.
*/
public void log(StateValues sv) throws PrismException
{
if (type instanceof TypeInt) {
valuesD = new double[size];
type = TypeDouble.getInstance();
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesD[i] = ExpressionFunc.evaluateLog(valuesI[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
for (int i = 0; i < size; i++) {
valuesD[i] = ExpressionFunc.evaluateLog(valuesI[i], sv.valuesD[i]);
}
} else {
throw new PrismException("Function log() can not be applied to Boolean vectors");
}
valuesI = null;
} else if (type instanceof TypeDouble) {
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesD[i] = ExpressionFunc.evaluateLog(valuesD[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
for (int i = 0; i < size; i++) {
valuesD[i] = ExpressionFunc.evaluateLog(valuesD[i], sv.valuesD[i]);
}
} else {
throw new PrismException("Function log() can not be applied to Boolean vectors");
}
} else {
throw new PrismException("Function log() can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying 'min' with operand {@code sv}.
*/
public void min(StateValues sv) throws PrismException
{
if (type instanceof TypeInt) {
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesI[i] = Math.min(valuesI[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
valuesD = new double[size];
type = TypeDouble.getInstance();
for (int i = 0; i < size; i++) {
valuesD[i] = Math.min(valuesI[i], sv.valuesD[i]);
}
valuesI = null;
} else {
throw new PrismException("Function min() can not be applied to Boolean vectors");
}
} else if (type instanceof TypeDouble) {
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesD[i] = Math.min(valuesD[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
for (int i = 0; i < size; i++) {
valuesD[i] = Math.min(valuesD[i], sv.valuesD[i]);
}
} else {
throw new PrismException("Function min() can not be applied to Boolean vectors");
}
} else {
throw new PrismException("Function min() can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying 'max' with operand {@code sv}.
*/
public void max(StateValues sv) throws PrismException
{
if (type instanceof TypeInt) {
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesI[i] = Math.max(valuesI[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
valuesD = new double[size];
type = TypeDouble.getInstance();
for (int i = 0; i < size; i++) {
valuesD[i] = Math.max(valuesI[i], sv.valuesD[i]);
}
valuesI = null;
} else {
throw new PrismException("Function max() can not be applied to Boolean vectors");
}
} else if (type instanceof TypeDouble) {
if (sv.type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesD[i] = Math.max(valuesD[i], sv.valuesI[i]);
}
} else if (sv.type instanceof TypeDouble) {
for (int i = 0; i < size; i++) {
valuesD[i] = Math.max(valuesD[i], sv.valuesD[i]);
}
} else {
throw new PrismException("Function max() can not be applied to Boolean vectors");
}
} else {
throw new PrismException("Function max() can not be applied to Boolean vectors");
}
}
/**
* Set the elements of this vector by reading them in from a file.
*/

Write Preview
Loading…
Cancel
Save