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);