From 1add0c6de7b8536ceb1496beaefa0e9564dfff8e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 13 Oct 2017 15:41:19 +0200 Subject: [PATCH] Property: support fractions in constant matching part of RESULT specs (experiments) Use DefinedConstant.parseDouble based parsing to handle fractions. For BigRational, this is already supported via BigRational.from() + test case --- .../verify/exact/exact-experiment-1.prism | 12 ++++++++++++ .../verify/exact/exact-experiment-1.prism.props | 6 ++++++ .../verify/exact/exact-experiment-1.prism.props.args | 3 +++ prism/src/parser/ast/Property.java | 3 ++- 4 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 prism-tests/functionality/verify/exact/exact-experiment-1.prism create mode 100644 prism-tests/functionality/verify/exact/exact-experiment-1.prism.props create mode 100644 prism-tests/functionality/verify/exact/exact-experiment-1.prism.props.args diff --git a/prism-tests/functionality/verify/exact/exact-experiment-1.prism b/prism-tests/functionality/verify/exact/exact-experiment-1.prism new file mode 100644 index 00000000..68d018a0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-experiment-1.prism @@ -0,0 +1,12 @@ +// test case for experiments using fractional constants and fractional RESULTs in the property file + +dtmc + +const double p; + +module M1 + s: [0..2] init 0; + + [] s=0 -> p:(s'=1) + 1-p:(s'=2); + [] s>=1 -> true; +endmodule diff --git a/prism-tests/functionality/verify/exact/exact-experiment-1.prism.props b/prism-tests/functionality/verify/exact/exact-experiment-1.prism.props new file mode 100644 index 00000000..1478c9c8 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-experiment-1.prism.props @@ -0,0 +1,6 @@ +// RESULT(p=0): 0 +// RESULT(p=1/3): 1/3 +// RESULT(p=2/3): 2/3 +// RESULT(p=1): 1 +P=?[F s=1] + diff --git a/prism-tests/functionality/verify/exact/exact-experiment-1.prism.props.args b/prism-tests/functionality/verify/exact/exact-experiment-1.prism.props.args new file mode 100644 index 00000000..65b165ef --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-experiment-1.prism.props.args @@ -0,0 +1,3 @@ +-hybrid -const p=0:1/3:1 +-explicit -const p=0:1/3:1 +-exact -const p=0:1/3:1 diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java index 4d4ff881..6fe71c4c 100644 --- a/prism/src/parser/ast/Property.java +++ b/prism/src/parser/ast/Property.java @@ -41,6 +41,7 @@ import prism.PrismException; import prism.PrismLangException; import prism.PrismNotSupportedException; import prism.PrismUtils; +import prism.DefinedConstant; import prism.Point; import prism.Prism; import prism.TileList; @@ -189,7 +190,7 @@ public class Property extends ASTElement match = false; // Check doubles numerically else if (constValToMatch instanceof Double) - match = PrismUtils.doublesAreCloseRel(((Double) constValToMatch).doubleValue(), Double.parseDouble(constVal), 1e-10); + match = PrismUtils.doublesAreCloseRel(((Double) constValToMatch).doubleValue(), DefinedConstant.parseDouble(constVal), 1e-10); // if constant is exact rational number, compare exactly else if (constValToMatch instanceof BigRational) match = BigRational.from(constVal).equals(constValToMatch);