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:
a0dfd52
)
Adding a prevChoiceValue class property to store the previous choice to update the...
author
rtrimana
<rtrimana@uci.edu>
Mon, 10 Feb 2020 21:38:03 +0000
(13:38 -0800)
committer
rtrimana
<rtrimana@uci.edu>
Mon, 10 Feb 2020 21:38:03 +0000
(13:38 -0800)
src/main/gov/nasa/jpf/listener/StateReducer.java
patch
|
blob
|
history
diff --git
a/src/main/gov/nasa/jpf/listener/StateReducer.java
b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 2194ff160d3074b2a9325a2c75cab2b97f2d0d1f..474058355c1f7f82f00403cf67705e4d406fd8a5 100644
(file)
--- a/
src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/
src/main/gov/nasa/jpf/listener/StateReducer.java
@@
-87,6
+87,8
@@
public class StateReducer extends ListenerAdapter {
private HashSet<Integer> visitedStateSet;
// Current state
private int stateId;
private HashSet<Integer> visitedStateSet;
// Current state
private int stateId;
+ // Previous choice number
+ private int prevChoiceValue;
public StateReducer(Config config, JPF jpf) {
debugMode = config.getBoolean("debug_state_transition", false);
public StateReducer(Config config, JPF jpf) {
debugMode = config.getBoolean("debug_state_transition", false);
@@
-104,6
+106,7
@@
public class StateReducer extends ListenerAdapter {
vodGraphMap = new HashMap<>();
visitedStateSet = new HashSet<>();
stateId = -1;
vodGraphMap = new HashMap<>();
visitedStateSet = new HashSet<>();
stateId = -1;
+ prevChoiceValue = -1;
initializeStateReduction();
}
initializeStateReduction();
}
@@
-297,17
+300,14
@@
public class StateReducer extends ListenerAdapter {
if (stateReductionMode) {
// Update vodGraph
int currChoice = choiceCounter - 1;
if (stateReductionMode) {
// Update vodGraph
int currChoice = choiceCounter - 1;
- int prevChoice = currChoice - 1;
- if (currChoice < 0) {
+ if (currChoice < 0 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) {
// Current choice has to be at least 0 (initial case can be -1)
// Current choice has to be at least 0 (initial case can be -1)
- visitedStateSet.add(stateId);
return;
}
return;
}
- // Current choice and previous choice values could be -1 (since we use -1 as the end-of-array condition)
- int currChoiceValue = (choices[currChoice] == -1) ? 0 : choices[currChoice];
// When current choice is 0, previous choice could be -1
// When current choice is 0, previous choice could be -1
- int prevChoiceValue = (prevChoice == -1) ? -1 : choices[prevChoice];
- updateVODGraph(prevChoiceValue, currChoiceValue);
+ updateVODGraph(prevChoiceValue, choices[currChoice]);
+ // Current choice becomes previous choice in the next iteration
+ prevChoiceValue = choices[currChoice];
// Line 19 in the paper page 11 (see the heading note above)
stateId = search.getStateId();
// Add state ID into the visited state set
// Line 19 in the paper page 11 (see the heading note above)
stateId = search.getStateId();
// Add state ID into the visited state set