From 71f8000ffd7282505b4d27610d6e697e3c3538bc Mon Sep 17 00:00:00 2001 From: rtrimana <rtrimana@uci.edu> Date: Thu, 21 May 2020 11:27:06 -0700 Subject: [PATCH] Adding different main.jpf files for different detections. --- main.jpf | 4 +-- main_alarms.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_cameras.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_dimmers.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_lights.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_location.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_locks.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_musicplayers.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_relayswitches.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_speeches.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_speechsynthesizers.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_switches.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_thermostats.jpf | 59 +++++++++++++++++++++++++++++++++++++ main_valves.jpf | 59 +++++++++++++++++++++++++++++++++++++ 14 files changed, 769 insertions(+), 2 deletions(-) create mode 100644 main_alarms.jpf create mode 100644 main_cameras.jpf create mode 100644 main_dimmers.jpf create mode 100644 main_lights.jpf create mode 100644 main_location.jpf create mode 100644 main_locks.jpf create mode 100644 main_musicplayers.jpf create mode 100644 main_relayswitches.jpf create mode 100644 main_speeches.jpf create mode 100644 main_speechsynthesizers.jpf create mode 100644 main_switches.jpf create mode 100644 main_thermostats.jpf create mode 100644 main_valves.jpf diff --git a/main.jpf b/main.jpf index da44beb..7a22a41 100644 --- a/main.jpf +++ b/main.jpf @@ -23,11 +23,11 @@ variables=currentLock #variables=colorChanged,currentHue,currentSaturation,currentLevel,currentSwitch,colorTemperature # Dimmers #variables=currentSwitch,currentLevel -# Speeches +# Speech Synthesizers #variables=level,oneUser # Music players #variables=status,duration,level,trackDescription,trackData,mute -# Relay switch +# Relay switches #variables=currentSwitch # Valves #variables=valve,valveLatestValue diff --git a/main_alarms.jpf b/main_alarms.jpf new file mode 100644 index 0000000..b22d55b --- /dev/null +++ b/main_alarms.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_cameras.jpf b/main_cameras.jpf new file mode 100644 index 0000000..e9be248 --- /dev/null +++ b/main_cameras.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_dimmers.jpf b/main_dimmers.jpf new file mode 100644 index 0000000..cc7d5de --- /dev/null +++ b/main_dimmers.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_lights.jpf b/main_lights.jpf new file mode 100644 index 0000000..87190b9 --- /dev/null +++ b/main_lights.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_location.jpf b/main_location.jpf new file mode 100644 index 0000000..459890a --- /dev/null +++ b/main_location.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_locks.jpf b/main_locks.jpf new file mode 100644 index 0000000..7a22a41 --- /dev/null +++ b/main_locks.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_musicplayers.jpf b/main_musicplayers.jpf new file mode 100644 index 0000000..c342b01 --- /dev/null +++ b/main_musicplayers.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_relayswitches.jpf b/main_relayswitches.jpf new file mode 100644 index 0000000..82ce18d --- /dev/null +++ b/main_relayswitches.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_speeches.jpf b/main_speeches.jpf new file mode 100644 index 0000000..da44beb --- /dev/null +++ b/main_speeches.jpf @@ -0,0 +1,59 @@ +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 +# 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 +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 diff --git a/main_speechsynthesizers.jpf b/main_speechsynthesizers.jpf new file mode 100644 index 0000000..98bf757 --- /dev/null +++ b/main_speechsynthesizers.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_switches.jpf b/main_switches.jpf new file mode 100644 index 0000000..c6230e6 --- /dev/null +++ b/main_switches.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_thermostats.jpf b/main_thermostats.jpf new file mode 100644 index 0000000..bb3d330 --- /dev/null +++ b/main_thermostats.jpf @@ -0,0 +1,59 @@ +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 diff --git a/main_valves.jpf b/main_valves.jpf new file mode 100644 index 0000000..2e07437 --- /dev/null +++ b/main_valves.jpf @@ -0,0 +1,59 @@ +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 -- 2.34.1