Browse Source

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
master
Joachim Klein 8 years ago
committed by Dave Parker
parent
commit
1add0c6de7
  1. 12
      prism-tests/functionality/verify/exact/exact-experiment-1.prism
  2. 6
      prism-tests/functionality/verify/exact/exact-experiment-1.prism.props
  3. 3
      prism-tests/functionality/verify/exact/exact-experiment-1.prism.props.args
  4. 3
      prism/src/parser/ast/Property.java

12
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

6
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]

3
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

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

Loading…
Cancel
Save