target = main # This is the listener that can detect variable write-after-write conflicts #listener=gov.nasa.jpf.listener.VariableConflictTracker #listener=gov.nasa.jpf.listener.StateReducer #listener=gov.nasa.jpf.listener.StateReducerOld #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerSimple #listener=gov.nasa.jpf.listener.ConflictTracker #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerClean #listener=gov.nasa.jpf.listener.StateReducerClean #listener=gov.nasa.jpf.listener.StateReducer # Potentially conflicting variables # Alarms #variables=currentAlarm # Locks variables=lock # Thermostats #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode # Switches #variables=currentSwitch # Lights #variables=colorChanged,currentHue,currentSaturation,currentLevel,currentSwitch,colorTemperature # Dimmers #variables=currentSwitch,currentLevel # Speeches #variables=level,oneUser # Music players #variables=status,duration,level,trackDescription,trackData,mute # Relay switch #variables=currentSwitch # Valves #variables=valve,valveLatestValue # Cameras #variables=image,alarmState # Location #variables=locationMode # Potentially conflicting apps (we default to App1 and App2 for now) apps=App1,App2 # Debug mode for ConflictTracker # We do not report any conflicts if the value is true debug_mode=true # Debug mode for StateReducer #debug_state_transition=true #activate_state_reduction=true # Timeout in minutes (default is 0 which means no timeout) timeout=30 #search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic #search.heuristic.beam_search=true #search.class = gov.nasa.jpf.search.heuristic.UserHeuristic #search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic #search.class = gov.nasa.jpf.search.heuristic.DFSHeuristic