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.ConflictTrackerOld #listener=gov.nasa.jpf.listener.DPORStateReducer listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld # Potentially conflicting variables # Alarms #variables=currentAlarm # Locks #variables=lock variables=currentLock # Thermostats #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode # Switches #variables=currentSwitch # Lights #variables=colorChanged,currentHue,currentSaturation,currentLevel,currentSwitch,colorTemperature # Dimmers #variables=currentSwitch,currentLevel # Speech Synthesizers #variables=level,oneUser # Music players #variables=status,duration,level,trackDescription,trackData,mute # Relay switches #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 printout_state_transition=true #activate_state_reduction=false file_output=moreStatistics # Timeout in minutes (default is 0 which means no timeout) #timeout=1440 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