Browse Source

Store vector in Result during model checking if requested.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8402 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
commit
b7864791dc
  1. 13
      prism/src/explicit/StateModelChecker.java
  2. 11
      prism/src/prism/StateModelChecker.java

13
prism/src/explicit/StateModelChecker.java

@ -36,6 +36,8 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
import jdd.JDD;
import parser.State;
import parser.Values;
import parser.ast.Expression;
@ -323,7 +325,8 @@ public class StateModelChecker extends PrismComponent
mainLog.print("\n" + resultString + "\n");
// Clean up
vals.clear();
//vals.clear();
result.setVector(vals);
// Return result
return result;
@ -967,10 +970,12 @@ public class StateModelChecker extends PrismComponent
} else {
result.setExplanation(null);
}
// Clear up
if (vals != null)
// Store vector if requested (and if not, clear it)
if (storeVector) {
result.setVector(vals);
} else if (vals != null) {
vals.clear();
}
return resVals;
}

11
prism/src/prism/StateModelChecker.java

@ -1332,11 +1332,14 @@ public class StateModelChecker implements ModelChecker
} else {
result.setExplanation(null);
}
// Derefs, clears
JDD.Deref(ddFilter);
if (vals != null)
// Store vector if requested (and if not, clear it)
if (storeVector) {
result.setVector(vals);
} else if (vals != null) {
vals.clear();
}
// Other derefs
JDD.Deref(ddFilter);
return resVals;
}

Loading…
Cancel
Save