From 233e1235b6b878570bfac04ff846489a0b0f5b4d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 14 Sep 2020 20:02:20 +0100 Subject: [PATCH] Fix PrismUtils.doublesAreEqual() and use in more places. Make this method, which is used to check that doubles are (approximately) equal, use relative rather than absolute error, which is more robust in general. This is now used in places where the same check was done, but with an (identical) hard-coded epsilon of 1e-12. Property.getExpectedResultString has also been changed, which previously used 1e-10, but there seems no reason for this not to use 1e-12. --- prism/src/explicit/Distribution.java | 2 +- prism/src/explicit/MDP.java | 4 ++-- prism/src/explicit/MDPSparse.java | 4 ++-- prism/src/explicit/STPGAbstrSimple.java | 4 ++-- prism/src/parser/ast/Property.java | 2 +- prism/src/prism/PrismUtils.java | 2 +- 6 files changed, 9 insertions(+), 9 deletions(-) diff --git a/prism/src/explicit/Distribution.java b/prism/src/explicit/Distribution.java index dfb0b2d8..c7dc1618 100644 --- a/prism/src/explicit/Distribution.java +++ b/prism/src/explicit/Distribution.java @@ -303,7 +303,7 @@ public class Distribution implements Iterable> Map.Entry e = i.next(); d1 = e.getValue(); d2 = d.map.get(e.getKey()); - if (d2 == null || !PrismUtils.doublesAreClose(d1, d2, 1e-12, false)) + if (d2 == null || !PrismUtils.doublesAreEqual(d1, d2)) return false; } return true; diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index fe88c41a..c1c3612a 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -409,7 +409,7 @@ public interface MDP extends MDPGeneric double d = mvMultSingle(s, choice, vect); // Store strategy info if value matches - if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { + if (PrismUtils.doublesAreEqual(val, d)) { result.add(choice); } } @@ -900,7 +900,7 @@ public interface MDP extends MDPGeneric for (int choice = 0, numChoices = getNumChoices(s); choice < numChoices; choice++) { double d = mvMultRewSingle(s, choice, vect, mdpRewards); // Store strategy info if value matches - if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { + if (PrismUtils.doublesAreEqual(val, d)) { result.add(choice); } } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index a7ddd821..9f2e8763 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -855,7 +855,7 @@ public class MDPSparse extends MDPExplicit d += nonZeros[k] * vect[cols[k]]; } // Store strategy info if value matches - if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { + if (PrismUtils.doublesAreEqual(val, d)) { res.add(j - l1); } } @@ -1103,7 +1103,7 @@ public class MDPSparse extends MDPExplicit } d += mdpRewards.getStateReward(s); // Store strategy info if value matches - if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { + if (PrismUtils.doublesAreEqual(val, d)) { res.add(j - l1); } } diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index c7877832..937d058a 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -699,7 +699,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS } // Store strategy info if value matches //if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) { - if (PrismUtils.doublesAreClose(val, minmax2, 1e-12, false)) { + if (PrismUtils.doublesAreEqual(val, minmax2)) { res.add(j); //res.add(distrs.getAction()); } @@ -849,7 +849,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS minmax2 += rewards.getTransitionReward(s, dsIter); // Store strategy info if value matches //if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) { - if (PrismUtils.doublesAreClose(val, minmax2, 1e-12, false)) { + if (PrismUtils.doublesAreEqual(val, minmax2)) { res.add(dsIter); //res.add(distrs.getAction()); } diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java index b65644d3..4fec06c1 100644 --- a/prism/src/parser/ast/Property.java +++ b/prism/src/parser/ast/Property.java @@ -209,7 +209,7 @@ public class Property extends ASTElement match = false; // Check doubles numerically else if (constValToMatch instanceof Double) - match = PrismUtils.doublesAreCloseRel(((Double) constValToMatch).doubleValue(), DefinedConstant.parseDouble(constVal), 1e-10); + match = PrismUtils.doublesAreEqual(((Double) constValToMatch).doubleValue(), DefinedConstant.parseDouble(constVal)); // if constant is exact rational number, compare exactly else if (constValToMatch instanceof BigRational) match = BigRational.from(constVal).equals(constValToMatch); diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index aa88a739..01f834ec 100644 --- a/prism/src/prism/PrismUtils.java +++ b/prism/src/prism/PrismUtils.java @@ -288,7 +288,7 @@ public class PrismUtils */ public static boolean doublesAreEqual(double d1, double d2) { - return doublesAreCloseAbs(d1, d2, epsilonDouble); + return doublesAreCloseRel(d1, d2, epsilonDouble); } /**