public class DPORStateReducerWithSummary extends ListenerAdapter {
// Information printout fields for verbose mode
+ private long startTime;
+ private long timeout;
private boolean verboseMode;
private boolean stateReductionMode;
private final PrintWriter out;
// Statistics
private int numOfTransitions;
- private HashMap<Integer, HashSet<Integer>> stateToUniqueEventMap;
+ private HashMap<Integer, HashSet<Integer>> stateToUniqueTransMap;
public DPORStateReducerWithSummary(Config config, JPF jpf) {
verboseMode = config.getBoolean("printout_state_transition", false);
relevantFields = new HashSet<>();
restorableStateMap = new HashMap<>();
stateToPredInfo = new HashMap<>();
- stateToUniqueEventMap = new HashMap<>();
+ stateToUniqueTransMap = new HashMap<>();
initializeStatesVariables();
+
+ // Timeout input from config is in minutes, so we need to convert into millis
+ timeout = config.getInt("timeout", 0) * 60 * 1000;
+ startTime = System.currentTimeMillis();
}
@Override
int summaryOfUniqueTransitions = summarizeUniqueTransitions();
out.println("\n==> DEBUG: ----------------------------------- search finished");
out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
+ if (choices != null) {
+ out.println("\n==> DEBUG: Number of events : " + choices.length);
+ } else {
+ // Without DPOR we don't have choices being assigned with a CG
+ out.println("\n==> DEBUG: Number of events : 0");
+ }
out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode);
+ if (choices != null) {
+ fileWriter.println("==> DEBUG: Number of events : " + choices.length);
+ } else {
+ // Without DPOR we don't have choices being assigned with a CG
+ fileWriter.println("==> DEBUG: Number of events : 0");
+ }
fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
fileWriter.println("==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
fileWriter.println();
} else {
// We only count IntChoiceFromSet CGs
numOfTransitions++;
- countUniqueStateId(vm.getStateId(), icsCG.getNextChoice());
+ countUniqueTransitions(vm.getStateId(), icsCG.getNextChoice());
}
// Map state to event
mapStateToEvent(icsCG.getNextChoice());
@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+ // Check the timeout
+ if (timeout > 0) {
+ if (System.currentTimeMillis() - startTime > timeout) {
+ StringBuilder sbTimeOut = new StringBuilder();
+ sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
+ ti.setNextPC(nextIns);
+ }
+ }
+
if (stateReductionMode) {
if (!isEndOfExecution) {
// Has to be initialized and it is a integer CG
// --- Functions related to statistics counting
// Count unique state IDs
- private void countUniqueStateId(int stateId, int nextChoiceValue) {
+ private void countUniqueTransitions(int stateId, int nextChoiceValue) {
HashSet<Integer> events;
// Get the set of events
- if (!stateToUniqueEventMap.containsKey(stateId)) {
+ if (!stateToUniqueTransMap.containsKey(stateId)) {
events = new HashSet<>();
- stateToUniqueEventMap.put(stateId, events);
+ stateToUniqueTransMap.put(stateId, events);
} else {
- events = stateToUniqueEventMap.get(stateId);
+ events = stateToUniqueTransMap.get(stateId);
}
// Insert the event
if (!events.contains(nextChoiceValue)) {
private int summarizeUniqueTransitions() {
// Just count the set size of each of entry map and sum them up
int numOfUniqueTransitions = 0;
- for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueEventMap.entrySet()) {
+ for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueTransMap.entrySet()) {
numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
}