From: rtrimana Date: Fri, 26 Jul 2019 21:13:47 +0000 (-0700) Subject: Adding path explorations for initializations. X-Git-Url: http://plrg.eecs.uci.edu/git/?p=smartthings-infrastructure.git;a=commitdiff_plain;h=9b8d2370b896feb3d8bae8f1aed9c15ea85da222 Adding path explorations for initializations. --- diff --git a/AccelerationSensor/AccelerationSensors.groovy b/AccelerationSensor/AccelerationSensors.groovy index 0d3c14f..8c1992c 100644 --- a/AccelerationSensor/AccelerationSensors.groovy +++ b/AccelerationSensor/AccelerationSensors.groovy @@ -2,6 +2,9 @@ package AccelerationSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class AccelerationSensors { private int deviceNumbers private List accelerationSensors @@ -21,6 +24,14 @@ public class AccelerationSensors { this.deviceNumbers = deviceNumbers this.accelerationSensors = [] + def init = Verify.getBoolean() + if (init) { + this.acceleration = "inactive" + this.accelerationLatestValue = "inactive" + } else { + this.acceleration = "active" + this.accelerationLatestValue = "active" + } accelerationSensors.add(new AccelerationSensor(id, label, displayName, this.acceleration, this.accelerationLatestValue)) } diff --git a/Alarm/Alarms.groovy b/Alarm/Alarms.groovy index 2eb775e..b2759bd 100644 --- a/Alarm/Alarms.groovy +++ b/Alarm/Alarms.groovy @@ -2,6 +2,9 @@ package Alarm import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class Alarms { int deviceNumbers List alarms @@ -22,6 +25,16 @@ public class Alarms { this.deviceNumbers = deviceNumbers this.alarms = [] + def init = Verify.getBoolean() + if (init) { + this.alarm = "off" + this.currentAlarm = "off" + this.alarmLatestValue = "off" + } else { + this.alarm = "on" + this.currentAlarm = "on" + this.alarmLatestValue = "on" + } alarms.add(new Alarm(sendEvent, id, label, displayName, this.alarm, this.currentAlarm, this.alarmLatestValue)) } diff --git a/Battery/Batteries.groovy b/Battery/Batteries.groovy index ce4a187..6e40e12 100644 --- a/Battery/Batteries.groovy +++ b/Battery/Batteries.groovy @@ -2,6 +2,9 @@ package Battery import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class Batteries { private int deviceNumbers private List batteries @@ -19,6 +22,9 @@ public class Batteries { this.sendEvent = sendEvent this.deviceNumbers = deviceNumbers this.batteries = [] + + def init = Verify.getIntFromList(30, 50, 70) + this.battery = init batteries.add(new Battery(id, label, displayName, this.battery)) } diff --git a/BeaconSensor/BeaconSensors.groovy b/BeaconSensor/BeaconSensors.groovy index 24bcfc8..33dd1fe 100644 --- a/BeaconSensor/BeaconSensors.groovy +++ b/BeaconSensor/BeaconSensors.groovy @@ -2,6 +2,9 @@ package BeaconSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class BeaconSensors { private int deviceNumbers private List beaconSensors @@ -21,6 +24,14 @@ public class BeaconSensors { this.deviceNumbers = deviceNumbers this.beaconSensors = [] + def init = Verify.getBoolean() + if (init) { + this.presence = "not present" + this.presenceLatestValue = "not present" + } else { + this.presence = "present" + this.presenceLatestValue = "present" + } beaconSensors.add(new BeaconSensor(id, label, displayName, this.presence, this.presenceLatestValue)) } diff --git a/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy b/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy index 7e848e3..511d031 100644 --- a/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy +++ b/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy @@ -2,6 +2,9 @@ package CarbonMonoxideDetector import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class CarbonMonoxideDetectors { private int deviceNumbers private List carbonMonoxideDetectors @@ -20,8 +23,19 @@ public class CarbonMonoxideDetectors { this.sendEvent = sendEvent this.deviceNumbers = deviceNumbers this.carbonMonoxideDetectors = [] - - carbonMonoxideDetectors.add(new CarbonMonoxideDetector(id, label, displayName, this.currentCarbonMonoxideValue, this.carbonMonoxideLatestValue)) + + def init = Verify.getInt(0,2) + if (init == 0) { + this.carbonMonoxide = "clear" + this.carbonMonoxideLatestValue = "clear" + } else if (init == 1) { + this.carbonMonoxide = "detected" + this.carbonMonoxideLatestValue = "detected" + } else { + this.carbonMonoxide = "tested" + this.carbonMonoxideLatestValue = "tested" + } + carbonMonoxideDetectors.add(new CarbonMonoxideDetector(id, label, displayName, this.carbonMonoxide, this.carbonMonoxideLatestValue)) } //By Model Checker diff --git a/ColorControl/ColorControls.groovy b/ColorControl/ColorControls.groovy index b3a6471..6eb5ac6 100644 --- a/ColorControl/ColorControls.groovy +++ b/ColorControl/ColorControls.groovy @@ -2,6 +2,8 @@ package ColorControl import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify public class ColorControls { private int deviceNumbers @@ -21,6 +23,19 @@ public class ColorControls { this.sendEvent = sendEvent this.deviceNumbers = deviceNumbers this.colorControls = [] + + def initHue = Verify.getIntFromList(30, 50, 70) + this.hue = initHue + def initSat = Verify.getIntFromList(40, 50, 60) + this.saturation = initSat + def init = Verify.getInt(0,2) + if (init == 0) { + this.color = "red" + } else if (init == 1) { + this.color = "green" + } else { + this.color = "blue" + } colorControls.add(new ColorControl(id, label, displayName, this.color, this.hue, this.saturation)) } diff --git a/ContactSensor/ContactSensors.groovy b/ContactSensor/ContactSensors.groovy index 1de8c76..489200d 100644 --- a/ContactSensor/ContactSensors.groovy +++ b/ContactSensor/ContactSensors.groovy @@ -2,6 +2,9 @@ package ContactSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class ContactSensors { private int deviceNumbers private List contacts @@ -22,6 +25,23 @@ public class ContactSensors { this.deviceNumbers = deviceNumbers this.contacts = [] + def initSensor = Verify.getBoolean() + if (initSensor) { + this.contactState = "closed" + this.currentContact = "closed" + this.latestValue = "closed" + } else { + this.contactState = "open" + this.currentContact = "open" + this.latestValue = "open" + } + + def initAlarm = Verify.getBoolean() + if (initAlarm) { + this.alarmState = "armed" + } else { + this.alarmState = "not armed" + } contacts.add(new ContactSensor(id, label, displayName, this.contactState, this.currentContact, this.alarmState, this.latestValue)) } diff --git a/DoorControl/DoorControls.groovy b/DoorControl/DoorControls.groovy index 9210899..444154d 100644 --- a/DoorControl/DoorControls.groovy +++ b/DoorControl/DoorControls.groovy @@ -2,6 +2,9 @@ package DoorControl import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class DoorControls { int deviceNumbers List doorControls @@ -20,7 +23,15 @@ public class DoorControls { this.timers = new SimulatedTimer() this.deviceNumbers = deviceNumbers this.doorControls = [] - + + def init = Verify.getBoolean() + if (init) { + this.doorState = "closed" + this.doorLatestValue = "closed" + } else { + this.doorState = "open" + this.doorLatestValue = "open" + } doorControls.add(new DoorControl(sendEvent, id, label, displayName, this.doorState, this.doorLatestValue)) } diff --git a/EnergyMeter/EnergyMeters.groovy b/EnergyMeter/EnergyMeters.groovy index caec875..5967084 100644 --- a/EnergyMeter/EnergyMeters.groovy +++ b/EnergyMeter/EnergyMeters.groovy @@ -18,7 +18,10 @@ public class EnergyMeters { this.sendEvent = sendEvent this.deviceNumbers = deviceNumbers this.energyMeters = [] - + + def init = Verify.getIntFromList(30, 50, 70) + this.energy = init + energyMeters.add(new EnergyMeter(id, label, displayName, this.energy)) } diff --git a/ImageCapture/ImageCaptures.groovy b/ImageCapture/ImageCaptures.groovy index 2a63a3e..9e5bd9a 100644 --- a/ImageCapture/ImageCaptures.groovy +++ b/ImageCapture/ImageCaptures.groovy @@ -20,6 +20,12 @@ public class ImageCaptures { this.deviceNumbers = deviceNumbers this.imageCaptureSensors = [] + def initAlarm = Verify.getBoolean() + if (initAlarm) { + this.alarmState = "armed" + } else { + this.alarmState = "not armed" + } imageCaptureSensors.add(new ImageCapture(id, label, displayName, this.image, this.alarmState)) } diff --git a/Lock/Locks.groovy b/Lock/Locks.groovy index f792c6c..f2b9d75 100644 --- a/Lock/Locks.groovy +++ b/Lock/Locks.groovy @@ -2,6 +2,9 @@ package Lock import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class Locks{ int deviceNumbers List locks @@ -22,6 +25,14 @@ public class Locks{ this.deviceNumbers = deviceNumbers this.locks = [] + def init = Verify.getBoolean() + if (init) { + this.lockState = "locked" + this.lockLatestValue = "locked" + } else { + this.lockState = "unlocked" + this.lockLatestValue = "unlocked" + } locks.add(new Lock(sendEvent,id, label, displayName, this.lockState, this.lockLatestValue)) } diff --git a/MotionSensor/MotionSensors.groovy b/MotionSensor/MotionSensors.groovy index 863903c..8516713 100644 --- a/MotionSensor/MotionSensors.groovy +++ b/MotionSensor/MotionSensors.groovy @@ -2,6 +2,9 @@ package MotionSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class MotionSensors { private int deviceNumbers private List motionSensors @@ -21,6 +24,14 @@ public class MotionSensors { this.deviceNumbers = deviceNumbers this.motionSensors = [] + def init = Verify.getBoolean() + if (init) { + this.motion = "inactive" + this.motionLatestValue = "inactive" + } else { + this.motion = "active" + this.motionLatestValue = "active" + } motionSensors.add(new MotionSensor(id, label, displayName, this.motion, this.motionLatestValue)) } diff --git a/MusicPlayer/MusicPlayers.groovy b/MusicPlayer/MusicPlayers.groovy index bf733db..847dd1c 100644 --- a/MusicPlayer/MusicPlayers.groovy +++ b/MusicPlayer/MusicPlayers.groovy @@ -2,6 +2,8 @@ package MusicPlayer import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify public class MusicPlayers { private int deviceNumbers @@ -25,6 +27,35 @@ public class MusicPlayers { this.sendEvent = sendEvent this.deviceNumbers = deviceNumbers this.musicPlayers = [] + + def initLevel = Verify.getIntFromList(10, 20, 30) + this.level = initLevel + def initTrack = Verify.getIntFromList(1, 2, 3) + this.trackNumber = initTrack + def initMute = Verify.getBoolean() + if (initMute) { + this.mute = "unmuted" + } else { + this.mute = "mute" + } + def initStatus = Verify.getBoolean() + if (initStatus) { + this.status = "pause" + } else { + this.status = "play" + } + def initTrackData = Verify.getBoolean() + if (initTrackData) { + this.trackData = "someTrack" + } else { + this.trackData = "someOtherTrack" + } + def initTrackDesc = Verify.getBoolean() + if (initTrackDesc) { + this.trackDescription = "someDescriptions" + } else { + this.trackDescription = "someOtherDescriptions" + } musicPlayers.add(new MusicPlayer(id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription)) } diff --git a/PresenceSensor/PresenceSensors.groovy b/PresenceSensor/PresenceSensors.groovy index 2408a5a..cb13242 100644 --- a/PresenceSensor/PresenceSensors.groovy +++ b/PresenceSensor/PresenceSensors.groovy @@ -2,6 +2,9 @@ package PresenceSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class PresenceSensors { private int deviceNumbers private List presenceSensors @@ -20,6 +23,14 @@ public class PresenceSensors { this.sendEvent = sendEvent this.deviceNumbers = deviceNumbers this.presenceSensors = [] + def init = Verify.getBoolean() + if (init) { + this.presence = "not present" + this.presenceLatestValue = "not present" + } else { + this.presence = "present" + this.presenceLatestValue = "present" + } presenceSensors.add(new PresenceSensor(id, label, displayName, this.presence, this.presenceLatestValue)) } diff --git a/SmokeDetector/SmokeDetectors.groovy b/SmokeDetector/SmokeDetectors.groovy index 95bcb3c..e9d5da2 100644 --- a/SmokeDetector/SmokeDetectors.groovy +++ b/SmokeDetector/SmokeDetectors.groovy @@ -2,6 +2,9 @@ package SmokeDetector import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class SmokeDetectors { private int deviceNumbers private List smokeDetectors @@ -21,6 +24,17 @@ public class SmokeDetectors { this.deviceNumbers = deviceNumbers this.smokeDetectors = [] + def init = Verify.getInt(0,2) + if (init == 0) { + this.currentSmokeValue = "clear" + this.smokeLatestValue = "clear" + } else if (init == 1) { + this.currentSmokeValue = "detected" + this.smokeLatestValue = "detected" + } else { + this.currentSmokeValue = "tested" + this.smokeLatestValue = "tested" + } smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue)) } diff --git a/SpeechSynthesis/SpeechSynthesises.groovy b/SpeechSynthesis/SpeechSynthesises.groovy index 033db31..bcdbbd7 100644 --- a/SpeechSynthesis/SpeechSynthesises.groovy +++ b/SpeechSynthesis/SpeechSynthesises.groovy @@ -2,6 +2,9 @@ package SpeechSynthesis import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class SpeechSynthesises { private int deviceNumbers private List speechSynthesises @@ -19,6 +22,9 @@ public class SpeechSynthesises { this.deviceNumbers = deviceNumbers this.speechSynthesises = [] + def init = Verify.getIntFromList(30, 50, 70) + this.level = init + speechSynthesises.add(new SpeechSynthesis(id, label, displayName, this.level)) } diff --git a/Switch/Switches.groovy b/Switch/Switches.groovy index 9007388..36ba2de 100644 --- a/Switch/Switches.groovy +++ b/Switch/Switches.groovy @@ -2,6 +2,9 @@ package Switch import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class Switches { int deviceNumbers List switches @@ -22,6 +25,19 @@ public class Switches { this.timers = new SimulatedTimer() this.deviceNumbers = deviceNumbers this.switches = [] + + def initLevel = Verify.getIntFromList(30, 50, 70) + this.currentLevel = initLevel + def init = Verify.getBoolean() + if (init) { + this.switchState = "off" + this.currentSwitch = "off" + this.switchLatestValue = "off" + } else { + this.switchState = "on" + this.currentSwitch = "on" + this.switchLatestValue = "on" + } switches.add(new Switch(sendEvent, id, label, displayName, this.switchState, this.currentSwitch, this.currentLevel, this.switchLatestValue)) } diff --git a/Thermostat/Thermostats.groovy b/Thermostat/Thermostats.groovy index cc955d1..66957dd 100644 --- a/Thermostat/Thermostats.groovy +++ b/Thermostat/Thermostats.groovy @@ -2,6 +2,9 @@ package Thermostat import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class Thermostats{ int deviceNumbers List thermostats @@ -35,6 +38,51 @@ public class Thermostats{ this.deviceNumbers = deviceNumbers this.thermostats = [] + def initTemperature = Verify.getIntFromList(60, 66, 70) + this.temperature = initTemperature + + def initCoolingSetpoint = Verify.getIntFromList(70, 80, 90) + this.currentCoolingSetpoint = initCoolingSetpoint + this.coolingSetpoint = initCoolingSetpoint + + def initHeatingSetpoint = Verify.getIntFromList(20, 35, 50) + this.currentHeatingSetpoint = initHeatingSetpoint + this.heatingSetpoint = initHeatingSetpoint + + def initThermostatSetpoint = Verify.getIntFromList(50, 60, 70) + this.currentHeatingSetpoint = initThermostatSetpoint + + def initFanMode = Verify.getInt(0,4) + if (initFanMode == 0) { + this.thermostatFanMode = "auto" + } else if (initFanMode == 1) { + this.thermostatFanMode = "fanCirculate" + } else if (initFanMode == 2) { + this.thermostatFanMode = "circulate" + } else if (initFanMode == 3) { + this.thermostatFanMode = "fanOn" + } else { + this.thermostatFanMode = "on" + } + + def initMode = Verify.getInt(0,4) + if (initMode == 0) { + this.thermostatMode = "auto" + this.currentThermostatMode = "auto" + } else if (initMode == 1) { + this.thermostatMode = "cool" + this.currentThermostatMode = "cool" + } else if (initMode == 2) { + this.thermostatMode = "emergencyHeat" + this.currentThermostatMode = "emergencyHeat" + } else if (initMode == 3) { + this.thermostatMode = "heat" + this.currentThermostatMode = "heat" + } else { + this.thermostatMode = "off" + this.currentThermostatMode = "off" + } + thermostats.add(new Thermostat(sendEvent, id, label, displayName, this.temperature, this.currentCoolingSetpoint, this.currentHeatingSetpoint, this.coolingSetpoint, this.thermostatSetpoint, this.heatingSetpoint, this.coolingSetpointRange, this.thermostatSetpointRange, this.heatingSetpointRange, this.supportedThermostatFanModes, this.supportedThermostatModes,