target = main # This is the listener that can detect variable write-after-write conflicts listener=gov.nasa.jpf.listener.VariableConflictTracker # Potentially conflicting variables # Alarms #variables=currentAlarm # Locks #variables=currentLock # Thermostats #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode # Switches #variables=currentSwitch # Lights #variables=colorChanged,currentHue,currentSaturation,currentLevel,currentSwitch,colorTemperature # Speeches #variables=level,oneUser # Music players #variables=status,duration,level,trackDescription,trackData,mute # Relay switch #variables=currentSwitch # Valves #variables=valve,valveLatestValue # Potentially conflicting apps (we default to App1 and App2 for now) apps=App1,App2 # Tracking the location.mode variable conflict track_location_var_conflict=true # Timeout in minutes (default is 0 which means no timeout) timeout=30 #search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic #search.class = gov.nasa.jpf.search.heuristic.UserHeuristic #search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic #search.class = gov.nasa.jpf.search.heuristic.DFSHeuristic