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:
15a4307
)
Bug fix: when state is not found in rGraph, that means the state is being visited...
author
rtrimana
<rtrimana@uci.edu>
Fri, 19 Jun 2020 18:50:50 +0000
(11:50 -0700)
committer
rtrimana
<rtrimana@uci.edu>
Fri, 19 Jun 2020 18:50:50 +0000
(11:50 -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 ef0994cbdeba690d46c526b1016c54a488bc09dc..13061d8aa03d5559ba740e64bd8fb5079c561d21 100644
(file)
--- a/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@
-352,6
+352,10
@@
public class DPORStateReducer extends ListenerAdapter {
return executionTrace.get(0);
}
return executionTrace.get(0);
}
+ public TransitionEvent getLastTransition() {
+ return executionTrace.get(executionTrace.size() - 1);
+ }
+
public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
return readWriteFieldsMap;
}
public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
return readWriteFieldsMap;
}
@@
-421,6
+425,12
@@
public class DPORStateReducer extends ListenerAdapter {
}
public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
}
public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
+ if (!graph.containsKey(stateId)) {
+ // This is a loop from a transition to itself, so just return the current transition
+ HashSet<TransitionEvent> transitionSet = new HashSet<>();
+ transitionSet.add(currentExecution.getLastTransition());
+ return transitionSet;
+ }
return graph.get(stateId);
}
return graph.get(stateId);
}