Updating classes with Verify API.
authorrtrimana <rtrimana@uci.edu>
Tue, 30 Jul 2019 17:37:18 +0000 (10:37 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 30 Jul 2019 17:37:18 +0000 (10:37 -0700)
16 files changed:
Extractor/App1/extractedFunctionsApp1.groovy [deleted file]
Extractor/App1/extractedObjectsConstructorApp1.groovy [deleted file]
IlluminanceMeasurement/IlluminanceMeasurements.groovy
ModelCheck.py
MusicPlayer/MusicPlayer.groovy
MusicPlayer/MusicPlayers.groovy
PowerMeter/PowerMeters.groovy
RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy
RelaySwitch/RelaySwitches.groovy
SleepSensor/SleepSensors.groovy
StepSensor/StepSensors.groovy
SwitchLevel/SwitchLevels.groovy
TemperatureMeasurement/TemperatureMeasurements.groovy
Valve/Valves.groovy
WaterSensor/WaterSensors.groovy
run.sh

diff --git a/Extractor/App1/extractedFunctionsApp1.groovy b/Extractor/App1/extractedFunctionsApp1.groovy
deleted file mode 100644 (file)
index b7e30e6..0000000
+++ /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 (file)
index 29bfad5..0000000
+++ /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]
index 4511001..1f3e974 100644 (file)
@@ -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))
        }
 
index 1a0c940..8ff62ff 100644 (file)
@@ -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
index 675f47a..80b5f49 100644 (file)
@@ -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
index 63a213b..960c66b 100644 (file)
@@ -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
index b452ec8..cf61090 100644 (file)
@@ -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))
        }
 
index bb5390a..8b6bc4b 100644 (file)
@@ -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))
        }
 
index afb3ace..07e1c30 100644 (file)
@@ -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))
        }
 
index 269a419..9c49eb9 100644 (file)
@@ -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))
        }
 
index 8f0f165..fa6d78c 100644 (file)
@@ -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))
        }
 
index 35c4ad9..3990109 100644 (file)
@@ -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))
        }
 
index 95ed91f..1860203 100644 (file)
@@ -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))
        }
index 7e8b220..f12bffd 100644 (file)
@@ -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))
        }
 
index 10a4cfd..184f2a0 100644 (file)
@@ -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 (executable)
--- 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