From: rtrimana Date: Tue, 30 Jul 2019 17:37:18 +0000 (-0700) Subject: Updating classes with Verify API. X-Git-Url: http://plrg.eecs.uci.edu/git/?p=smartthings-infrastructure.git;a=commitdiff_plain;h=0c6e63360c2c1dc55705ced3bf5ddabf22f7abed Updating classes with Verify API. --- diff --git a/Extractor/App1/extractedFunctionsApp1.groovy b/Extractor/App1/extractedFunctionsApp1.groovy deleted file mode 100644 index b7e30e6..0000000 --- a/Extractor/App1/extractedFunctionsApp1.groovy +++ /dev/null @@ -1,12 +0,0 @@ -//Global Object for functions in subscribe method! -def installed = this.&installed -//Global Object for functions in subscribe method! -def updated = this.&updated -//Global Object for functions in subscribe method! -def initialize = this.&initialize -//Global Object for functions in subscribe method! -def lockDoor = this.&lockDoor -//Global Object for functions in subscribe method! -def unlockDoor = this.&unlockDoor -//Global Object for functions in subscribe method! -def doorHandler = this.&doorHandler diff --git a/Extractor/App1/extractedObjectsConstructorApp1.groovy b/Extractor/App1/extractedObjectsConstructorApp1.groovy deleted file mode 100644 index 29bfad5..0000000 --- a/Extractor/App1/extractedObjectsConstructorApp1.groovy +++ /dev/null @@ -1,4 +0,0 @@ -lock1 = obj.lockObject -contact = obj.contactObject -//Global variable for settings! -settings = [app:app, lock1:lock1, contact:contact, minutesLater:minutesLater, secondsLater:secondsLater, recipients:recipients, phoneNumber:phoneNumber] diff --git a/IlluminanceMeasurement/IlluminanceMeasurements.groovy b/IlluminanceMeasurement/IlluminanceMeasurements.groovy index 4511001..1f3e974 100644 --- a/IlluminanceMeasurement/IlluminanceMeasurements.groovy +++ b/IlluminanceMeasurement/IlluminanceMeasurements.groovy @@ -2,6 +2,9 @@ package IlluminanceMeasurement import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class IlluminanceMeasurements { private int deviceNumbers private List illuminanceMeasurements @@ -20,6 +23,9 @@ public class IlluminanceMeasurements { this.deviceNumbers = deviceNumbers this.illuminanceMeasurements = [] + def init = Verify.getIntFromList(40000, 50000, 60000) + this.illuminance = init + illuminanceMeasurements.add(new IlluminanceMeasurement(id, label, displayName, this.illuminance)) } diff --git a/ModelCheck.py b/ModelCheck.py index 1a0c940..8ff62ff 100644 --- a/ModelCheck.py +++ b/ModelCheck.py @@ -58,6 +58,7 @@ firstList = sys.argv[4] # PART 1: Generate the permutations of app pairs print "PHASE 1: Extracting the app pairs from the app lists ...\n" +print "Got here!" appList1 = [] appList2 = [] # Extract the first list diff --git a/MusicPlayer/MusicPlayer.groovy b/MusicPlayer/MusicPlayer.groovy index 675f47a..80b5f49 100644 --- a/MusicPlayer/MusicPlayer.groovy +++ b/MusicPlayer/MusicPlayer.groovy @@ -13,8 +13,10 @@ public class MusicPlayer { private int trackNumber private String trackData private String trackDescription + def sendEvent - MusicPlayer(String id, String label, String displayName, int level, String mute, String status, int trackNumber, String trackData, String trackDescription) { + MusicPlayer(Closure sendEvent, String id, String label, String displayName, int level, String mute, String status, int trackNumber, String trackData, String trackDescription) { + this.sendEvent = sendEvent this.id = id this.label = label this.displayName = displayName diff --git a/MusicPlayer/MusicPlayers.groovy b/MusicPlayer/MusicPlayers.groovy index 63a213b..960c66b 100644 --- a/MusicPlayer/MusicPlayers.groovy +++ b/MusicPlayer/MusicPlayers.groovy @@ -34,16 +34,31 @@ public class MusicPlayers { if (initMute) { this.mute = "unmuted" } else { - this.mute = "mute" + this.mute = "muted" } - def initStatus = Verify.getBoolean() - if (initStatus) { + def initStatus = Verify.getInt(0,2) + if (initStatus == 0) { this.status = "paused" - } else { + } else if (initStatus == 1) { this.status = "playing" + } else { + this.status = "stopped" } - - musicPlayers.add(new MusicPlayer(id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription)) + def initTrack = Verify.getIntFromList(1, 2, 3) + this.trackNumber = initTrack + def initData = Verify.getBoolean() + if (initData) { + this.trackData = "someTrack" + } else { + this.trackData = "someOtherTrack" + } + def initDesc = Verify.getBoolean() + if (initDesc) { + this.trackDescription = "someDescriptions" + } else { + this.trackDescription = "someOtherDescriptions" + } + musicPlayers.add(new MusicPlayer(sendEvent, id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription)) } //By model checker diff --git a/PowerMeter/PowerMeters.groovy b/PowerMeter/PowerMeters.groovy index b452ec8..cf61090 100644 --- a/PowerMeter/PowerMeters.groovy +++ b/PowerMeter/PowerMeters.groovy @@ -2,6 +2,9 @@ package PowerMeter import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class PowerMeters { private int deviceNumbers private List powerMeters @@ -20,6 +23,9 @@ public class PowerMeters { this.deviceNumbers = deviceNumbers this.powerMeters = [] + def init = Verify.getIntFromList(30, 50, 70) + this.power = init + powerMeters.add(new PowerMeter(id, label, displayName, this.power)) } diff --git a/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy b/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy index bb5390a..8b6bc4b 100644 --- a/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy +++ b/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy @@ -2,6 +2,9 @@ package RelativeHumidityMeasurement import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class RelativeHumidityMeasurements { private int deviceNumbers private List humidityMeasurements @@ -20,6 +23,9 @@ public class RelativeHumidityMeasurements { this.deviceNumbers = deviceNumbers this.humidityMeasurements = [] + def init = Verify.getIntFromList(30, 50, 70) + this.humidity = init + humidityMeasurements.add(new RelativeHumidityMeasurement(id, label, displayName, this.humidity)) } diff --git a/RelaySwitch/RelaySwitches.groovy b/RelaySwitch/RelaySwitches.groovy index afb3ace..07e1c30 100644 --- a/RelaySwitch/RelaySwitches.groovy +++ b/RelaySwitch/RelaySwitches.groovy @@ -2,6 +2,9 @@ package RelaySwitch import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class RelaySwitches { int deviceNumbers List relaySwitches @@ -22,6 +25,16 @@ public class RelaySwitches { this.deviceNumbers = deviceNumbers this.relaySwitches = [] + 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" + } relaySwitches.add(new RelaySwitch(sendEvent, id, label, displayName, this.switchState, this.currentSwitch, this.switchLatestValue)) } diff --git a/SleepSensor/SleepSensors.groovy b/SleepSensor/SleepSensors.groovy index 269a419..9c49eb9 100644 --- a/SleepSensor/SleepSensors.groovy +++ b/SleepSensor/SleepSensors.groovy @@ -2,6 +2,9 @@ package SleepSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class SleepSensors { private int deviceNumbers private List sleepSensors @@ -19,6 +22,12 @@ public class SleepSensors { this.deviceNumbers = deviceNumbers this.sleepSensors = [] + def init = Verify.getBoolean() + if (init) { + this.sleeping = "sleeping" + } else { + this.sleeping = "not sleeping" + } sleepSensors.add(new SleepSensor(id, label, displayName, this.sleeping)) } diff --git a/StepSensor/StepSensors.groovy b/StepSensor/StepSensors.groovy index 8f0f165..fa6d78c 100644 --- a/StepSensor/StepSensors.groovy +++ b/StepSensor/StepSensors.groovy @@ -2,6 +2,9 @@ package StepSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class StepSensors { private int deviceNumbers private List stepSensors @@ -20,6 +23,11 @@ public class StepSensors { this.deviceNumbers = deviceNumbers this.stepSensors = [] + def initGoal = Verify.getIntFromList(1000, 2000, 3000) + this.goal = initGoal + def initSteps = Verify.getIntFromList(0, 1, 2) + this.steps = initSteps + stepSensors.add(new StepSensor(id, label, displayName, this.steps, this.goal)) } diff --git a/SwitchLevel/SwitchLevels.groovy b/SwitchLevel/SwitchLevels.groovy index 35c4ad9..3990109 100644 --- a/SwitchLevel/SwitchLevels.groovy +++ b/SwitchLevel/SwitchLevels.groovy @@ -2,6 +2,9 @@ package SwitchLevel import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class SwitchLevels { int deviceNumbers List switchLevels @@ -24,6 +27,18 @@ public class SwitchLevels { this.deviceNumbers = deviceNumbers this.switchLevels = [] + def initLevel = Verify.getIntFromList(30, 50, 70) + this.level = 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" + } switchLevels.add(new SwitchLevel(sendEvent, id, label, displayName, this.level, this.switchState, this.switchLatestValue)) } diff --git a/TemperatureMeasurement/TemperatureMeasurements.groovy b/TemperatureMeasurement/TemperatureMeasurements.groovy index 95ed91f..1860203 100644 --- a/TemperatureMeasurement/TemperatureMeasurements.groovy +++ b/TemperatureMeasurement/TemperatureMeasurements.groovy @@ -2,6 +2,9 @@ package TemperatureMeasurement import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class TemperatureMeasurements { private int deviceNumbers private List temperatureMeasurements @@ -12,14 +15,14 @@ public class TemperatureMeasurements { private String label = "temperatureMeasurement0" private String displayName = "temperatureMeasurement0" private int temperature = 50 - - - TemperatureMeasurements(Closure sendEvent, int deviceNumbers) { this.sendEvent = sendEvent this.deviceNumbers = deviceNumbers this.temperatureMeasurements = [] + + def initTemp = Verify.getIntFromList(30, 50, 70) + this.temperature = initTemp temperatureMeasurements.add(new TemperatureMeasurement(id, label, displayName, this.temperature)) } diff --git a/Valve/Valves.groovy b/Valve/Valves.groovy index 7e8b220..f12bffd 100644 --- a/Valve/Valves.groovy +++ b/Valve/Valves.groovy @@ -2,6 +2,9 @@ package Valve import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class Valves { int deviceNumbers List valves @@ -21,6 +24,14 @@ public class Valves { this.deviceNumbers = deviceNumbers this.valves = [] + def init = Verify.getBoolean() + if (init) { + this.valve = "closed" + this.valveLatestValue = "closed" + } else { + this.valve = "open" + this.valveLatestValue = "open" + } valves.add(new Valve(sendEvent, id, label, displayName, this.valve, this.valveLatestValue)) } diff --git a/WaterSensor/WaterSensors.groovy b/WaterSensor/WaterSensors.groovy index 10a4cfd..184f2a0 100644 --- a/WaterSensor/WaterSensors.groovy +++ b/WaterSensor/WaterSensors.groovy @@ -2,6 +2,9 @@ package WaterSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class WaterSensors { private int deviceNumbers private List waterSensors @@ -19,6 +22,12 @@ public class WaterSensors { this.deviceNumbers = deviceNumbers this.waterSensors = [] + def init = Verify.getBoolean() + if (init) { + this.water = "dry" + } else { + this.water = "wet" + } waterSensors.add(new WaterSensor(id, label, displayName, this.water)) } diff --git a/run.sh b/run.sh index 6c955ce..473b9e5 100755 --- a/run.sh +++ b/run.sh @@ -1,7 +1,8 @@ #!/bin/bash # Device conflict -python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ appLists/device-interaction/locksAppList +#python ModelCheck.py ../jpf-core/ ../logs/locks/ ../smartapps/ appLists/device-interaction/locksAppList +python ModelCheck.py ../jpf-core/ ../logs/musicPlayers/ ../smartapps/ appLists/device-interaction/musicPlayersAppList # Physical conflict #python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ appLists/physical-interaction/soundsensorAppList appLists/physical-interaction/soundAppList