# Potentially conflicting variables
# Alarms
-variables=currentAlarm
+#variables=currentAlarm
# Locks
-#variables=currentLock
+variables=currentLock
# Thermostats
#variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
# Switches
# Tracking the location.mode variable conflict
#track_location_var_conflict=true
+# Timeout in minutes (default is 0 which means no timeout)
+timeout=3
+
#search.class = gov.nasa.jpf.search.heuristic.UserHeuristic
import gov.nasa.jpf.vm.bytecode.StoreInstruction;
import gov.nasa.jpf.vm.bytecode.WriteInstruction;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.List;
+import java.util.*;
// TODO: Fix for Groovy's model-checking
// TODO: This is a listener created to detect device conflicts and global variable conflicts
private final HashSet<String> conflictSet = new HashSet<>();
private final HashSet<String> appSet = new HashSet<>();
private boolean trackLocationVar;
+ private int timeout;
+ private Timer timeoutTimer;
private final String SET_LOCATION_METHOD = "setLocationMode";
private final String LOCATION_VAR = "location.mode";
}
}
trackLocationVar = config.getBoolean("track_location_var_conflict", false);
+ // Timeout is in minutes
+ timeout = config.getInt("timeout", 0);
+ timeoutTimer = null;
+ }
+
+ // Create a task for timer to do a timeout
+ private class TimeoutTask extends TimerTask {
+
+ ThreadInfo ti;
+
+ public TimeoutTask(ThreadInfo ti) {
+ this.ti = ti;
+ }
+
+ @Override
+ public void run() {
+ StringBuilder sb = new StringBuilder();
+ sb.append("Execution timeout!\n");
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+ ti.setNextPC(nextIns);
+ }
}
@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+ // Instantiate timeoutTimer
+ if (timeoutTimer == null && timeout > 0) {
+ ThreadList threads = vm.getThreadList();
+ ThreadInfo mainThread = threads.getThreadInfoForId(0);
+ timeoutTimer = new Timer();
+ timeoutTimer.schedule(new TimeoutTask(mainThread), timeout * 60 * 1000);
+ }
+
// CASE #1: Detecting variable write-after-write conflict
if (executedInsn instanceof WriteInstruction) {
// Check for write-after-write conflict
// Get variable info
byte type = getType(ti, executedInsn);
String value = getValue(ti, executedInsn, type);
+ //System.out.println("\n\n" + ti.getStackTrace() + "\n\n");
String writer = getWriter(ti.getStack());
// Just return if the writer is not one of the listed apps in the .jpf file
if (writer == null)
}
}
}
-
+
private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
if (writeMap.containsKey(var)) {