From 83d05859a187ab523503b6a4e2dc7afee1973bdd Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 3 Apr 2020 12:11:18 +0100 Subject: [PATCH] Allow negative rationals for test mode RESULT specifications. Was previously being parsed as a PRISM expression as a fallback, but the parser currently does not handle big integers. Test case added. And these tests moved to a new "testing" directory. --- .../bugfixes/normaltestwithrationalresult.prism.props | 2 -- .../testing}/normaltestwithrationalresult.prism | 0 .../testing/normaltestwithrationalresult.prism.props | 5 +++++ prism/src/parser/ast/Property.java | 2 +- 4 files changed, 6 insertions(+), 3 deletions(-) delete mode 100644 prism-tests/bugfixes/normaltestwithrationalresult.prism.props rename prism-tests/{bugfixes => functionality/testing}/normaltestwithrationalresult.prism (100%) create mode 100644 prism-tests/functionality/testing/normaltestwithrationalresult.prism.props diff --git a/prism-tests/bugfixes/normaltestwithrationalresult.prism.props b/prism-tests/bugfixes/normaltestwithrationalresult.prism.props deleted file mode 100644 index 0dd68fbb..00000000 --- a/prism-tests/bugfixes/normaltestwithrationalresult.prism.props +++ /dev/null @@ -1,2 +0,0 @@ -// RESULT: 1503982516387544510687823213516750681753609533738014093985492327446021823341670745201522478360759626261166470522913554557570937367804047825330483938531949304640395637223627199/3552713678800500929355621337890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 -"p1": P=? [ F s=5 ]; diff --git a/prism-tests/bugfixes/normaltestwithrationalresult.prism b/prism-tests/functionality/testing/normaltestwithrationalresult.prism similarity index 100% rename from prism-tests/bugfixes/normaltestwithrationalresult.prism rename to prism-tests/functionality/testing/normaltestwithrationalresult.prism diff --git a/prism-tests/functionality/testing/normaltestwithrationalresult.prism.props b/prism-tests/functionality/testing/normaltestwithrationalresult.prism.props new file mode 100644 index 00000000..03183917 --- /dev/null +++ b/prism-tests/functionality/testing/normaltestwithrationalresult.prism.props @@ -0,0 +1,5 @@ +// RESULT: 1503982516387544510687823213516750681753609533738014093985492327446021823341670745201522478360759626261166470522913554557570937367804047825330483938531949304640395637223627199/3552713678800500929355621337890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 +"p1": P=? [ F s=5 ]; + +// RESULT: -1503982516387544510687823213516750681753609533738014093985492327446021823341670745201522478360759626261166470522913554557570937367804047825330483938531949304640395637223627199/3552713678800500929355621337890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 +"neg_p1": -P=? [ F s=5 ]; diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java index b1b59116..cae4ddea 100644 --- a/prism/src/parser/ast/Property.java +++ b/prism/src/parser/ast/Property.java @@ -397,7 +397,7 @@ public class Property extends ASTElement doubleExp = Double.NaN; } // See if it's a fraction - else if (strExpectedValue.matches("[0-9]+/[0-9]+")) { + else if (strExpectedValue.matches("-?[0-9]+/[0-9]+")) { doubleExp = new BigRational(strExpectedValue).doubleValue(); simple = false; // complex expression }