From 45ac6e02e8019ef230452bb4893b9ff73a384fea Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Sat, 20 Jan 2018 11:21:01 +0100 Subject: [PATCH] exact/parametric: support if-the-else expressions in properties + test case --- .../verify/param/param-ite.prism | 10 ++++ .../verify/param/param-ite.prism.args | 2 + .../verify/param/param-ite.prism.props | 7 +++ prism/src/param/BoxRegion.java | 18 +++++++ prism/src/param/ParamModelChecker.java | 18 +++++++ prism/src/param/Region.java | 2 + prism/src/param/RegionIntersection.java | 17 ++++++- prism/src/param/RegionValues.java | 49 +++++++++++++++++++ .../src/param/RegionValuesIntersections.java | 24 +++++++-- 9 files changed, 141 insertions(+), 6 deletions(-) create mode 100644 prism-tests/functionality/verify/param/param-ite.prism create mode 100644 prism-tests/functionality/verify/param/param-ite.prism.args create mode 100644 prism-tests/functionality/verify/param/param-ite.prism.props diff --git a/prism-tests/functionality/verify/param/param-ite.prism b/prism-tests/functionality/verify/param/param-ite.prism new file mode 100644 index 00000000..382860cc --- /dev/null +++ b/prism-tests/functionality/verify/param/param-ite.prism @@ -0,0 +1,10 @@ +dtmc + +const double p; +formula outcome = (s>0 ? s-1 : -1); + +module M1 + s: [0..4] init 0; + + [] s=0 -> 1/2:(s'=0) + 1/8:(s'=1) + 1/8:(s'=2) + 1/8:(s'=3) + 1/8:(s'=4); +endmodule diff --git a/prism-tests/functionality/verify/param/param-ite.prism.args b/prism-tests/functionality/verify/param/param-ite.prism.args new file mode 100644 index 00000000..e815f7d2 --- /dev/null +++ b/prism-tests/functionality/verify/param/param-ite.prism.args @@ -0,0 +1,2 @@ +-exact -const p=0 +-param p=0:1 diff --git a/prism-tests/functionality/verify/param/param-ite.prism.props b/prism-tests/functionality/verify/param/param-ite.prism.props new file mode 100644 index 00000000..04db1224 --- /dev/null +++ b/prism-tests/functionality/verify/param/param-ite.prism.props @@ -0,0 +1,7 @@ +// test case: support for if-then-else and formulas in expressions (exact / parametric) + +// RESULT: 1/4 +P=?[F outcome=2] + +// RESULT: 0 +P=?[G outcome=-1] diff --git a/prism/src/param/BoxRegion.java b/prism/src/param/BoxRegion.java index 40537b09..f219cb42 100644 --- a/prism/src/param/BoxRegion.java +++ b/prism/src/param/BoxRegion.java @@ -416,6 +416,24 @@ final class BoxRegion extends Region { return result; } + @Override + RegionValues ITE(StateValues valuesI, StateValues valuesT, StateValues valuesE) + { + RegionValues result = new RegionValues(factory); + int numStates = valuesI.getNumStates(); + StateValues values = new StateValues(numStates, factory.getInitialState()); + for (int state = 0; state < numStates; state++) { + if (valuesI.getStateValueAsBoolean(state)) { + values.setStateValue(state, valuesT.getStateValue(state)); + } else { + values.setStateValue(state, valuesE.getStateValue(state)); + } + } + result.add(this, values); + + return result; + } + /** * Split region in longest dimension. * diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index d3e88a0e..1b4a843a 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -70,6 +70,7 @@ import parser.ast.ExpressionFilter.FilterOperator; import parser.ast.ExpressionForAll; import parser.ast.ExpressionFormula; import parser.ast.ExpressionFunc; +import parser.ast.ExpressionITE; import parser.ast.ExpressionLabel; import parser.ast.ExpressionLiteral; import parser.ast.ExpressionProb; @@ -371,6 +372,8 @@ final public class ParamModelChecker extends PrismComponent res = checkExpressionUnaryOp(model, (ExpressionUnaryOp) expr, needStates); } else if (expr instanceof ExpressionBinaryOp) { res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr, needStates); + } else if (expr instanceof ExpressionITE) { + res = checkExpressionITE(model, (ExpressionITE) expr, needStates); } else if (expr instanceof ExpressionLabel) { res = checkExpressionLabel(model, (ExpressionLabel) expr, needStates); } else if (expr instanceof ExpressionFormula) { @@ -466,6 +469,21 @@ final public class ParamModelChecker extends PrismComponent return res1.binaryOp(parserBinaryOpToRegionOp(expr.getOperator()), res2); } + /** + * Model check an If-Then-Else operator. + */ + protected RegionValues checkExpressionITE(ParamModel model, ExpressionITE expr, BitSet needStates) throws PrismException + { + RegionValues resI = checkExpression(model, expr.getOperand1(), needStates); + RegionValues resT = checkExpression(model, expr.getOperand2(), needStates); + RegionValues resE = checkExpression(model, expr.getOperand3(), needStates); + resI.clearNotNeeded(needStates); + resT.clearNotNeeded(needStates); + resE.clearNotNeeded(needStates); + + return resI.ITE(resT, resE); + } + /** * Model check a label. */ diff --git a/prism/src/param/Region.java b/prism/src/param/Region.java index 41b72f7c..302dc214 100644 --- a/prism/src/param/Region.java +++ b/prism/src/param/Region.java @@ -94,6 +94,8 @@ abstract class Region { abstract RegionValues binaryOp(int op, StateValues values1, StateValues values2); + abstract RegionValues ITE(StateValues valueI, StateValues valueT, StateValues valueE); + /** * Splits this region into several parts. * How this is done exactly depends on the implementation in derived diff --git a/prism/src/param/RegionIntersection.java b/prism/src/param/RegionIntersection.java index 3c99127f..83051cfc 100644 --- a/prism/src/param/RegionIntersection.java +++ b/prism/src/param/RegionIntersection.java @@ -30,7 +30,7 @@ package param; * Maintains the intersection of two regions. * This class is to be used in combination with * {@code RegionValuesIntersections} to iterate over the intersection - * of two {@RegionValues}. + * of two (or three) {@RegionValues}. * * @author Ernst Moritz Hahn (University of Oxford) * @see RegionValuesIntersections @@ -39,14 +39,21 @@ final class RegionIntersection { private Region region; private StateValues values1; private StateValues values2; + private StateValues values3; public RegionIntersection(Region region, StateValues values1, StateValues values2) + { + this(region, values1, values2, null); + } + + public RegionIntersection(Region region, StateValues values1, StateValues values2, StateValues values3) { this.region = region; this.values1 = values1; this.values2 = values2; + this.values3 = values3; } - + public Region getRegion() { return region; @@ -61,4 +68,10 @@ final class RegionIntersection { { return values2; } + + public StateValues getStateValues3() + { + return values3; + } + } diff --git a/prism/src/param/RegionValues.java b/prism/src/param/RegionValues.java index e458ff59..852b8af8 100644 --- a/prism/src/param/RegionValues.java +++ b/prism/src/param/RegionValues.java @@ -176,6 +176,40 @@ public final class RegionValues implements Iterable> other.values = otherNewStateValues; } + public void cosplit(RegionValues other, RegionValues other2) + { + this.simplify(); + other.simplify(); + other2.simplify(); + + ArrayList newRegions = new ArrayList(); + HashMap thisNewStateValues = new HashMap(); + HashMap otherNewStateValues = new HashMap(); + HashMap other2NewStateValues = new HashMap(); + for (Region thisRegion : this.regions) { + for (Region otherRegion : other.regions) { + for (Region other2Region : other2.regions) { + Region newRegion = thisRegion.conjunct(otherRegion); + if (newRegion != null) + newRegion = newRegion.conjunct(other2Region); + if (newRegion != null) { + newRegions.add(newRegion); + thisNewStateValues.put(newRegion, this.values.get(thisRegion)); + otherNewStateValues.put(newRegion, other.values.get(otherRegion)); + other2NewStateValues.put(newRegion, other2.values.get(other2Region)); + } + } + } + } + + this.regions = new ArrayList(newRegions); + this.values = thisNewStateValues; + other.regions = new ArrayList(newRegions); + other.values = otherNewStateValues; + other2.regions = new ArrayList(newRegions); + other2.values = other2NewStateValues; + } + @Override public String toString() { @@ -478,4 +512,19 @@ public final class RegionValues implements Iterable> } return result; } + + public RegionValues ITE(RegionValues resT, RegionValues resE) + { + RegionValues result = new RegionValues(factory); + RegionValuesIntersections co = new RegionValuesIntersections(this, resT, resE); + for (RegionIntersection inter : co) { + Region region = inter.getRegion(); + StateValues valueI = inter.getStateValues1(); + StateValues valueT = inter.getStateValues2(); + StateValues valueE = inter.getStateValues3(); + RegionValues values = region.ITE(valueI, valueT, valueE); + result.addAll(values); + } + return result; + } } diff --git a/prism/src/param/RegionValuesIntersections.java b/prism/src/param/RegionValuesIntersections.java index cb00e6d2..b4882427 100644 --- a/prism/src/param/RegionValuesIntersections.java +++ b/prism/src/param/RegionValuesIntersections.java @@ -30,28 +30,33 @@ import java.util.Iterator; import java.util.NoSuchElementException; /** + * Computes the intersections of two (or three) regions. * @author Ernst Moritz Hahn (University of Oxford) */ final class RegionValuesIntersections implements Iterable { final private class RegionIntersectionOperator implements Iterator { private RegionValues regions1; private RegionValues regions2; + private RegionValues regions3; private int numRegions1; private int regions1Index; private boolean hasNext; private Region region; private StateValues stateValues1; private StateValues stateValues2; + private StateValues stateValues3; - RegionIntersectionOperator(RegionValues regions1, RegionValues regions2) + RegionIntersectionOperator(RegionValues regions1, RegionValues regions2, RegionValues regions3) { this.regions1 = regions1; this.regions2 = regions2; + this.regions3 = regions3; regions1Index = 0; numRegions1 = regions1.getNumRegions(); region = null; stateValues1 = null; stateValues2 = null; + stateValues3 = null; findNext(); } @@ -61,7 +66,9 @@ final class RegionValuesIntersections implements Iterable { region = regions1.getRegion(regions1Index); stateValues1 = regions1.getResult(region); stateValues2 = regions2.getResult(region); - found = stateValues2 != null; + stateValues3 = regions3 != null ? regions3.getResult(region) : null; + found = (stateValues2 != null + && (regions3 == null || stateValues3 != null)); regions1Index++; } hasNext = found; @@ -75,7 +82,7 @@ final class RegionValuesIntersections implements Iterable { @Override public RegionIntersection next() { if (hasNext) { - RegionIntersection result = new RegionIntersection(region, stateValues1, stateValues2); + RegionIntersection result = new RegionIntersection(region, stateValues1, stateValues2, stateValues3); findNext(); return result; } else { @@ -91,16 +98,25 @@ final class RegionValuesIntersections implements Iterable { private RegionValues regions1; private RegionValues regions2; + private RegionValues regions3; public RegionValuesIntersections(RegionValues regions1, RegionValues regions2) { regions1.cosplit(regions2); this.regions1 = regions1; this.regions2 = regions2; + this.regions3 = null; + } + + public RegionValuesIntersections(RegionValues regions1, RegionValues regions2, RegionValues regions3) { + regions1.cosplit(regions2, regions3); + this.regions1 = regions1; + this.regions2 = regions2; + this.regions3 = regions3; } @Override public Iterator iterator() { - return new RegionIntersectionOperator(regions1, regions2); + return new RegionIntersectionOperator(regions1, regions2, regions3); } }