s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Use model checking accuracy when checking min/max/argmin/argmax filters.

accumulation-v4.7
Dave Parker 5 years ago
parent
dd563f254e
commit
b99337e970
2 changed files with 8 additions and 12 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      prism/src/explicit/StateModelChecker.java
  2. 8
      prism/src/prism/StateModelChecker.java

12
prism/src/explicit/StateModelChecker.java
View File

@ -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

8
prism/src/prism/StateModelChecker.java
View File

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

Write Preview
Loading…
Cancel
Save