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

Unary operators handled properly in explicit engine. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4629 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
1f315247a3
commit
4bd2319af1
2 changed files with 89 additions and 21 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. 25
      prism/src/explicit/StateModelChecker.java
  2. 85
      prism/src/explicit/StateValues.java

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

@ -250,6 +250,10 @@ public class StateModelChecker
if (expr instanceof ExpressionBinaryOp) {
res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr);
}
// Unary ops
if (expr instanceof ExpressionUnaryOp) {
res = checkExpressionUnaryOp(model, (ExpressionUnaryOp) expr);
}
// Literals
else if (expr instanceof ExpressionLiteral) {
res = checkExpressionLiteral(model, (ExpressionLiteral) expr);
@ -322,6 +326,27 @@ public class StateModelChecker
return res1;
}
/**
* Model check a unary operator.
*/
protected StateValues checkExpressionUnaryOp(Model model, ExpressionUnaryOp expr) throws PrismException
{
StateValues res1 = null;
int op = expr.getOperator();
// Check operand recursively
res1 = checkExpression(model, expr.getOperand());
// Parentheses are easy - nothing to do:
if (op == ExpressionUnaryOp.PARENTH)
return res1;
// Apply operation
res1.applyUnaryOp(op);
return res1;
}
/**
* Model check a literal.
*/

85
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.ExpressionUnaryOp;
import parser.type.Type;
import parser.type.TypeBool;
import parser.type.TypeDouble;
@ -365,7 +366,7 @@ public class StateValues
valuesB.xor(sv.valuesB);
valuesB.flip(0, size);
}
/**
* Modify the vector by applying 'or' with operand {@code sv}.
*/
@ -376,7 +377,7 @@ public class StateValues
}
valuesB.or(sv.valuesB);
}
/**
* Modify the vector by applying 'and' with operand {@code sv}.
*/
@ -387,7 +388,7 @@ public class StateValues
}
valuesB.and(sv.valuesB);
}
/**
* Modify the vector by applying 'equals' with operand {@code sv}.
*/
@ -425,7 +426,7 @@ public class StateValues
valuesI = null;
valuesD = null;
}
/**
* Modify the vector by applying 'not-equals' with operand {@code sv}.
*/
@ -462,7 +463,7 @@ public class StateValues
valuesI = null;
valuesD = null;
}
/**
* Modify the vector by applying '>' with operand {@code sv}.
*/
@ -491,8 +492,7 @@ public class StateValues
for (int i = 0; i < size; i++) {
valuesB.set(i, valuesD[i] > sv.valuesD[i]);
}
}
else {
} else {
throw new PrismException("Operator > can not be applied to Boolean vectors");
}
} else {
@ -502,7 +502,7 @@ public class StateValues
valuesI = null;
valuesD = null;
}
/**
* Modify the vector by applying '>=' with operand {@code sv}.
*/
@ -531,8 +531,7 @@ public class StateValues
for (int i = 0; i < size; i++) {
valuesB.set(i, valuesD[i] >= sv.valuesD[i]);
}
}
else {
} else {
throw new PrismException("Operator >= can not be applied to Boolean vectors");
}
} else {
@ -542,7 +541,7 @@ public class StateValues
valuesI = null;
valuesD = null;
}
/**
* Modify the vector by applying '<' with operand {@code sv}.
*/
@ -571,8 +570,7 @@ public class StateValues
for (int i = 0; i < size; i++) {
valuesB.set(i, valuesD[i] < sv.valuesD[i]);
}
}
else {
} else {
throw new PrismException("Operator < can not be applied to Boolean vectors");
}
} else {
@ -582,7 +580,7 @@ public class StateValues
valuesI = null;
valuesD = null;
}
/**
* Modify the vector by applying '<=' with operand {@code sv}.
*/
@ -611,8 +609,7 @@ public class StateValues
for (int i = 0; i < size; i++) {
valuesB.set(i, valuesD[i] <= sv.valuesD[i]);
}
}
else {
} else {
throw new PrismException("Operator <= can not be applied to Boolean vectors");
}
} else {
@ -622,7 +619,7 @@ public class StateValues
valuesI = null;
valuesD = null;
}
/**
* Modify the vector by applying 'plus' with operand {@code sv}.
*/
@ -659,7 +656,7 @@ public class StateValues
throw new PrismException("Operator + can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying 'minus' with operand {@code sv}.
*/
@ -696,7 +693,7 @@ public class StateValues
throw new PrismException("Operator - can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying 'times' with operand {@code sv}.
*/
@ -733,7 +730,7 @@ public class StateValues
throw new PrismException("Operator * can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying 'divide' with operand {@code sv}.
*/
@ -770,7 +767,53 @@ public class StateValues
throw new PrismException("Operator / can not be applied to Boolean vectors");
}
}
/**
* Modify the vector by applying unary operator {@code op}.
*/
public void applyUnaryOp(int op) throws PrismException
{
switch (op) {
case ExpressionUnaryOp.NOT:
not();
break;
case ExpressionUnaryOp.MINUS:
minus();
break;
default:
throw new PrismException("Unknown binary operator");
}
}
/**
* Modify the vector by applying 'not'
*/
public void not() throws PrismException
{
if (!(type instanceof TypeBool)) {
throw new PrismException("Operator ! can only be applied to Boolean vectors");
}
valuesB.flip(0, size);
}
/**
* Modify the vector by applying (unary) 'minus'.
*/
public void minus() throws PrismException
{
if (type instanceof TypeInt) {
for (int i = 0; i < size; i++) {
valuesI[i] = -valuesI[i];
}
} else if (type instanceof TypeDouble) {
for (int i = 0; i < size; i++) {
valuesD[i] = -valuesD[i];
}
} else {
throw new PrismException("Operator - 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