Updating classes with Verify API.

diff --git a/Extractor/App1/extractedFunctionsApp1.groovy b/Extractor/App1/extractedFunctionsApp1.groovy
deleted file mode 100644 (file)
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 (file)
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 451100120eea720d6543792b3ecc9d81239f19bd..1f3e9746b0086bb3c8d14dfaf93ed99e8ca412c1 100644 (file)
--- 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 1a0c940bb66ff273d3fc6300b4914d8879f940c5..8ff62ffb4999da90b85c1b74b1770cdfdce4cfe0 100644 (file)
--- 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 675f47a6a8faeb4855f800731e5a401f9b2c5cc0..80b5f49cc825edced9452c3445e15dd202eb88f6 100644 (file)
--- 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 63a213b9852f6b263e997b76446b6cfa86520158..960c66b5a7574912c9d9149074c2066824e847bb 100644 (file)
--- 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 b452ec8dcec4910650230b367553225e423caa93..cf610900283de8442923c8493909feecaffe409c 100644 (file)
--- 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 bb5390a07df9fb8e482c23927fb95f4f5ad1d964..8b6bc4bfa76e58dfdf8b0d6241becaf55225d278 100644 (file)
--- 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 afb3ace98a00990b18e161a32b9bbdede20ad54a..07e1c305b7a4a28e2f94dcfef08d22bb03e59df1 100644 (file)
--- 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 269a419e2212b28945b4514ec31cd91e0e0a9f7f..9c49eb9bc0dfdc68d384c55ce9d4ee796d7130e5 100644 (file)
--- 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 8f0f165f70bf24148786cc2b7cf48187b11242de..fa6d78cccc36225717787752409b0acd333947ff 100644 (file)
--- 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 35c4ad9669d21dbeab9a5b4e8b5b2de7c7836c7f..3990109beda158ce7c7af3aa06938cefe72d4f74 100644 (file)
--- 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 95ed91f53ef4932da998bbd5df383097234a0e89..18602034e8771a7e2d07407ec2269d74c43d1b8b 100644 (file)
--- 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 7e8b22059925795a91e5446ce10b3cfc61d8e747..f12bffd66dbd259ad7bc625d2cfe9f4866248659 100644 (file)
--- 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 10a4cfd6d145043f95622afcff3cb4214d7e07f1..184f2a081506d8e9ea4b6ca527a56a4829108e1d 100644 (file)
--- 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 6c955cea6e3c8df18fec04372294c46ec3951e92..473b9e52e81e2057464ddda59211c4b248996456 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