+ // This class compactly stores backtrack execution:
+ // 1) backtrack choice list, and
+ // 2) first backtrack point (linking with predecessor execution)
+ private class BacktrackExecution {
+ private Integer[] choiceList;
+ private TransitionEvent firstTransition;
+
+ public BacktrackExecution(Integer[] choList, TransitionEvent fTransition) {
+ choiceList = choList;
+ firstTransition = fTransition;
+ }
+
+ public Integer[] getChoiceList() {
+ return choiceList;
+ }
+
+ public TransitionEvent getFirstTransition() {
+ return firstTransition;
+ }
+ }
+
+ // This class stores a representation of an execution
+ // TODO: We can modify this class to implement some optimization (e.g., clock-vector)
+ // TODO: We basically need to keep track of:
+ // TODO: (1) last read/write access to each memory location
+ // TODO: (2) last state with two or more incoming events/transitions
+ private class Execution {
+ private HashMap<IntChoiceFromSet, Integer> cgToChoiceMap; // Map between CG to choice numbers for O(1) access
+ private ArrayList<TransitionEvent> executionTrace; // The BacktrackPoint objects of this execution
+ private boolean isNew; // Track if this is the first time it is accessed
+ private HashMap<Integer, ReadWriteSet> readWriteFieldsMap; // Record fields that are accessed
+
+ public Execution() {
+ cgToChoiceMap = new HashMap<>();
+ executionTrace = new ArrayList<>();
+ isNew = true;
+ readWriteFieldsMap = new HashMap<>();
+ }
+
+ public void addTransition(TransitionEvent newBacktrackPoint) {
+ executionTrace.add(newBacktrackPoint);
+ }
+
+ public void clearCGToChoiceMap() {
+ cgToChoiceMap = null;
+ }
+
+ public int getChoiceFromCG(IntChoiceFromSet icsCG) {
+ return cgToChoiceMap.get(icsCG);
+ }
+
+ public ArrayList<TransitionEvent> getExecutionTrace() {
+ return executionTrace;
+ }
+
+ public TransitionEvent getFirstTransition() {
+ return executionTrace.get(0);
+ }
+
+ public TransitionEvent getLastTransition() {
+ return executionTrace.get(executionTrace.size() - 1);
+ }
+
+ public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
+ return readWriteFieldsMap;
+ }
+
+ public boolean isNew() {
+ if (isNew) {
+ // Right after this is accessed, it is no longer new
+ isNew = false;
+ return true;
+ }
+ return false;
+ }
+
+ public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
+ cgToChoiceMap.put(icsCG, choice);
+ }
+ }
+
+ // This class compactly stores a predecessor
+ // 1) a predecessor execution
+ // 2) the predecessor choice in that predecessor execution
+ private class Predecessor {
+ private int choice; // Predecessor choice
+ private Execution execution; // Predecessor execution
+
+ public Predecessor(int predChoice, Execution predExec) {
+ choice = predChoice;
+ execution = predExec;
+ }
+
+ public int getChoice() {
+ return choice;
+ }
+
+ public Execution getExecution() {
+ return execution;
+ }
+ }
+
+ // This class represents a R-Graph (in the paper it is a state transition graph R)
+ // This implementation stores reachable transitions from and connects with past executions
+ private class RGraph {
+ private int hiStateId; // Maximum state Id
+ private HashMap<Integer, HashSet<TransitionEvent>> graph; // Reachable transitions from past executions
+
+ public RGraph() {
+ hiStateId = 0;
+ graph = new HashMap<>();
+ }
+
+ public void addReachableTransition(int stateId, TransitionEvent transition) {
+ HashSet<TransitionEvent> transitionSet;
+ if (graph.containsKey(stateId)) {
+ transitionSet = graph.get(stateId);
+ } else {
+ transitionSet = new HashSet<>();
+ graph.put(stateId, transitionSet);
+ }
+ // Insert into the set if it does not contain it yet
+ if (!transitionSet.contains(transition)) {
+ transitionSet.add(transition);
+ }
+ // Update highest state ID
+ if (hiStateId < stateId) {
+ hiStateId = 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);
+ }
+
+ public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
+ HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
+ // All transitions from states higher than the given state ID (until the highest state ID) are reachable
+ for(int stId = stateId; stId <= hiStateId; stId++) {
+ // We might encounter state IDs from the first round of Boolean CG
+ // The second round of Boolean CG should consider these new states
+ if (graph.containsKey(stId)) {
+ reachableTransitions.addAll(graph.get(stId));
+ }
+ }
+ return reachableTransitions;
+ }
+ }
+