+
+ public HashMap<Integer, TransitionEvent> getReachableSummaryTransitions(int stateId) {
+ return eventSummary.get(stateId);
+ }
+
+ public HashMap<Integer, ReadWriteSet> getReachableSummaryRWSets(int stateId) {
+ return graphSummary.get(stateId);
+ }
+
+ private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
+ // Combine the same write accesses and record in the recordedRWSet
+ HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
+ HashMap<String, Integer> writeMap = rwSet.getWriteMap();
+ for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
+ String writeField = entry.getKey();
+ // Remove the entry from rwSet if both field and object ID are the same
+ if (writeMap.containsKey(writeField) &&
+ (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
+ writeMap.remove(writeField);
+ }
+ }
+ // Then add everything into the recorded map because these will be traversed
+ recordedWriteMap.putAll(writeMap);
+ // Combine the same read accesses and record in the recordedRWSet
+ HashMap<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
+ HashMap<String, Integer> readMap = rwSet.getReadMap();
+ for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
+ String readField = entry.getKey();
+ // Remove the entry from rwSet if both field and object ID are the same
+ if (readMap.containsKey(readField) &&
+ (readMap.get(readField) == recordedReadMap.get(readField))) {
+ readMap.remove(readField);
+ }
+ }
+ // Then add everything into the recorded map because these will be traversed
+ recordedReadMap.putAll(readMap);
+
+ return rwSet;
+ }
+
+ public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) {
+ // Record transition into graphSummary
+ // TransitionMap maps event (choice) number to a R/W set
+ HashMap<Integer, ReadWriteSet> transitionMap;
+ if (graphSummary.containsKey(stateId)) {
+ transitionMap = graphSummary.get(stateId);
+ } else {
+ transitionMap = new HashMap<>();
+ graphSummary.put(stateId, transitionMap);
+ }
+ int choice = transition.getChoice();
+ ReadWriteSet recordedRWSet;
+ // Insert transition into the map if we haven't had this event number recorded
+ if (!transitionMap.containsKey(choice)) {
+ recordedRWSet = rwSet.getCopy();
+ transitionMap.put(choice, recordedRWSet);
+ // Insert the actual TransitionEvent object into the map
+ HashMap<Integer, TransitionEvent> eventMap = new HashMap<>();
+ eventMap.put(choice, transition);
+ eventSummary.put(stateId, eventMap);
+ } else {
+ recordedRWSet = transitionMap.get(choice);
+ // Perform union and subtraction between the recorded and the given R/W sets
+ rwSet = performUnion(recordedRWSet, rwSet);
+ }
+ return rwSet;
+ }