From b99337e9702d4d6297f09ded7175e66ba3ba0215 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 23 Dec 2020 01:03:43 +0000 Subject: [PATCH] Use model checking accuracy when checking min/max/argmin/argmax filters. --- prism/src/explicit/StateModelChecker.java | 12 ++++-------- prism/src/prism/StateModelChecker.java | 8 ++++---- 2 files changed, 8 insertions(+), 12 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 7a043963..08f5a270 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -1051,8 +1051,7 @@ public class StateModelChecker extends PrismComponent resultExpl = "Minimum value over " + filterStatesString; mainLog.println("\n" + resultExpl + ": " + resObj); // Also find states that (are close to) selected value for display to log - // TODO: un-hard-code precision once StateValues knows hoe precise it is - bsMatch = vals.getBitSetFromCloseValue(resObj, 1e-5, false); + bsMatch = vals.getBitSetFromCloseValue(resObj); bsMatch.and(bsFilter); break; case MAX: @@ -1064,8 +1063,7 @@ public class StateModelChecker extends PrismComponent resultExpl = "Maximum value over " + filterStatesString; mainLog.println("\n" + resultExpl + ": " + resObj); // Also find states that (are close to) selected value for display to log - // TODO: un-hard-code precision once StateValues knows hoe precise it is - bsMatch = vals.getBitSetFromCloseValue(resObj, 1e-5, false); + bsMatch = vals.getBitSetFromCloseValue(resObj); bsMatch.and(bsFilter); break; case ARGMIN: @@ -1073,8 +1071,7 @@ public class StateModelChecker extends PrismComponent resObj = vals.minOverBitSet(bsFilter); mainLog.print("\nMinimum value over " + filterStatesString + ": " + resObj); // Find states that (are close to) selected value - // TODO: un-hard-code precision once StateValues knows hoe precise it is - bsMatch = vals.getBitSetFromCloseValue(resObj, 1e-5, false); + bsMatch = vals.getBitSetFromCloseValue(resObj); bsMatch.and(bsFilter); // Store states in vector; for ARGMIN, don't store a single value (in resObj) // Also, don't bother with explanation string @@ -1088,8 +1085,7 @@ public class StateModelChecker extends PrismComponent resObj = vals.maxOverBitSet(bsFilter); mainLog.print("\nMaximum value over " + filterStatesString + ": " + resObj); // Find states that (are close to) selected value - // TODO: un-hard-code precision once StateValues knows hoe precise it is - bsMatch = vals.getBitSetFromCloseValue(resObj, 1e-5, false); + bsMatch = vals.getBitSetFromCloseValue(resObj); bsMatch.and(bsFilter); // Store states in vector; for ARGMAX, don't store a single value (in resObj) // Also, don't bother with explanation string diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index f5cfc4a2..edc576ad 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -1224,7 +1224,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker resultExpl = "Minimum value over " + filterStatesString; mainLog.println("\n" + resultExpl + ": " + resObj); // Also find states that (are close to) selected value for display to log - ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); + ddMatch = vals.getBDDFromCloseValue(d); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); break; @@ -1238,7 +1238,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker resultExpl = "Maximum value over " + filterStatesString; mainLog.println("\n" + resultExpl + ": " + resObj); // Also find states that (are close to) selected value for display to log - ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); + ddMatch = vals.getBDDFromCloseValue(d); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); break; @@ -1248,7 +1248,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker mainLog.print("\nMinimum value over " + filterStatesString + ": "); mainLog.println(decodeFromDouble(expr.getType(), d)); // Find states that (are close to) selected value - ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); + ddMatch = vals.getBDDFromCloseValue(d); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); // Store states in vector; for ARGMIN, don't store a single value (in resObj) @@ -1264,7 +1264,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker mainLog.print("\nMaximum value over " + filterStatesString + ": "); mainLog.println(decodeFromDouble(expr.getType(), d)); // Find states that (are close to) selected value - ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); + ddMatch = vals.getBDDFromCloseValue(d); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); // Store states in vector; for ARGMAX, don't store a single value (in resObj)