projects
/
jpf-core.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
95356fb
)
Adding a counter for number of conflicts.
author
rtrimana
<rtrimana@uci.edu>
Sun, 12 Apr 2020 07:21:43 +0000
(
00:21
-0700)
committer
rtrimana
<rtrimana@uci.edu>
Sun, 12 Apr 2020 07:21:43 +0000
(
00:21
-0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
patch
|
blob
|
history
diff --git
a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index a35286454e3025d6311d0b50c72cb7ab0f538082..22cc82f859545e3e2bdf1d778cdc06c191d34b41 100644
(file)
--- a/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@
-88,7
+88,8
@@
public class DPORStateReducer extends ListenerAdapter {
private boolean isEndOfExecution;
// Statistics
private boolean isEndOfExecution;
// Statistics
- private int numOfTransitions;
+ private int numOfConflicts;
+ private int numOfTransitions;
public DPORStateReducer(Config config, JPF jpf) {
verboseMode = config.getBoolean("printout_state_transition", false);
public DPORStateReducer(Config config, JPF jpf) {
verboseMode = config.getBoolean("printout_state_transition", false);
@@
-99,6
+100,7
@@
public class DPORStateReducer extends ListenerAdapter {
out = null;
}
isBooleanCGFlipped = false;
out = null;
}
isBooleanCGFlipped = false;
+ numOfConflicts = 0;
numOfTransitions = 0;
restorableStateMap = new HashMap<>();
initializeStatesVariables();
numOfTransitions = 0;
restorableStateMap = new HashMap<>();
initializeStatesVariables();
@@
-165,9
+167,14
@@
public class DPORStateReducer extends ListenerAdapter {
@Override
public void searchFinished(Search search) {
@Override
public void searchFinished(Search search) {
+ if (stateReductionMode) {
+ // Number of conflicts = first trace + subsequent backtrack points
+ numOfConflicts += 1 + doneBacktrackSet.size();
+ }
if (verboseMode) {
out.println("\n==> DEBUG: ----------------------------------- search finished");
out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
if (verboseMode) {
out.println("\n==> DEBUG: ----------------------------------- search finished");
out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
+ out.println("\n==> DEBUG: Number of conflicts : " + numOfConflicts);
out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
}
out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
}
@@
-212,6
+219,8
@@
public class DPORStateReducer extends ListenerAdapter {
if (!isBooleanCGFlipped) {
isBooleanCGFlipped = true;
} else {
if (!isBooleanCGFlipped) {
isBooleanCGFlipped = true;
} else {
+ // Number of conflicts = first trace + subsequent backtrack points
+ numOfConflicts = 1 + doneBacktrackSet.size();
// Allocate new objects for data structure when the boolean is flipped from "false" to "true"
initializeStatesVariables();
}
// Allocate new objects for data structure when the boolean is flipped from "false" to "true"
initializeStatesVariables();
}