+ // 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 the execution graph node
+ // 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 HashMap<Integer, ReadWriteSet> readWriteFieldsMap; // Record fields that are accessed
+ private HashMap<Integer, TransitionEvent> stateToTransitionMap; // For O(1) access to backtrack point
+
+ public Execution() {
+ cgToChoiceMap = new HashMap<>();
+ executionTrace = new ArrayList<>();
+ readWriteFieldsMap = new HashMap<>();
+ stateToTransitionMap = new HashMap<>();
+ }
+
+ public void addTransition(TransitionEvent newBacktrackPoint) {
+ executionTrace.add(newBacktrackPoint);
+ }
+
+ public void clearCGToChoiceMap() {
+ cgToChoiceMap = null;
+ }
+
+ public TransitionEvent getTransitionFromState(int stateId) {
+ if (stateToTransitionMap.containsKey(stateId)) {
+ return stateToTransitionMap.get(stateId);
+ }
+ return null;
+ }
+
+ public int getChoiceFromCG(IntChoiceFromSet icsCG) {
+ return cgToChoiceMap.get(icsCG);
+ }
+
+ public ArrayList<TransitionEvent> getExecutionTrace() {
+ return executionTrace;
+ }
+
+ public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
+ return readWriteFieldsMap;
+ }
+
+ public TransitionEvent getFirstTransition() {
+ return executionTrace.get(0);
+ }
+
+ public TransitionEvent getLastTransition() {
+ return executionTrace.get(executionTrace.size() - 1);
+ }
+
+ public boolean isNew() {
+ return executionTrace.size() == 1;
+ }
+
+ public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
+ cgToChoiceMap.put(icsCG, choice);
+ }
+
+ public void mapStateToTransition(int stateId, TransitionEvent backtrackPoint) {
+ stateToTransitionMap.put(stateId, backtrackPoint);
+ }
+ }
+
+ // This class compactly stores a predecessor
+ // 1) a predecessor execution
+ // 2) the predecessor choice in that predecessor execution
+ private class Predecessor {
+ private int predecessorChoice; // Predecessor choice
+ private Execution predecessorExecution; // Predecessor execution
+
+ public Predecessor(int predChoice, Execution predExec) {
+ predecessorChoice = predChoice;
+ predecessorExecution = predExec;
+ }
+
+ public int getPredecessorChoice() {
+ return predecessorChoice;
+ }
+
+ public Execution getPredecessorExecution() {
+ return predecessorExecution;
+ }
+ }
+
+ // This class compactly stores backtrack points:
+ // 1) CG,
+ // 2) state ID,
+ // 3) choice,
+ // 4) predecessors (for backward DFS).
+ private class TransitionEvent {
+ private IntChoiceFromSet transitionCG; // CG at this transition
+ private int stateId; // State at this transition
+ private int choice; // Choice chosen at this transition
+ private Execution execution; // The execution where this transition belongs
+ private int choiceCounter; // Choice counter at this transition
+ private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
+
+ public TransitionEvent() {
+ transitionCG = null;
+ stateId = -1;
+ choice = -1;
+ execution = null;
+ choiceCounter = -1;
+ predecessors = new HashSet<>();
+ }
+
+ public void setTransitionCG(IntChoiceFromSet cg) {
+ transitionCG = cg;
+ }
+
+ public void setStateId(int stId) {
+ stateId = stId;
+ }
+
+ public void setChoice(int cho) {
+ choice = cho;
+ }
+
+ public void setChoiceCounter(int choCounter) {
+ choiceCounter = choCounter;
+ }
+
+ public IntChoiceFromSet getTransitionCG() { return transitionCG; }
+
+ public int getStateId() {
+ return stateId;
+ }
+
+ public int getChoice() {
+ return choice;
+ }
+
+ public int getChoiceCounter() {
+ return choiceCounter;
+ }
+
+ public void setExecution(Execution exec) {
+ execution = exec;
+ }
+
+ public Execution getExecution() {
+ return execution;
+ }
+
+ public HashSet<Predecessor> getPredecessors() {
+ return predecessors;
+ }
+
+ public void recordPredecessor(Execution execution, int choice) {
+ predecessors.add(new Predecessor(choice, execution));
+ }
+ }
+