From e9a1859339f4e2fba566e06c2361b12e8e757e3f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 16 Oct 2011 19:44:29 +0000 Subject: [PATCH] Add binary operators to StateValues class and use in explicit model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3996 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 26 +- prism/src/explicit/StateValues.java | 501 +++++++++++++++++++++- 2 files changed, 506 insertions(+), 21 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 9f13548a..831d2f30 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -34,7 +34,6 @@ import parser.Values; import parser.ast.*; import parser.ast.ExpressionFilter.FilterOperator; import parser.type.*; -import prism.Prism; import prism.PrismException; import prism.PrismLog; import prism.PrismPrintStreamLog; @@ -248,8 +247,7 @@ public class StateModelChecker StateValues res = null; // Binary ops - // (just "and" for now - more to come later) - if (expr instanceof ExpressionBinaryOp && Expression.isAnd(expr)) { + if (expr instanceof ExpressionBinaryOp) { res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr); } // Literals @@ -304,11 +302,25 @@ public class StateModelChecker */ protected StateValues checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr) throws PrismException { - // (just "and" for now - more to come later) - StateValues res1 = checkExpression(model, expr.getOperand1()); - StateValues res2 = checkExpression(model, expr.getOperand2()); - res1.and(res2); + StateValues res1 = null, res2 = null; + int op = expr.getOperator(); + + // Check operands recursively + try { + res1 = checkExpression(model, expr.getOperand1()); + res2 = checkExpression(model, expr.getOperand2()); + } catch (PrismException e) { + if (res1 != null) + res1.clear(); + throw e; + } + res1 = checkExpression(model, expr.getOperand1()); + res2 = checkExpression(model, expr.getOperand2()); + + // Apply operation + res1.applyBinaryOp(op, res2); res2.clear(); + return res1; } diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java index ed2a33e1..13004c2c 100644 --- a/prism/src/explicit/StateValues.java +++ b/prism/src/explicit/StateValues.java @@ -34,6 +34,7 @@ import java.util.BitSet; import java.util.List; import parser.State; +import parser.ast.ExpressionBinaryOp; import parser.type.Type; import parser.type.TypeBool; import parser.type.TypeDouble; @@ -288,14 +289,488 @@ public class StateValues valuesB.set(i, val); } + /** + * Modify the vector by applying binary operator {@code op} with second operand {@code sv}. + */ + public void applyBinaryOp(int op, StateValues sv) throws PrismException + { + switch (op) { + case ExpressionBinaryOp.IMPLIES: + implies(sv); + break; + case ExpressionBinaryOp.IFF: + iff(sv); + break; + case ExpressionBinaryOp.OR: + or(sv); + break; + case ExpressionBinaryOp.AND: + and(sv); + break; + case ExpressionBinaryOp.EQ: + equals(sv); + break; + case ExpressionBinaryOp.NE: + notEquals(sv); + break; + case ExpressionBinaryOp.GT: + greaterThan(sv); + break; + case ExpressionBinaryOp.GE: + greaterThanEquals(sv); + break; + case ExpressionBinaryOp.LT: + lessThan(sv); + break; + case ExpressionBinaryOp.LE: + lessThanEquals(sv); + break; + case ExpressionBinaryOp.PLUS: + plus(sv); + break; + case ExpressionBinaryOp.MINUS: + minus(sv); + break; + case ExpressionBinaryOp.TIMES: + times(sv); + break; + case ExpressionBinaryOp.DIVIDE: + divide(sv); + break; + default: + throw new PrismException("Unknown binary operator"); + } + } + + /** + * Modify the vector by applying 'implies' with operand {@code sv}. + */ + public void implies(StateValues sv) throws PrismException + { + if (!(type instanceof TypeBool) || !(sv.type instanceof TypeBool)) { + throw new PrismException("Operator => can only be applied to Boolean vectors"); + } + valuesB.flip(0, size); + valuesB.or(sv.valuesB); + } + + /** + * Modify the vector by applying 'iff' with operand {@code sv}. + */ + public void iff(StateValues sv) throws PrismException + { + if (!(type instanceof TypeBool) || !(sv.type instanceof TypeBool)) { + throw new PrismException("Operator <=> can only be applied to Boolean vectors"); + } + valuesB.xor(sv.valuesB); + valuesB.flip(0, size); + } + + /** + * Modify the vector by applying 'or' with operand {@code sv}. + */ + public void or(StateValues sv) throws PrismException + { + if (!(type instanceof TypeBool) || !(sv.type instanceof TypeBool)) { + throw new PrismException("Operator | can only be applied to Boolean vectors"); + } + valuesB.or(sv.valuesB); + } + + /** + * Modify the vector by applying 'and' with operand {@code sv}. + */ public void and(StateValues sv) throws PrismException { if (!(type instanceof TypeBool) || !(sv.type instanceof TypeBool)) { - throw new PrismException("Conjunction can only be applied to Boolean vectors"); + throw new PrismException("Operator & can only be applied to Boolean vectors"); } valuesB.and(sv.valuesB); } - + + /** + * Modify the vector by applying 'equals' with operand {@code sv}. + */ + public void equals(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] == sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] == sv.valuesD[i]); + } + } + } else if (type instanceof TypeDouble) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] == sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] == sv.valuesD[i]); + } + } + } else if (type instanceof TypeBool) { + if (sv.type instanceof TypeBool) { + valuesB.xor(sv.valuesB); + valuesB.flip(0, size); + } + } + type = TypeBool.getInstance(); + valuesI = null; + valuesD = null; + } + + /** + * Modify the vector by applying 'not-equals' with operand {@code sv}. + */ + public void notEquals(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] != sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] != sv.valuesD[i]); + } + } + } else if (type instanceof TypeDouble) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] != sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] != sv.valuesD[i]); + } + } + } else if (type instanceof TypeBool) { + if (sv.type instanceof TypeBool) { + valuesB.xor(sv.valuesB); + } + } + type = TypeBool.getInstance(); + valuesI = null; + valuesD = null; + } + + /** + * Modify the vector by applying '>' with operand {@code sv}. + */ + public void greaterThan(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] > sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] > sv.valuesD[i]); + } + } else { + throw new PrismException("Operator > can not be applied to Boolean vectors"); + } + } else if (type instanceof TypeDouble) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] > sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] > sv.valuesD[i]); + } + } + else { + throw new PrismException("Operator > can not be applied to Boolean vectors"); + } + } else { + throw new PrismException("Operator > can not be applied to Boolean vectors"); + } + type = TypeBool.getInstance(); + valuesI = null; + valuesD = null; + } + + /** + * Modify the vector by applying '>=' with operand {@code sv}. + */ + public void greaterThanEquals(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] >= sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] >= sv.valuesD[i]); + } + } else { + throw new PrismException("Operator >= can not be applied to Boolean vectors"); + } + } else if (type instanceof TypeDouble) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] >= sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] >= sv.valuesD[i]); + } + } + else { + throw new PrismException("Operator >= can not be applied to Boolean vectors"); + } + } else { + throw new PrismException("Operator >= can not be applied to Boolean vectors"); + } + type = TypeBool.getInstance(); + valuesI = null; + valuesD = null; + } + + /** + * Modify the vector by applying '<' with operand {@code sv}. + */ + public void lessThan(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] < sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] < sv.valuesD[i]); + } + } else { + throw new PrismException("Operator < can not be applied to Boolean vectors"); + } + } else if (type instanceof TypeDouble) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] < sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] < sv.valuesD[i]); + } + } + else { + throw new PrismException("Operator < can not be applied to Boolean vectors"); + } + } else { + throw new PrismException("Operator < can not be applied to Boolean vectors"); + } + type = TypeBool.getInstance(); + valuesI = null; + valuesD = null; + } + + /** + * Modify the vector by applying '<=' with operand {@code sv}. + */ + public void lessThanEquals(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] <= sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesI[i] <= sv.valuesD[i]); + } + } else { + throw new PrismException("Operator <= can not be applied to Boolean vectors"); + } + } else if (type instanceof TypeDouble) { + valuesB = new BitSet(); + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] <= sv.valuesI[i]); + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesB.set(i, valuesD[i] <= sv.valuesD[i]); + } + } + else { + throw new PrismException("Operator <= can not be applied to Boolean vectors"); + } + } else { + throw new PrismException("Operator <= can not be applied to Boolean vectors"); + } + type = TypeBool.getInstance(); + valuesI = null; + valuesD = null; + } + + /** + * Modify the vector by applying 'plus' with operand {@code sv}. + */ + public void plus(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + 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] = valuesI[i] + sv.valuesD[i]; + } + valuesI = null; + } else { + throw new PrismException("Operator + 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] += sv.valuesI[i]; + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesD[i] += sv.valuesD[i]; + } + } else { + throw new PrismException("Operator + can not be applied to Boolean vectors"); + } + } else { + throw new PrismException("Operator + can not be applied to Boolean vectors"); + } + } + + /** + * Modify the vector by applying 'minus' with operand {@code sv}. + */ + public void minus(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + 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] = valuesI[i] - sv.valuesD[i]; + } + valuesI = null; + } else { + throw new PrismException("Operator - 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] -= sv.valuesI[i]; + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesD[i] -= sv.valuesD[i]; + } + } else { + throw new PrismException("Operator - can not be applied to Boolean vectors"); + } + } else { + throw new PrismException("Operator - can not be applied to Boolean vectors"); + } + } + + /** + * Modify the vector by applying 'times' with operand {@code sv}. + */ + public void times(StateValues sv) throws PrismException + { + if (type instanceof TypeInt) { + if (sv.type instanceof TypeInt) { + for (int i = 0; i < size; i++) { + 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] = valuesI[i] * sv.valuesD[i]; + } + valuesI = null; + } else { + throw new PrismException("Operator * 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] *= sv.valuesI[i]; + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesD[i] *= sv.valuesD[i]; + } + } else { + throw new PrismException("Operator * can not be applied to Boolean vectors"); + } + } else { + throw new PrismException("Operator * can not be applied to Boolean vectors"); + } + } + + /** + * Modify the vector by applying 'divide' with operand {@code sv}. + */ + public void divide(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] = ((double) valuesI[i]) / sv.valuesI[i]; + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesD[i] = valuesI[i] / sv.valuesD[i]; + } + } else { + throw new PrismException("Operator / 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] /= sv.valuesI[i]; + } + } else if (sv.type instanceof TypeDouble) { + for (int i = 0; i < size; i++) { + valuesD[i] /= sv.valuesD[i]; + } + } else { + throw new PrismException("Operator / can not be applied to Boolean vectors"); + } + } 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. */ @@ -304,12 +779,13 @@ public class StateValues BufferedReader in; String s; int lineNum = 0, count = 0; - + try { // open file for reading in = new BufferedReader(new FileReader(file)); // read remaining lines - s = in.readLine(); lineNum++; + s = in.readLine(); + lineNum++; while (s != null) { s = s.trim(); if (!("".equals(s))) { @@ -318,33 +794,30 @@ public class StateValues if (type instanceof TypeInt) { int i = Integer.parseInt(s); setIntValue(count, i); - } - else if (type instanceof TypeDouble) { + } else if (type instanceof TypeDouble) { double d = Double.parseDouble(s); setDoubleValue(count, d); - } - else if (type instanceof TypeBool) { + } else if (type instanceof TypeBool) { boolean b = Boolean.parseBoolean(s); setBooleanValue(count, b); } count++; } - s = in.readLine(); lineNum++; + s = in.readLine(); + lineNum++; } // close file in.close(); // check size if (count < size) throw new PrismException("Too few values in file \"" + file + "\" (" + count + ", not " + size + ")"); - } - catch (IOException e) { + } catch (IOException e) { throw new PrismException("File I/O error reading from \"" + file + "\""); - } - catch (NumberFormatException e) { + } catch (NumberFormatException e) { throw new PrismException("Error detected at line " + lineNum + " of file \"" + file + "\""); } } - + // ... /**