Changing Verify API call scheme for device handlers.

diff --git a/AccelerationSensor/AccelerationSensors.groovy b/AccelerationSensor/AccelerationSensors.groovy
index 7df4347f47bea0915b29841bea4374132309c9d9..7cfe1d08094f25c1fbcbb25186df96ce349ca1ab 100644 (file)
--- a/AccelerationSensor/AccelerationSensors.groovy
+++ b/AccelerationSensor/AccelerationSensors.groovy
@@ -2,9 +2,6 @@
 package AccelerationSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class AccelerationSensors {
        private int deviceNumbers
        private List accelerationSensors
@@ -20,19 +17,18 @@ public class AccelerationSensors {
        
 
                
-       AccelerationSensors(Closure sendEvent, int deviceNumbers) {
+       AccelerationSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                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/AeonKeyFob/AeonKeyFobs.groovy b/AeonKeyFob/AeonKeyFobs.groovy
index 6383898b5538d9af16ea8f8fc0d6375d628b0d57..f001f0d8fe0ce3b126eb4528c3594ccd96650e41 100644 (file)
--- a/AeonKeyFob/AeonKeyFobs.groovy
+++ b/AeonKeyFob/AeonKeyFobs.groovy
@@ -2,9 +2,6 @@
 package AeonKeyFob
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class AeonKeyFobs {
        private int deviceNumbers
        private List aeonKeyFobs

diff --git a/Alarm/Alarms.groovy b/Alarm/Alarms.groovy
index 30c55d9b537ac70d6e9a7a3c3507b6da344914e2..7e5edd408eb6fe26ab8bd0c92db7cde18d5d74c3 100644 (file)
--- a/Alarm/Alarms.groovy
+++ b/Alarm/Alarms.groovy
@@ -2,9 +2,6 @@
 package Alarm
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class Alarms {
        int deviceNumbers       
        List alarms
@@ -19,13 +16,12 @@ public class Alarms {
        private String currentAlarm = "off"
        private String alarmLatestValue = "off"
 
-       Alarms(Closure sendEvent, int deviceNumbers) {
+       Alarms(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.alarms = []
 
-               /*def init = Verify.getBoolean()
                if (init) {
                        this.alarm = "off"
                        this.currentAlarm = "off"
@@ -34,7 +30,7 @@ public class Alarms {
                        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 d7d8f1b348e314ae440019b989d6a4d74ac6e9d6..732b6bdec6dc49a42b1b72e5031713029644c2ad 100644 (file)
--- a/Battery/Batteries.groovy
+++ b/Battery/Batteries.groovy
@@ -2,9 +2,6 @@
 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,13 +16,20 @@ public class Batteries {
        private int batteryLatestValue = 50
 
                
-       Batteries(Closure sendEvent, int deviceNumbers) {
+       Batteries(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.batteries = []
 
-               //def init = Verify.getIntFromList(30, 50, 70)
-               //this.battery = init
+               if (init) {
+                       this.battery = 50
+                       this.currentBattery = 50
+                       this.batteryLatestValue = 50
+               } else {
+                       this.battery = 35
+                       this.currentBattery = 35
+                       this.batteryLatestValue = 35
+               }
 
                batteries.add(new Battery(id, label, displayName, this.battery))
        }

diff --git a/BeaconSensor/BeaconSensors.groovy b/BeaconSensor/BeaconSensors.groovy
index 0e9996f89fde3e8e42b785deb42bc0ece00df485..4550965ad876a28d4c30425ee5fb257a4914d145 100644 (file)
--- a/BeaconSensor/BeaconSensors.groovy
+++ b/BeaconSensor/BeaconSensors.groovy
@@ -2,9 +2,6 @@
 package BeaconSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class BeaconSensors {
        private int deviceNumbers
        private List beaconSensors
@@ -19,19 +16,20 @@ public class BeaconSensors {
        private String presenceLatestValue = "not present"
 
                
-       BeaconSensors(Closure sendEvent, int deviceNumbers) {
+       BeaconSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.beaconSensors = []
 
-               /*def init = Verify.getBoolean()
                if (init) {
                        this.presence = "not present"
+                       this.currentPresence = "not present"
                        this.presenceLatestValue = "not present"
                } else {
                        this.presence = "present"
+                       this.currentPresence = "present"
                        this.presenceLatestValue = "present"
-               }*/
+               }
                beaconSensors.add(new BeaconSensor(id, label, displayName, this.presence, this.presenceLatestValue))
        }
 

diff --git a/Button/Buttons.groovy b/Button/Buttons.groovy
index 423b9569fdb44a6a9a1a1cda6fcfbb118e891920..f15a30072aeee0f4033dd80e65ee454cb4542a9f 100644 (file)
--- a/Button/Buttons.groovy
+++ b/Button/Buttons.groovy
@@ -2,9 +2,6 @@
 package Button
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class Buttons {
        private int deviceNumbers
        private List buttons
@@ -18,11 +15,16 @@ public class Buttons {
        private int numberOfButtons = 4
        
                
-       Buttons(Closure sendEvent, int deviceNumbers) {
+       Buttons(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.buttons = []
 
+               if (init) {
+                       this.button = "pushed"
+               } else {
+                       this.button = "held"
+               }
                buttons.add(new Button(id, label, displayName, button, numberOfButtons))
        }
 

diff --git a/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy b/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy
index 21aa5921e70436446e84caf2b5dca80c093c5f57..ba828d7d0542a73be5dee54e167adceb4f14e84f 100644 (file)
--- a/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy
+++ b/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy
@@ -2,9 +2,6 @@
 package CarbonMonoxideDetector
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class CarbonMonoxideDetectors {
        private int deviceNumbers
        private List carbonMonoxideDetectors
@@ -19,22 +16,20 @@ public class CarbonMonoxideDetectors {
        private String carbonMonoxideLatestValue = "clear"
 
                
-       CarbonMonoxideDetectors(Closure sendEvent, int deviceNumbers) {
+       CarbonMonoxideDetectors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.carbonMonoxideDetectors = []
                
-               /*def init = Verify.getInt(0,2)
-               if (init == 0) {
+               if (init) {
                        this.carbonMonoxide = "clear"
+                       this.currentCarbonMonoxideValue = "clear"
                        this.carbonMonoxideLatestValue = "clear"
                } else if (init == 1) {
                        this.carbonMonoxide = "detected"
+                       this.currentCarbonMonoxideValue = "detected"
                        this.carbonMonoxideLatestValue = "detected"
-               } else {
-                       this.carbonMonoxide = "tested"
-                       this.carbonMonoxideLatestValue = "tested"               
-               }*/
+               }
                carbonMonoxideDetectors.add(new CarbonMonoxideDetector(id, label, displayName, this.currentCarbonMonoxideValue, this.carbonMonoxideLatestValue))
        }
 

diff --git a/ColorControl/ColorControls.groovy b/ColorControl/ColorControls.groovy
index a85298d2ebbd9b459c6eeb4c572ae6d42dd8bfa4..6fc62aa14461788cf41218f7f2828ffaa9edd9b6 100644 (file)
--- a/ColorControl/ColorControls.groovy
+++ b/ColorControl/ColorControls.groovy
@@ -2,9 +2,6 @@
 package ColorControl
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class ColorControls {
        private int deviceNumbers
        private List colorControls
@@ -26,27 +23,22 @@ public class ColorControls {
        private int colorTemperature = 15000
        
 
-       ColorControls(Closure sendEvent, int deviceNumbers) {
+       ColorControls(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.deviceNumbers = deviceNumbers
                this.colorControls = []
 
-               /*def initHue = Verify.getIntFromList(30, 50)
-               this.hue = initHue
-               def initSat = Verify.getIntFromList(40, 50)
-               this.saturation = initSat
-               def initColor = Verify.getBoolean()
-               if (initColor) {
-                       this.color = "red"
-               } else {
-                       this.color = "blue"
-               }
-               def init = Verify.getBoolean()
                if (init) {
+                       this.hue = 30
+                       this.saturation = 40
+                       this.color = "red"
                        this.currentSwitch = "off"
                } else {
+                       this.hue = 50
+                       this.saturation = 50
+                       this.color = "blue"
                        this.currentSwitch = "on"
-               }*/
+               }
 
                colorControls.add(new ColorControl(sendEvent, id, label, displayName, this.color, this.hue, this.saturation, this.level, this.currentSwitch, this.colorTemperature))
        }

diff --git a/ColorTemperature/ColorTemperatures.groovy b/ColorTemperature/ColorTemperatures.groovy
index 99fe7e6a22f752794f3da630ebac18d2e2c87c99..d3826804318a6448eff9382233a52bfd1b0043e3 100644 (file)
--- a/ColorTemperature/ColorTemperatures.groovy
+++ b/ColorTemperature/ColorTemperatures.groovy
@@ -2,9 +2,6 @@
 package ColorTemperature
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class ColorTemperatures {
        private int deviceNumbers
        private List colorTemperatues
@@ -20,21 +17,20 @@ public class ColorTemperatures {
        private int colorTemperature = 15000
        
 
-       ColorTemperatures(Closure sendEvent, int deviceNumbers) {
+       ColorTemperatures(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.deviceNumbers = deviceNumbers
                this.colorTemperatues = []
 
-               /*def initLevel = Verify.getIntFromList(50, 70)
-               this.level = initLevel 
-               def initTemp = Verify.getIntFromList(10000, 15000)
-               this.colorTemperature = initTemp 
-               def init = Verify.getBoolean()
                if (init) {
-                       this.currentSwitch = "off"
+                       this.level = 30
+                       this.currentLevel = 40
+                       this.colorTemperature = 10000
                } else {
-                       this.currentSwitch = "on"
-               }*/
+                       this.level = 50
+                       this.currentLevel = 50
+                       this.colorTemperature = 15000
+               }
 
                colorTemperatues.add(new ColorTemperature(sendEvent, id, label, displayName, this.level, this.currentSwitch, this.colorTemperature))
        }

diff --git a/ContactSensor/ContactSensors.groovy b/ContactSensor/ContactSensors.groovy
index 5f5f20e97b9ad97e13bcdfd96493de08f0c53141..c4136e301a843a3f836dea903abddf68a4c1940f 100644 (file)
--- a/ContactSensor/ContactSensors.groovy
+++ b/ContactSensor/ContactSensors.groovy
@@ -2,9 +2,6 @@
 package ContactSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class ContactSensors {
        private int deviceNumbers
        private List contacts
@@ -20,10 +17,22 @@ public class ContactSensors {
        private String alarmState = "armed"
 
                
-       ContactSensors(Closure sendEvent, int deviceNumbers) {
+       ContactSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.contacts = []
+               
+               if (init) {
+                       this.contactState = "closed"
+                       this.currentContact = "closed"
+                       this.latestValue = "closed"
+                       this.alarmState = "armed"
+               } else {
+                       this.contactState = "open"
+                       this.currentContact = "open"
+                       this.latestValue = "open"
+                       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 ac6decc59c64343620a1f696cca6c5322a53c8cc..5327be01e731bec554808bb79b3ab406318940fb 100644 (file)
--- a/DoorControl/DoorControls.groovy
+++ b/DoorControl/DoorControls.groovy
@@ -2,9 +2,6 @@
 package DoorControl
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class DoorControls {
        int deviceNumbers       
        List doorControls
@@ -18,20 +15,19 @@ public class DoorControls {
        private String doorState = "closed"
        private String doorLatestValue = "closed"
 
-       DoorControls(Closure sendEvent, int deviceNumbers) {
+       DoorControls(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                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 907ec6680065932c3f48f59e65cbc1e5e660b17f..d5a7aea62e626dbb07e35b433d82b52ccd396cff 100644 (file)
--- a/EnergyMeter/EnergyMeters.groovy
+++ b/EnergyMeter/EnergyMeters.groovy
@@ -2,9 +2,6 @@
 package EnergyMeter
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class EnergyMeters {
        private int deviceNumbers
        private List energyMeters
@@ -18,14 +15,18 @@ public class EnergyMeters {
        private int currentEnergy = 50
 
                
-       EnergyMeters(Closure sendEvent, int deviceNumbers) {
+       EnergyMeters(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.energyMeters = []
 
-               //def init = Verify.getIntFromList(30, 50, 70)
-               //this.energy = init
-
+               if (init) {
+                       this.energy = 50
+                       this.currentEnergy = 50
+               } else {
+                       this.energy = 60
+                       this.currentEnergy = 60
+               }
                energyMeters.add(new EnergyMeter(id, label, displayName, this.energy))
        }
 

diff --git a/Extractor/Extractor.groovy b/Extractor/Extractor.groovy
index c8c7019118e6b22e62a929ef5b22c78a7eb6de07..4c90690d7266816e62564a6e679c21e3e9b30280 100644 (file)
--- a/Extractor/Extractor.groovy
+++ b/Extractor/Extractor.groovy
@@ -413,22 +413,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def lockObject = new Locks(sendEvent, 1)\n")
+                               globalObjects.append("@Field def lockObject = new Locks(sendEvent, 1, init)\n")
 
                        if (lockObjects == 0) {
                                lockObject0 = metaData['name']
-                               this[lockObject0] = new Locks({}, 1)
+                               this[lockObject0] = new Locks({}, 1, true)
                        } else if (lockObjects == 1) {
                                lockObject1 = metaData['name']
-                               this[lockObject1] = new Locks({}, 1)
+                               this[lockObject1] = new Locks({}, 1, true)
                        } else if (lockObjects == 2) {
                                lockObject2 = metaData['name']
-                               this[lockObject2] = new Locks({}, 1)
+                               this[lockObject2] = new Locks({}, 1, true)
                        }
 
                        lockObjects=lockObjects+1
 
-                       settings.put(metaData['name'], new Locks({}, 1)) 
+                       settings.put(metaData['name'], new Locks({}, 1, true)) 
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class lock!\n")
@@ -448,22 +448,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def alarmObject = new Alarms(sendEvent, 1)\n")
+                               globalObjects.append("@Field def alarmObject = new Alarms(sendEvent, 1, init)\n")
 
                        if (alarmObjects == 0) {
                                alarmObject0 = metaData['name']
-                               this[alarmObject0] = new Alarms({}, 1)
+                               this[alarmObject0] = new Alarms({}, 1, true)
                        } else if (alarmObjects == 1) {
                                alarmObject1 = metaData['name']
-                               this[alarmObject1] = new Alarms({}, 1)
+                               this[alarmObject1] = new Alarms({}, 1, true)
                        } else if (alarmObjects == 2) {
                                alarmObject2 = metaData['name']
-                               this[alarmObject2] = new Alarms({}, 1)
+                               this[alarmObject2] = new Alarms({}, 1, true)
                        }
 
                        alarmObjects=alarmObjects+1
 
-                       settings.put(metaData['name'], new Alarms({}, 1)) 
+                       settings.put(metaData['name'], new Alarms({}, 1, true)) 
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class alarm!\n")
@@ -483,22 +483,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def buttonObject = new Buttons(sendEvent, 1)\n")
+                               globalObjects.append("@Field def buttonObject = new Buttons(sendEvent, 1, init)\n")
 
                        if (buttonObjects == 0) {
                                buttonObject0 = metaData['name']
-                               this[buttonObject0] = new Buttons({}, 1)
+                               this[buttonObject0] = new Buttons({}, 1, true)
                        } else if (buttonObjects == 1) {
                                buttonObject1 = metaData['name']
-                               this[buttonObject1] = new Buttons({}, 1)
+                               this[buttonObject1] = new Buttons({}, 1, true)
                        } else if (buttonObjects == 2) {
                                buttonObject2 = metaData['name']
-                               this[buttonObject2] = new Buttons({}, 1)
+                               this[buttonObject2] = new Buttons({}, 1, true)
                        }
 
                        buttonObjects=buttonObjects+1
 
-                       settings.put(metaData['name'], new Buttons({}, 1))
+                       settings.put(metaData['name'], new Buttons({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class Button!\n")
@@ -518,22 +518,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def batteryObject = new Batteries(sendEvent, 1)\n")
+                               globalObjects.append("@Field def batteryObject = new Batteries(sendEvent, 1, init)\n")
 
                        if (batteryObjects == 0) {
                                batteryObject0 = metaData['name']
-                               this[batteryObject0] = new Batteries({}, 1)
+                               this[batteryObject0] = new Batteries({}, 1, true)
                        } else if (batteryObjects == 1) {
                                batteryObject1 = metaData['name']
-                               this[batteryObject1] = new Batteries({}, 1)
+                               this[batteryObject1] = new Batteries({}, 1, true)
                        } else if (batteryObjects == 2) {
                                batteryObject2 = metaData['name']
-                               this[batteryObject2] = new Batteries({}, 1)
+                               this[batteryObject2] = new Batteries({}, 1, true)
                        }
 
                        batteryObjects=batteryObjects+1
 
-                       settings.put(metaData['name'], new Batteries({}, 1))
+                       settings.put(metaData['name'], new Batteries({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class Battery!\n")
@@ -553,22 +553,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def beaconSensorObject = new BeaconSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def beaconSensorObject = new BeaconSensors(sendEvent, 1, init)\n")
 
                        if (beaconSensorObjects == 0) {
                                beaconSensorObject0 = metaData['name']
-                               this[beaconSensorObject0] = new BeaconSensors({}, 1)
+                               this[beaconSensorObject0] = new BeaconSensors({}, 1, true)
                        } else if (beaconSensorObjects == 1) {
                                beaconSensorObject1 = metaData['name']
-                               this[beaconSensorObject1] = new BeaconSensors({}, 1)
+                               this[beaconSensorObject1] = new BeaconSensors({}, 1, true)
                        } else if (beaconSensorObjects == 2) {
                                beaconSensorObject2 = metaData['name']
-                               this[beaconSensorObject2] = new BeaconSensors({}, 1)
+                               this[beaconSensorObject2] = new BeaconSensors({}, 1, true)
                        }
 
                        beaconSensorObjects=beaconSensorObjects+1
 
-                       settings.put(metaData['name'], new BeaconSensors({}, 1))
+                       settings.put(metaData['name'], new BeaconSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class beacon sensor!\n")
@@ -588,22 +588,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def carbonMonoxideDetectorObject = new CarbonMonoxideDetectors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def carbonMonoxideDetectorObject = new CarbonMonoxideDetectors(sendEvent, 1, init)\n")
 
                        if (carbonMonoxideDetectorObjects == 0) {
                                carbonMonoxideDetectorObject0 = metaData['name']
-                               this[carbonMonoxideDetectorObject0] = new CarbonMonoxideDetectors({}, 1)
+                               this[carbonMonoxideDetectorObject0] = new CarbonMonoxideDetectors({}, 1, true)
                        } else if (carbonMonoxideDetectorObjects == 1) {
                                carbonMonoxideDetectorObject1 = metaData['name']
-                               this[carbonMonoxideDetectorObject1] = new CarbonMonoxideDetectors({}, 1)
+                               this[carbonMonoxideDetectorObject1] = new CarbonMonoxideDetectors({}, 1, true)
                        } else if (carbonMonoxideDetectorObjects == 2) {
                                carbonMonoxideDetectorObject2 = metaData['name']
-                               this[carbonMonoxideDetectorObject2] = new CarbonMonoxideDetectors({}, 1)
+                               this[carbonMonoxideDetectorObject2] = new CarbonMonoxideDetectors({}, 1, true)
                        }
 
                        carbonMonoxideDetectorObjects=carbonMonoxideDetectorObjects+1
                        
-                       settings.put(metaData['name'], new CarbonMonoxideDetectors({}, 1))
+                       settings.put(metaData['name'], new CarbonMonoxideDetectors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class carbon monoxide detector!\n")
@@ -623,22 +623,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def colorTemperatureObject = new ColorTemperatures(sendEvent, 1)\n")
+                               globalObjects.append("@Field def colorTemperatureObject = new ColorTemperatures(sendEvent, 1, init)\n")
 
                        if (colorTemperatureObjects == 0) {
                                colorTemperatureObject0 = metaData['name']
-                               this[colorTemperatureObject0] = new ColorTemperatures({}, 1)
+                               this[colorTemperatureObject0] = new ColorTemperatures({}, 1, true)
                        } else if (colorTemperatureObjects == 1) {
                                colorTemperatureObject1 = metaData['name']
-                               this[colorTemperatureObject1] = new ColorTemperatures({}, 1)
+                               this[colorTemperatureObject1] = new ColorTemperatures({}, 1, true)
                        } else if (colorTemperatureObjects == 2) {
                                colorTemperatureObject2 = metaData['name']
-                               this[colorTemperatureObject2] = new ColorTemperatures({}, 1)
+                               this[colorTemperatureObject2] = new ColorTemperatures({}, 1, true)
                        }
 
                        colorTemperatureObjects=colorTemperatureObjects+1
 
-                       settings.put(metaData['name'], new ColorTemperatures({}, 1))
+                       settings.put(metaData['name'], new ColorTemperatures({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class color temperature!\n")
@@ -658,22 +658,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def colorControlObject = new ColorControls(sendEvent, 1)\n")
+                               globalObjects.append("@Field def colorControlObject = new ColorControls(sendEvent, 1, init)\n")
 
                        if (colorControlObjects == 0) {
                                colorControlObject0 = metaData['name']
-                               this[colorControlObject0] = new ColorControls({}, 1)
+                               this[colorControlObject0] = new ColorControls({}, 1, true)
                        } else if (colorControlObjects == 1) {
                                colorControlObject1 = metaData['name']
-                               this[colorControlObject1] = new ColorControls({}, 1)
+                               this[colorControlObject1] = new ColorControls({}, 1, true)
                        } else if (colorControlObjects == 2) {
                                colorControlObject2 = metaData['name']
-                               this[colorControlObject2] = new ColorControls({}, 1)
+                               this[colorControlObject2] = new ColorControls({}, 1, true)
                        }
 
                        colorControlObjects=colorControlObjects+1
 
-                       settings.put(metaData['name'], new ColorControls({}, 1))
+                       settings.put(metaData['name'], new ColorControls({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class color control!\n")
@@ -693,22 +693,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def contactObject = new ContactSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def contactObject = new ContactSensors(sendEvent, 1, init)\n")
 
                        if (contactObjects == 0) {
                                contactObject0 = metaData['name']
-                               this[contactObject0] = new ContactSensors({}, 1)
+                               this[contactObject0] = new ContactSensors({}, 1, true)
                        } else if (contactObjects == 1) {
                                contactObject1 = metaData['name']
-                               this[contactObject1] = new ContactSensors({}, 1)
+                               this[contactObject1] = new ContactSensors({}, 1, true)
                        } else if (contactObjects == 2) {
                                contactObject2 = metaData['name']
-                               this[contactObject2] = new ContactSensors({}, 1)
+                               this[contactObject2] = new ContactSensors({}, 1, true)
                        }
 
                        contactObjects=contactObjects+1
 
-                       settings.put(metaData['name'], new ContactSensors({}, 1))
+                       settings.put(metaData['name'], new ContactSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class contactSensor!\n")
@@ -728,22 +728,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def threeAxisObject = new ThreeAxises(sendEvent, 1)\n")
+                               globalObjects.append("@Field def threeAxisObject = new ThreeAxises(sendEvent, 1, init)\n")
 
                        if (threeAxisObjects == 0) {
                                threeAxisObject0 = metaData['name']
-                               this[threeAxisObject0] = new ThreeAxises({}, 1)
+                               this[threeAxisObject0] = new ThreeAxises({}, 1, true)
                        } else if (threeAxisObjects == 1) {
                                threeAxisObject1 = metaData['name']
-                               this[threeAxisObject1] = new ThreeAxises({}, 1)
+                               this[threeAxisObject1] = new ThreeAxises({}, 1, true)
                        } else if (threeAxisObjects == 2) {
                                threeAxisObject2 = metaData['name']
-                               this[threeAxisObject2] = new ThreeAxises({}, 1)
+                               this[threeAxisObject2] = new ThreeAxises({}, 1, true)
                        }
 
                        threeAxisObjects=threeAxisObjects+1
 
-                       settings.put(metaData['name'], new ThreeAxises({}, 1))
+                       settings.put(metaData['name'], new ThreeAxises({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class three axis!\n")
@@ -763,22 +763,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def doorControlObject = new DoorControls(sendEvent, 1)\n")
+                               globalObjects.append("@Field def doorControlObject = new DoorControls(sendEvent, 1, init)\n")
 
                        if (doorControlObjects == 0) {
                                doorControlObject0 = metaData['name']
-                               this[doorControlObject0] = new DoorControls({}, 1)
+                               this[doorControlObject0] = new DoorControls({}, 1, true)
                        } else if (doorControlObjects == 1) {
                                doorControlObject1 = metaData['name']
-                               this[doorControlObject1] = new DoorControls({}, 1)
+                               this[doorControlObject1] = new DoorControls({}, 1, true)
                        } else if (doorControlObjects == 2) {
                                doorControlObject2 = metaData['name']
-                               this[doorControlObject2] = new DoorControls({}, 1)
+                               this[doorControlObject2] = new DoorControls({}, 1, true)
                        }
 
                        doorControlObjects=doorControlObjects+1
 
-                       settings.put(metaData['name'], new DoorControls({}, 1))
+                       settings.put(metaData['name'], new DoorControls({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class door control!\n")
@@ -798,22 +798,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def energyMeterObject = new EnergyMeters(sendEvent, 1)\n")
+                               globalObjects.append("@Field def energyMeterObject = new EnergyMeters(sendEvent, 1, init)\n")
 
                        if (energyMeterObjects == 0) {
                                energyMeterObject0 = metaData['name']
-                               this[energyMeterObject0] = new EnergyMeters({}, 1)
+                               this[energyMeterObject0] = new EnergyMeters({}, 1, true)
                        } else if (energyMeterObjects == 1) {
                                energyMeterObject1 = metaData['name']
-                               this[energyMeterObject1] = new EnergyMeters({}, 1)
+                               this[energyMeterObject1] = new EnergyMeters({}, 1, true)
                        } else if (energyMeterObjects == 2) {
                                energyMeterObject2 = metaData['name']
-                               this[energyMeterObject2] = new EnergyMeters({}, 1)
+                               this[energyMeterObject2] = new EnergyMeters({}, 1, true)
                        }
 
                        energyMeterObjects=energyMeterObjects+1
 
-                       settings.put(metaData['name'], new EnergyMeters({}, 1))
+                       settings.put(metaData['name'], new EnergyMeters({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class energy meter!\n")
@@ -833,22 +833,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def illuminanceMeasurementObject = new IlluminanceMeasurements(sendEvent, 1)\n")
+                               globalObjects.append("@Field def illuminanceMeasurementObject = new IlluminanceMeasurements(sendEvent, 1, init)\n")
 
                        if (illuminanceMeasurementObjects == 0) {
                                illuminanceMeasurementObject0 = metaData['name']
-                               this[illuminanceMeasurementObject0] = new IlluminanceMeasurements({}, 1)
+                               this[illuminanceMeasurementObject0] = new IlluminanceMeasurements({}, 1, true)
                        } else if (illuminanceMeasurementObjects == 1) {
                                illuminanceMeasurementObject1 = metaData['name']
-                               this[illuminanceMeasurementObject1] = new IlluminanceMeasurements({}, 1)
+                               this[illuminanceMeasurementObject1] = new IlluminanceMeasurements({}, 1, true)
                        } else if (illuminanceMeasurementObjects == 2) {
                                illuminanceMeasurementObject2 = metaData['name']
-                               this[illuminanceMeasurementObject2] = new IlluminanceMeasurements({}, 1)
+                               this[illuminanceMeasurementObject2] = new IlluminanceMeasurements({}, 1, true)
                        }
 
                        illuminanceMeasurementObjects=illuminanceMeasurementObjects+1
 
-                       settings.put(metaData['name'], new IlluminanceMeasurements({}, 1))
+                       settings.put(metaData['name'], new IlluminanceMeasurements({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class illuminance measurement!\n")
@@ -868,22 +868,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def accelerationSensorObject = new AccelerationSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def accelerationSensorObject = new AccelerationSensors(sendEvent, 1, init)\n")
 
                        if (accelerationSensorObjects == 0) {
                                accelerationSensorObject0 = metaData['name']
-                               this[accelerationSensorObject0] = new AccelerationSensors({}, 1)
+                               this[accelerationSensorObject0] = new AccelerationSensors({}, 1, true)
                        } else if (accelerationSensorObjects == 1) {
                                accelerationSensorObject1 = metaData['name']
-                               this[accelerationSensorObject1] = new AccelerationSensors({}, 1)
+                               this[accelerationSensorObject1] = new AccelerationSensors({}, 1, true)
                        } else if (accelerationSensorObjects == 2) {
                                accelerationSensorObject2 = metaData['name']
-                               this[accelerationSensorObject2] = new AccelerationSensors({}, 1)
+                               this[accelerationSensorObject2] = new AccelerationSensors({}, 1, true)
                        }
 
                        accelerationSensorObjects=accelerationSensorObjects+1
 
-                       settings.put(metaData['name'], new AccelerationSensors({}, 1))
+                       settings.put(metaData['name'], new AccelerationSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class Acceleration Sensor!\n")
@@ -903,22 +903,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def motionSensorObject = new MotionSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def motionSensorObject = new MotionSensors(sendEvent, 1, init)\n")
 
                        if (motionSensorObjects == 0) {
                                motionSensorObject0 = metaData['name']
-                               this[motionSensorObject0] = new MotionSensors({}, 1)
+                               this[motionSensorObject0] = new MotionSensors({}, 1, true)
                        } else if (motionSensorObjects == 1) {
                                motionSensorObject1 = metaData['name']
-                               this[motionSensorObject1] = new MotionSensors({}, 1)
+                               this[motionSensorObject1] = new MotionSensors({}, 1, true)
                        } else if (motionSensorObjects == 2) {
                                motionSensorObject2 = metaData['name']
-                               this[motionSensorObject2] = new MotionSensors({}, 1)
+                               this[motionSensorObject2] = new MotionSensors({}, 1, true)
                        }
 
                        motionSensorObjects=motionSensorObjects+1
 
-                       settings.put(metaData['name'], new MotionSensors({}, 1))
+                       settings.put(metaData['name'], new MotionSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class Motion Sensor!\n")
@@ -938,22 +938,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def musicPlayerObject = new MusicPlayers(sendEvent, 1)\n")
+                               globalObjects.append("@Field def musicPlayerObject = new MusicPlayers(sendEvent, 1, init)\n")
 
                        if (musicPlayerObjects == 0) {
                                musicPlayerObject0 = metaData['name']
-                               this[musicPlayerObject0] = new MusicPlayers({}, 1)
+                               this[musicPlayerObject0] = new MusicPlayers({}, 1, true)
                        } else if (musicPlayerObjects == 1) {
                                musicPlayerObject1 = metaData['name']
-                               this[musicPlayerObject1] = new MusicPlayers({}, 1)
+                               this[musicPlayerObject1] = new MusicPlayers({}, 1, true)
                        } else if (musicPlayerObjects == 2) {
                                musicPlayerObject2 = metaData['name']
-                               this[musicPlayerObject2] = new MusicPlayers({}, 1)
+                               this[musicPlayerObject2] = new MusicPlayers({}, 1, true)
                        }
 
                        musicPlayerObjects=musicPlayerObjects+1
 
-                       settings.put(metaData['name'], new MusicPlayers({}, 1)) 
+                       settings.put(metaData['name'], new MusicPlayers({}, 1, true)) 
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class music player!\n")
@@ -973,22 +973,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def powerMeterObject = new PowerMeters(sendEvent, 1)\n")
+                               globalObjects.append("@Field def powerMeterObject = new PowerMeters(sendEvent, 1, init)\n")
 
                        if (powerMeterObjects == 0) {
                                powerMeterObject0 = metaData['name']
-                               this[powerMeterObject0] = new PowerMeters({}, 1)
+                               this[powerMeterObject0] = new PowerMeters({}, 1, true)
                        } else if (powerMeterObjects == 1) {
                                powerMeterObject1 = metaData['name']
-                               this[powerMeterObject1] = new PowerMeters({}, 1)
+                               this[powerMeterObject1] = new PowerMeters({}, 1, true)
                        } else if (powerMeterObjects == 2) {
                                powerMeterObject2 = metaData['name']
-                               this[powerMeterObject2] = new PowerMeters({}, 1)
+                               this[powerMeterObject2] = new PowerMeters({}, 1, true)
                        }
 
                        powerMeterObjects=powerMeterObjects+1
 
-                       settings.put(metaData['name'], new PowerMeters({}, 1))
+                       settings.put(metaData['name'], new PowerMeters({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class power meter!\n")
@@ -1008,22 +1008,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def presenceSensorObject = new PresenceSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def presenceSensorObject = new PresenceSensors(sendEvent, 1, init)\n")
 
                        if (presenceSensorObjects == 0) {
                                presenceSensorObject0 = metaData['name']
-                               this[presenceSensorObject0] = new PresenceSensors({}, 1)
+                               this[presenceSensorObject0] = new PresenceSensors({}, 1, true)
                        } else if (presenceSensorObjects == 1) {
                                presenceSensorObject1 = metaData['name']
-                               this[presenceSensorObject1] = new PresenceSensors({}, 1)
+                               this[presenceSensorObject1] = new PresenceSensors({}, 1, true)
                        } else if (presenceSensorObjects == 2) {
                                presenceSensorObject2 = metaData['name']
-                               this[presenceSensorObject2] = new PresenceSensors({}, 1)
+                               this[presenceSensorObject2] = new PresenceSensors({}, 1, true)
                        }
 
                        presenceSensorObjects=presenceSensorObjects+1
 
-                       settings.put(metaData['name'], new PresenceSensors({}, 1))
+                       settings.put(metaData['name'], new PresenceSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class presence sensor!\n")
@@ -1043,22 +1043,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def humidityMeasurementObject = new RelativeHumidityMeasurements(sendEvent, 1)\n")
+                               globalObjects.append("@Field def humidityMeasurementObject = new RelativeHumidityMeasurements(sendEvent, 1, init)\n")
 
                        if (humidityMeasurementObjects == 0) {
                                humidityMeasurementObject0 = metaData['name']
-                               this[humidityMeasurementObject0] = new RelativeHumidityMeasurements({}, 1)
+                               this[humidityMeasurementObject0] = new RelativeHumidityMeasurements({}, 1, true)
                        } else if (humidityMeasurementObjects == 1) {
                                humidityMeasurementObject1 = metaData['name']
-                               this[humidityMeasurementObject1] = new RelativeHumidityMeasurements({}, 1)
+                               this[humidityMeasurementObject1] = new RelativeHumidityMeasurements({}, 1, true)
                        } else if (humidityMeasurementObjects == 2) {
                                humidityMeasurementObject2 = metaData['name']
-                               this[humidityMeasurementObject2] = new RelativeHumidityMeasurements({}, 1)
+                               this[humidityMeasurementObject2] = new RelativeHumidityMeasurements({}, 1, true)
                        }
 
                        humidityMeasurementObjects=humidityMeasurementObjects+1
 
-                       settings.put(metaData['name'], new RelativeHumidityMeasurements({}, 1))
+                       settings.put(metaData['name'], new RelativeHumidityMeasurements({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class humidity measurement!\n")
@@ -1078,22 +1078,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def relaySwitchObject = new RelaySwitches(sendEvent, 1)\n")
+                               globalObjects.append("@Field def relaySwitchObject = new RelaySwitches(sendEvent, 1, init)\n")
 
                        if (relaySwitchObjects == 0) {
                                relaySwitchObject0 = metaData['name']
-                               this[relaySwitchObject0] = new RelaySwitches({}, 1)
+                               this[relaySwitchObject0] = new RelaySwitches({}, 1, true)
                        } else if (relaySwitchObjects == 1) {
                                relaySwitchObject1 = metaData['name']
-                               this[relaySwitchObject1] = new RelaySwitches({}, 1)
+                               this[relaySwitchObject1] = new RelaySwitches({}, 1, true)
                        } else if (relaySwitchObjects == 2) {
                                relaySwitchObject2 = metaData['name']
-                               this[relaySwitchObject2] = new RelaySwitches({}, 1)
+                               this[relaySwitchObject2] = new RelaySwitches({}, 1, true)
                        }
 
                        relaySwitchObjects=relaySwitchObjects+1
                        
-                       settings.put(metaData['name'], new RelaySwitches({}, 1))
+                       settings.put(metaData['name'], new RelaySwitches({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class relay switch!\n")
@@ -1113,22 +1113,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def sleepSensorObject = new SleepSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def sleepSensorObject = new SleepSensors(sendEvent, 1, init)\n")
 
                        if (sleepSensorObjects == 0) {
                                sleepSensorObject0 = metaData['name']
-                               this[sleepSensorObject0] = new SleepSensors({}, 1)
+                               this[sleepSensorObject0] = new SleepSensors({}, 1, true)
                        } else if (sleepSensorObjects == 1) {
                                sleepSensorObject1 = metaData['name']
-                               this[sleepSensorObject1] = new SleepSensors({}, 1)
+                               this[sleepSensorObject1] = new SleepSensors({}, 1, true)
                        } else if (sleepSensorObjects == 2) {
                                sleepSensorObject2 = metaData['name']
-                               this[sleepSensorObject2] = new SleepSensors({}, 1)
+                               this[sleepSensorObject2] = new SleepSensors({}, 1, true)
                        }
 
                        sleepSensorObjects=sleepSensorObjects+1
                        
-                       settings.put(metaData['name'], new SleepSensors({}, 1))
+                       settings.put(metaData['name'], new SleepSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class sleep sensor!\n")
@@ -1148,22 +1148,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def smokeDetectorObject = new SmokeDetectors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def smokeDetectorObject = new SmokeDetectors(sendEvent, 1, init)\n")
 
                        if (smokeDetectorObjects == 0) {
                                smokeDetectorObject0 = metaData['name']
-                               this[smokeDetectorObject0] = new SmokeDetectors({}, 1)
+                               this[smokeDetectorObject0] = new SmokeDetectors({}, 1, true)
                        } else if (smokeDetectorObjects == 1) {
                                smokeDetectorObject1 = metaData['name']
-                               this[smokeDetectorObject1] = new SmokeDetectors({}, 1)
+                               this[smokeDetectorObject1] = new SmokeDetectors({}, 1, true)
                        } else if (smokeDetectorObjects == 2) {
                                smokeDetectorObject2 = metaData['name']
-                               this[smokeDetectorObject2] = new SmokeDetectors({}, 1)
+                               this[smokeDetectorObject2] = new SmokeDetectors({}, 1, true)
                        }
 
                        smokeDetectorObjects=smokeDetectorObjects+1
                        
-                       settings.put(metaData['name'], new SmokeDetectors({}, 1))
+                       settings.put(metaData['name'], new SmokeDetectors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class smoke detector!\n")
@@ -1183,22 +1183,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def stepSensorObject = new StepSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def stepSensorObject = new StepSensors(sendEvent, 1, init)\n")
 
                        if (stepSensorObjects == 0) {
                                stepSensorObject0 = metaData['name']
-                               this[stepSensorObject0] = new StepSensors({}, 1)
+                               this[stepSensorObject0] = new StepSensors({}, 1, true)
                        } else if (stepSensorObjects == 1) {
                                stepSensorObject1 = metaData['name']
-                               this[stepSensorObject1] = new StepSensors({}, 1)
+                               this[stepSensorObject1] = new StepSensors({}, 1, true)
                        } else if (stepSensorObjects == 2) {
                                stepSensorObject2 = metaData['name']
-                               this[stepSensorObject2] = new StepSensors({}, 1)
+                               this[stepSensorObject2] = new StepSensors({}, 1, true)
                        }
 
                        stepSensorObjects=stepSensorObjects+1
                        
-                       settings.put(metaData['name'], new StepSensors({}, 1))
+                       settings.put(metaData['name'], new StepSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class step sensor!\n")
@@ -1218,22 +1218,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def switchObject = new Switches(sendEvent, 1)\n")
+                               globalObjects.append("@Field def switchObject = new Switches(sendEvent, 1, init)\n")
 
                        if (switchObjects == 0) {
                                switchObject0 = metaData['name']
-                               this[switchObject0] = new Switches({}, 1)
+                               this[switchObject0] = new Switches({}, 1, true)
                        } else if (switchObjects == 1) {
                                switchObject1 = metaData['name']
-                               this[switchObject1] = new Switches({}, 1)
+                               this[switchObject1] = new Switches({}, 1, true)
                        } else if (switchObjects == 2) {
                                switchObject2 = metaData['name']
-                               this[switchObject2] = new Switches({}, 1)
+                               this[switchObject2] = new Switches({}, 1, true)
                        }
 
                        switchObjects=switchObjects+1
                        
-                       settings.put(metaData['name'], new Switches({}, 1))
+                       settings.put(metaData['name'], new Switches({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class switch!\n")
@@ -1253,22 +1253,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def switchLevelObject = new SwitchLevels(sendEvent, 1)\n")
+                               globalObjects.append("@Field def switchLevelObject = new SwitchLevels(sendEvent, 1, init)\n")
 
                        if (switchLevelObjects == 0) {
                                switchLevelObject0 = metaData['name']
-                               this[switchLevelObject0] = new SwitchLevels({}, 1)
+                               this[switchLevelObject0] = new SwitchLevels({}, 1, true)
                        } else if (switchLevelObjects == 1) {
                                switchLevelObject1 = metaData['name']
-                               this[switchLevelObject1] = new SwitchLevels({}, 1)
+                               this[switchLevelObject1] = new SwitchLevels({}, 1, true)
                        } else if (switchLevelObjects == 2) {
                                switchLevelObject2 = metaData['name']
-                               this[switchLevelObject2] = new SwitchLevels({}, 1)
+                               this[switchLevelObject2] = new SwitchLevels({}, 1, true)
                        }
 
                        switchLevelObjects=switchLevelObjects+1
 
-                       settings.put(metaData['name'], new SwitchLevels({}, 1))
+                       settings.put(metaData['name'], new SwitchLevels({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class switch level!\n")
@@ -1288,22 +1288,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def temperatureMeasurementObject = new TemperatureMeasurements(sendEvent, 1)\n")
+                               globalObjects.append("@Field def temperatureMeasurementObject = new TemperatureMeasurements(sendEvent, 1, init)\n")
 
                        if (temperatureMeasurementObjects == 0) {
                                temperatureMeasurementObject0 = metaData['name']
-                               this[temperatureMeasurementObject0] = new TemperatureMeasurements({}, 1)
+                               this[temperatureMeasurementObject0] = new TemperatureMeasurements({}, 1, true)
                        } else if (temperatureMeasurementObjects == 1) {
                                temperatureMeasurementObject1 = metaData['name']
-                               this[temperatureMeasurementObject1] = new TemperatureMeasurements({}, 1)
+                               this[temperatureMeasurementObject1] = new TemperatureMeasurements({}, 1, true)
                        } else if (temperatureMeasurementObjects == 2) {
                                temperatureMeasurementObject2 = metaData['name']
-                               this[temperatureMeasurementObject2] = new TemperatureMeasurements({}, 1)
+                               this[temperatureMeasurementObject2] = new TemperatureMeasurements({}, 1, true)
                        }
 
                        temperatureMeasurementObjects=temperatureMeasurementObjects+1
 
-                       settings.put(metaData['name'], new TemperatureMeasurements({}, 1))
+                       settings.put(metaData['name'], new TemperatureMeasurements({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class temperature measurement!\n")
@@ -1323,22 +1323,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def thermostatObject = new Thermostats(sendEvent, 1)\n")
+                               globalObjects.append("@Field def thermostatObject = new Thermostats(sendEvent, 1, init)\n")
                                
                        if (thermostatObjects == 0) {
                                thermostatObject0 = metaData['name']
-                               this[thermostatObject0] = new Thermostats({}, 1)
+                               this[thermostatObject0] = new Thermostats({}, 1, true)
                        } else if (thermostatObjects == 1) {
                                thermostatObject1 = metaData['name']
-                               this[thermostatObject1] = new Thermostats({}, 1)
+                               this[thermostatObject1] = new Thermostats({}, 1, true)
                        } else if (thermostatObjects == 2) {
                                thermostatObject2 = metaData['name']
-                               this[thermostatObject2] = new Thermostats({}, 1)
+                               this[thermostatObject2] = new Thermostats({}, 1, true)
                        }
 
                        thermostatObjects=thermostatObjects+1
 
-                       settings.put(metaData['name'], new Thermostats({}, 1))
+                       settings.put(metaData['name'], new Thermostats({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class thermostat!\n")
@@ -1358,22 +1358,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def valveObject = new Valves(sendEvent, 1)\n")
+                               globalObjects.append("@Field def valveObject = new Valves(sendEvent, 1, init)\n")
 
                        if (valveObjects == 0) {
                                valveObject0 = metaData['name']
-                               this[valveObject0] = new Valves({}, 1)
+                               this[valveObject0] = new Valves({}, 1, true)
                        } else if (valveObjects == 1) {
                                valveObject1 = metaData['name']
-                               this[valveObject1] = new Valves({}, 1)
+                               this[valveObject1] = new Valves({}, 1, true)
                        } else if (valveObjects == 2) {
                                valveObject2 = metaData['name']
-                               this[valveObject2] = new Valves({}, 1)
+                               this[valveObject2] = new Valves({}, 1, true)
                        }
 
                        valveObjects=valveObjects+1
 
-                       settings.put(metaData['name'], new Valves({}, 1))
+                       settings.put(metaData['name'], new Valves({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class valve!\n")
@@ -1393,22 +1393,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def speechSynthesisObject = new SpeechSynthesises(sendEvent, 1)\n")
+                               globalObjects.append("@Field def speechSynthesisObject = new SpeechSynthesises(sendEvent, 1, init)\n")
 
                        if (speechSynthesisObjects == 0) {
                                speechSynthesisObject0 = metaData['name']
-                               this[speechSynthesisObject0] = new SpeechSynthesises({}, 1)
+                               this[speechSynthesisObject0] = new SpeechSynthesises({}, 1, true)
                        } else if (speechSynthesisObjects == 1) {
                                speechSynthesisObject1 = metaData['name']
-                               this[speechSynthesisObject1] = new SpeechSynthesises({}, 1)
+                               this[speechSynthesisObject1] = new SpeechSynthesises({}, 1, true)
                        } else if (speechSynthesisObjects == 2) {
                                speechSynthesisObject2 = metaData['name']
-                               this[speechSynthesisObject2] = new SpeechSynthesises({}, 1)
+                               this[speechSynthesisObject2] = new SpeechSynthesises({}, 1, true)
                        }
 
                        speechSynthesisObjects=speechSynthesisObjects+1
 
-                       settings.put(metaData['name'], new SpeechSynthesises({}, 1))
+                       settings.put(metaData['name'], new SpeechSynthesises({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class speech synthesis!\n")
@@ -1428,22 +1428,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def waterSensorObject = new WaterSensors(sendEvent, 1)\n")
+                               globalObjects.append("@Field def waterSensorObject = new WaterSensors(sendEvent, 1, init)\n")
 
                        if (waterSensorObjects == 0) {
                                waterSensorObject0 = metaData['name']
-                               this[waterSensorObject0] = new WaterSensors({}, 1)
+                               this[waterSensorObject0] = new WaterSensors({}, 1, true)
                        } else if (waterSensorObjects == 1) {
                                waterSensorObject1 = metaData['name']
-                               this[waterSensorObject1] = new WaterSensors({}, 1)
+                               this[waterSensorObject1] = new WaterSensors({}, 1, true)
                        } else if (waterSensorObjects == 2) {
                                waterSensorObject2 = metaData['name']
-                               this[waterSensorObject2] = new WaterSensors({}, 1)
+                               this[waterSensorObject2] = new WaterSensors({}, 1, true)
                        }
 
                        waterSensorObjects=waterSensorObjects+1
 
-                       settings.put(metaData['name'], new WaterSensors({}, 1))
+                       settings.put(metaData['name'], new WaterSensors({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class water sensor!\n")
@@ -1498,22 +1498,22 @@ def input(LinkedHashMap metaData) {
                        }
 
                        if (contains == 0)
-                               globalObjects.append("@Field def imageCaptureObject = new ImageCaptures(sendEvent, 1)\n")
+                               globalObjects.append("@Field def imageCaptureObject = new ImageCaptures(sendEvent, 1, init)\n")
 
                        if (imageCaptureObjects == 0) {
                                imageCaptureObject0 = metaData['name']
-                               this[imageCaptureObject0] = new ImageCaptures({}, 1)
+                               this[imageCaptureObject0] = new ImageCaptures({}, 1, true)
                        } else if (imageCaptureObjects == 1) {
                                imageCaptureObject1 = metaData['name']
-                               this[imageCaptureObject1] = new ImageCaptures({}, 1)
+                               this[imageCaptureObject1] = new ImageCaptures({}, 1, true)
                        } else if (imageCaptureObjects == 2) {
                                imageCaptureObject2 = metaData['name']
-                               this[imageCaptureObject2] = new ImageCaptures({}, 1)
+                               this[imageCaptureObject2] = new ImageCaptures({}, 1, true)
                        }
 
                        imageCaptureObjects=imageCaptureObjects+1
 
-                       settings.put(metaData['name'], new ImageCaptures({}, 1))
+                       settings.put(metaData['name'], new ImageCaptures({}, 1, true))
 
                        if (App == "App1") {
                                extractedObjectsApp1.append("//Object for class Image Capture!\n")

diff --git a/IlluminanceMeasurement/IlluminanceMeasurements.groovy b/IlluminanceMeasurement/IlluminanceMeasurements.groovy
index 6f7637479a8d54a22796deb1536885d374abcbd0..dbeae2a60b34e7d508969756311e27e3565a11ec 100644 (file)
--- a/IlluminanceMeasurement/IlluminanceMeasurements.groovy
+++ b/IlluminanceMeasurement/IlluminanceMeasurements.groovy
@@ -2,9 +2,6 @@
 package IlluminanceMeasurement
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class IlluminanceMeasurements {
        private int deviceNumbers
        private List illuminanceMeasurements
@@ -18,13 +15,18 @@ public class IlluminanceMeasurements {
        private int currentIlluminance = 50000
 
                
-       IlluminanceMeasurements(Closure sendEvent, int deviceNumbers) {
+       IlluminanceMeasurements(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.illuminanceMeasurements = []
 
-               //def init = Verify.getIntFromList(40000, 50000, 60000)
-               //this.illuminance = init
+               if (init) {
+                       this.illuminance = 50000
+                       this.currentIlluminance = 50000
+               } else {
+                       this.illuminance = 60000
+                       this.currentIlluminance = 60000
+               }
 
                illuminanceMeasurements.add(new IlluminanceMeasurement(id, label, displayName, this.illuminance))
        }

diff --git a/ImageCapture/ImageCaptures.groovy b/ImageCapture/ImageCaptures.groovy
index 95d0812266cba4b02cf32dc1e51e02000cc28605..05880352588f563ef1d425ddd71f4f0a1da5e165 100644 (file)
--- a/ImageCapture/ImageCaptures.groovy
+++ b/ImageCapture/ImageCaptures.groovy
@@ -2,9 +2,6 @@
 package ImageCapture
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class ImageCaptures {
        private int deviceNumbers
        private List imageCaptureSensors
@@ -18,17 +15,16 @@ public class ImageCaptures {
        private String alarmState = "armed"
 
                
-       ImageCaptures(Closure sendEvent, int deviceNumbers) {
+       ImageCaptures(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.imageCaptureSensors = []
 
-               /*def initAlarm = Verify.getBoolean()
-               if (initAlarm) {
+               if (init) {
                        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 8b73dc55ac20e393cd311655c2ddd4f03a2859c9..ad297ab8ed2512c5740582a8fd28324443e5bdff 100644 (file)
--- a/Lock/Locks.groovy
+++ b/Lock/Locks.groovy
@@ -2,9 +2,6 @@
 package Lock
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class Locks{
        int deviceNumbers       
        List locks      
@@ -19,18 +16,19 @@ public class Locks{
        private String currentLock = "locked"
        private String lockLatestValue = "locked"
 
-       Locks(Closure sendEvent, int deviceNumbers) {
+       Locks(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.locks = []
 
-               def init = Verify.getBoolean()
                if (init) {
                        this.lockState = "locked"
+                       this.currentLock = "locked"
                        this.lockLatestValue = "locked"
                } else {
                        this.lockState = "unlocked"
+                       this.currentLock = "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 52034d9521b50b2823b4d40be65c9566cb06ea86..0ae021a9531fc10f5d3255a7ce3e848f9d90a4d3 100644 (file)
--- a/MotionSensor/MotionSensors.groovy
+++ b/MotionSensor/MotionSensors.groovy
@@ -2,9 +2,6 @@
 package MotionSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class MotionSensors {
        private int deviceNumbers
        private List motionSensors
@@ -19,19 +16,20 @@ public class MotionSensors {
        private String motionLatestValue = "inactive"
 
                
-       MotionSensors(Closure sendEvent, int deviceNumbers) {
+       MotionSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.motionSensors = []
 
-               /*def init = Verify.getBoolean()
                if (init) {
                        this.motion = "inactive"
+                       this.currentMotion = "inactive"
                        this.motionLatestValue = "inactive"
                } else {
                        this.motion = "active"
+                       this.currentMotion = "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 e476a8df8595833f760f3ffac44afc7a73abdee6..1906b01edd105090c11ff383c6ea0e254dac713a 100644 (file)
--- a/MusicPlayer/MusicPlayers.groovy
+++ b/MusicPlayer/MusicPlayers.groovy
@@ -2,9 +2,6 @@
 package MusicPlayer
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class MusicPlayers {
        private int deviceNumbers
        private List musicPlayers
@@ -23,41 +20,26 @@ public class MusicPlayers {
 
        
                
-       MusicPlayers(Closure sendEvent, int deviceNumbers) {
+       MusicPlayers(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.deviceNumbers = deviceNumbers
                this.musicPlayers = []
-
-               /*def initLevel = Verify.getIntFromList(10, 20, 30)
-               this.level = initLevel
-               def initMute = Verify.getBoolean()
-               if (initMute) {
+               
+               if (init) {
+                       this.level = 20
                        this.mute = "unmuted"
-               } else {
-                       this.mute = "muted"
-               }
-               def initStatus = Verify.getInt(0,2)
-               if (initStatus == 0) {
                        this.status = "paused"
-               } else if (initStatus == 1) {
-                       this.status = "playing"
-               } else {
-                       this.status = "stopped"
-               }
-               def initTrack = Verify.getIntFromList(1, 2, 3)
-               this.trackNumber = initTrack 
-               def initData = Verify.getBoolean()
-               if (initData) {
+                       this.trackNumber = 1
                        this.trackData = "someTrack"
-               } else {
-                       this.trackData = "someOtherTrack"
-               }
-               def initDesc = Verify.getBoolean()
-               if (initDesc) {
                        this.trackDescription = "someDescriptions"
                } else {
+                       this.level = 30
+                       this.mute = "muted"
+                       this.status = "playing"
+                       this.trackNumber = 2
+                       this.trackData = "someOtherTrack"
                        this.trackDescription = "someOtherDescriptions"
-               }*/
+               }
                musicPlayers.add(new MusicPlayer(sendEvent, id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription))
        }
 

diff --git a/PowerMeter/PowerMeters.groovy b/PowerMeter/PowerMeters.groovy
index 836218299f018ae5026547b9e1f34629535c838f..727da7dc69c1510f287289f0ccb77c2dda61e46c 100644 (file)
--- a/PowerMeter/PowerMeters.groovy
+++ b/PowerMeter/PowerMeters.groovy
@@ -2,9 +2,6 @@
 package PowerMeter
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class PowerMeters {
        private int deviceNumbers
        private List powerMeters
@@ -18,14 +15,18 @@ public class PowerMeters {
        private int currentPower = 50
 
                
-       PowerMeters(Closure sendEvent, int deviceNumbers) {
+       PowerMeters(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.powerMeters = []
 
-               //def init = Verify.getIntFromList(30, 50, 70)
-               //this.power = init
-
+               if (init) {
+                       this.power = 50
+                       this.currentPower = 50
+               } else {
+                       this.power = 60
+                       this.currentPower = 60
+               }
                powerMeters.add(new PowerMeter(id, label, displayName, this.power))
        }
 

diff --git a/PresenceSensor/PresenceSensors.groovy b/PresenceSensor/PresenceSensors.groovy
index 181be404dc46d8f1cf2dbc046e98ef94826e1f74..fd88b33c4ec528e940ab6584e3c90a7a5e8ffadb 100644 (file)
--- a/PresenceSensor/PresenceSensors.groovy
+++ b/PresenceSensor/PresenceSensors.groovy
@@ -2,9 +2,6 @@
 package PresenceSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class PresenceSensors {
        private int deviceNumbers
        private List presenceSensors
@@ -19,19 +16,20 @@ public class PresenceSensors {
        private String presenceLatestValue = "not present"
 
                
-       PresenceSensors(Closure sendEvent, int deviceNumbers) {
+       PresenceSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.presenceSensors = []
-               /*def init = Verify.getBoolean()
+
                if (init) {
                        this.presence = "not present"
+                       this.currentPresence = "not present"
                        this.presenceLatestValue = "not present"
                } else {
                        this.presence = "present"
+                       this.currentPresence = "present"
                        this.presenceLatestValue = "present"
-               }*/
-
+               }
                presenceSensors.add(new PresenceSensor(id, label, displayName, this.presence, this.presenceLatestValue))
        }
 

diff --git a/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy b/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy
index 7bee67627e85557eb190e36908c7c0001747396d..a2cd5cdb422763c4fb93c336d4facf19520d5a82 100644 (file)
--- a/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy
+++ b/RelativeHumidityMeasurement/RelativeHumidityMeasurements.groovy
@@ -2,9 +2,6 @@
 package RelativeHumidityMeasurement
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class RelativeHumidityMeasurements {
        private int deviceNumbers
        private List humidityMeasurements
@@ -18,14 +15,18 @@ public class RelativeHumidityMeasurements {
        private int currentHumidity = 50
 
                
-       RelativeHumidityMeasurements(Closure sendEvent, int deviceNumbers) {
+       RelativeHumidityMeasurements(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.humidityMeasurements = []
 
-               //def init = Verify.getIntFromList(30, 50, 70)
-               //this.humidity = init
-
+               if (init) {
+                       this.humidity = 50
+                       this.currentHumidity = 50
+               } else {
+                       this.humidity = 60
+                       this.currentHumidity = 60
+               }
                humidityMeasurements.add(new RelativeHumidityMeasurement(id, label, displayName, this.humidity))
        }
 

diff --git a/RelaySwitch/RelaySwitches.groovy b/RelaySwitch/RelaySwitches.groovy
index e7b6e0080bd68b95e0d4a67f3cb214165e9076d0..fb5977b69dbb704303182e410ccc3e1456c5689e 100644 (file)
--- a/RelaySwitch/RelaySwitches.groovy
+++ b/RelaySwitch/RelaySwitches.groovy
@@ -2,9 +2,6 @@
 package RelaySwitch
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class RelaySwitches {
        int deviceNumbers       
        List relaySwitches
@@ -19,13 +16,12 @@ public class RelaySwitches {
        private String currentSwitch = "off"
        private String switchLatestValue = "off"
 
-       RelaySwitches(Closure sendEvent, int deviceNumbers) {
+       RelaySwitches(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.relaySwitches = []
 
-               /*def init = Verify.getBoolean()
                if (init) {
                        this.switchState = "off"
                        this.currentSwitch = "off"
@@ -34,7 +30,7 @@ public class RelaySwitches {
                        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/Runner.py b/Runner.py
index 087dd3e569432a92664675658aa9870886028c51..0c0492eeca8d105a1e2ccedc264be0e996396b9a 100644 (file)
--- a/Runner.py
+++ b/Runner.py
@@ -129,6 +129,7 @@ for line in eventHandler:
        Out.write(line)
 Out.write("\n")
 Out.write("//GlobalVariables for both Apps\n")
+Out.write("@Field def init = Verify.getBoolean()\n\n")
 for line in GlobalVariablesBothApps:
        Out.write(line)
 Out.write("\n")

diff --git a/SleepSensor/SleepSensors.groovy b/SleepSensor/SleepSensors.groovy
index fc26621c1f1d586a8d2632987ef05b75c7b849dc..0db103302ed0869fbc2c8170ec124d9b34645f4a 100644 (file)
--- a/SleepSensor/SleepSensors.groovy
+++ b/SleepSensor/SleepSensors.groovy
@@ -2,9 +2,6 @@
 package SleepSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class SleepSensors {
        private int deviceNumbers
        private List sleepSensors
@@ -17,17 +14,16 @@ public class SleepSensors {
        private String sleeping = "sleeping"
 
                
-       SleepSensors(Closure sendEvent, int deviceNumbers) {
+       SleepSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                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/SmokeDetector/SmokeDetectors.groovy b/SmokeDetector/SmokeDetectors.groovy
index 2c09a20b43326b9a933dacf4634601733bd742f3..d2c61291ae4e0a3b023af747fd68886f302d2710 100644 (file)
--- a/SmokeDetector/SmokeDetectors.groovy
+++ b/SmokeDetector/SmokeDetectors.groovy
@@ -2,9 +2,6 @@
 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,39 +18,34 @@ public class SmokeDetectors {
        private String currentCarbonMonoxideValue = "clear"
        private String carbonMonoxideLatestValue = "clear"
        private int battery = 50
-        private int batteryValue = 50
+    private int batteryValue = 50
        private int batteryLatestValue = 50
 
                
-       SmokeDetectors(Closure sendEvent, int deviceNumbers) {
+       SmokeDetectors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.smokeDetectors = []
 
-               /*def init = Verify.getInt(0,2)
-               if (init == 0) {
+               if (init) {
                        this.currentSmokeValue = "clear"
                        this.smokeLatestValue = "clear"
-               } else if (initSmoke == 1) {
-                       this.currentSmokeValue = "detected"
-                       this.smokeLatestValue = "detected"
-               } else {
-                       this.currentSmokeValue = "tested"
-                       this.smokeLatestValue = "tested"                
-               }
-
-               def initCarbonMonoxide = Verify.getInt(0,2)
-               if (initCarbonMonoxide == 0) {
+                       this.carbonMonoxide = "clear"
                        this.currentCarbonMonoxideValue = "clear"
                        this.carbonMonoxideLatestValue = "clear"
-               } else if (initCarbonMonoxide == 1) {
+                       this.battery = 50
+                       this.batteryValue = 50
+                       this.batteryLatestValue = 50
+               } else {
+                       this.currentSmokeValue = "detected"
+                       this.smokeLatestValue = "detected"
+                       this.carbonMonoxide = "detected"
                        this.currentCarbonMonoxideValue = "detected"
                        this.carbonMonoxideLatestValue = "detected"
-               } else {
-                       this.currentCarbonMonoxideValue = "tested"
-                       this.carbonMonoxideLatestValue = "tested"               
+                       this.battery = 60
+                       this.batteryValue = 60
+                       this.batteryLatestValue = 60
                }
-               }*/
                smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue, this.carbonMonoxide, this.carbonMonoxideLatestValue, this.battery))
        }
 

diff --git a/SpeechSynthesis/SpeechSynthesises.groovy b/SpeechSynthesis/SpeechSynthesises.groovy
index 2a125987d1806787f72821694a14bda378ab40fd..50417cc8615a278a5bb8fce4f87ce69122c29b9b 100644 (file)
--- a/SpeechSynthesis/SpeechSynthesises.groovy
+++ b/SpeechSynthesis/SpeechSynthesises.groovy
@@ -2,9 +2,6 @@
 package SpeechSynthesis
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class SpeechSynthesises {
        private int deviceNumbers
        private List speechSynthesises
@@ -17,14 +14,16 @@ public class SpeechSynthesises {
        private int level = 50
 
                
-       SpeechSynthesises(Closure sendEvent, int deviceNumbers) {
+       SpeechSynthesises(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.speechSynthesises = []
 
-               //def init = Verify.getIntFromList(30, 50, 70)
-               //this.level = init
-
+               if (init) {
+                       this.level = 50
+               } else {
+                       this.level = 60
+               }
                speechSynthesises.add(new SpeechSynthesis(id, label, displayName, this.level))
        }
 

diff --git a/StepSensor/StepSensors.groovy b/StepSensor/StepSensors.groovy
index fbfe70ff48fabd34813d64d2ee59e92af1b9097c..d3edb7b4f6f9fc035374e54317c3fb5788dbac27 100644 (file)
--- a/StepSensor/StepSensors.groovy
+++ b/StepSensor/StepSensors.groovy
@@ -2,9 +2,6 @@
 package StepSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class StepSensors {
        private int deviceNumbers
        private List stepSensors
@@ -18,16 +15,18 @@ public class StepSensors {
        private int steps = 0
 
                
-       StepSensors(Closure sendEvent, int deviceNumbers) {
+       StepSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                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*/
-
+               if (init) {
+                       this.goal = 50
+                       this.steps = 0
+               } else {
+                       this.goal = 60
+                       this.steps = 1
+               }
                stepSensors.add(new StepSensor(id, label, displayName, this.steps, this.goal))
        }
 

diff --git a/Switch/Switches.groovy b/Switch/Switches.groovy
index a13030a7d71a216344c9edb2fa50677d4189c5fd..e6ac8646571f6c4580146f0cb8a2fb08f22339d1 100644 (file)
--- a/Switch/Switches.groovy
+++ b/Switch/Switches.groovy
@@ -2,9 +2,6 @@
 package Switch
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class Switches {
        int deviceNumbers       
        List switches
@@ -20,25 +17,23 @@ public class Switches {
        private int currentLevel = 50
        private String switchLatestValue = "off"
 
-       Switches(Closure sendEvent, int deviceNumbers) {
+       Switches(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                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) {
+               if (init) {
                        this.switchState = "off"
                        this.currentSwitch = "off"
                        this.switchLatestValue = "off"
+                       this.currentLevel = 50
                } else {
                        this.switchState = "on"
                        this.currentSwitch = "on"
                        this.switchLatestValue = "on"
-               }*/
-
+                       this.currentLevel = 60
+               }
                switches.add(new Switch(sendEvent, id, label, displayName, this.switchState, this.currentSwitch, this.currentLevel, this.switchLatestValue))
        }
 

diff --git a/SwitchLevel/SwitchLevels.groovy b/SwitchLevel/SwitchLevels.groovy
index 09bf7a6f163c480949b40dc5b5a48681f168a625..5d02053b334ebdea6aaaf85cc78608b8866e0dc8 100644 (file)
--- a/SwitchLevel/SwitchLevels.groovy
+++ b/SwitchLevel/SwitchLevels.groovy
@@ -2,9 +2,6 @@
 package SwitchLevel
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class SwitchLevels {
        int deviceNumbers       
        List switchLevels
@@ -23,24 +20,29 @@ public class SwitchLevels {
        private String currentSwitch = "on"
        private String switchLatestValue = "on"
 
-       SwitchLevels(Closure sendEvent, int deviceNumbers) {
+       SwitchLevels(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.switchLevels = []
 
-               /*def initLevel = Verify.getIntFromList(30, 50, 70)
-               this.level = initLevel
-               def init = Verify.getBoolean()
                if (init) {
+                       this.level = 50
+                       this.rate = 50
+                       this.hue = 30
+                       this.saturation = 70
                        this.switchState = "off"
                        this.currentSwitch = "off"
                        this.switchLatestValue = "off"
                } else {
+                       this.level = 60
+                       this.rate = 60
+                       this.hue = 50
+                       this.saturation = 90
                        this.switchState = "on"
                        this.currentSwitch = "on"
                        this.switchLatestValue = "on"
-               }*/
+               }
                switchLevels.add(new SwitchLevel(sendEvent, id, label, displayName, this.level, this.hue, this.saturation, this.switchState, this.switchLatestValue))
        }
 

diff --git a/TemperatureMeasurement/TemperatureMeasurements.groovy b/TemperatureMeasurement/TemperatureMeasurements.groovy
index 31ba842155c964f2da0b8140c6ffe03863ba9924..1f6d932e2ddb569c97d26b3d9ffe569482d58641 100644 (file)
--- a/TemperatureMeasurement/TemperatureMeasurements.groovy
+++ b/TemperatureMeasurement/TemperatureMeasurements.groovy
@@ -2,9 +2,6 @@
 package TemperatureMeasurement
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class TemperatureMeasurements {
        private int deviceNumbers
        private List temperatureMeasurements
@@ -17,14 +14,18 @@ public class TemperatureMeasurements {
        private int temperature = 50
        private int currentTemperature = 50
 
-       TemperatureMeasurements(Closure sendEvent, int deviceNumbers) {
+       TemperatureMeasurements(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.temperatureMeasurements = []
 
-               //def initTemp = Verify.getIntFromList(30, 50, 70)
-               //this.temperature = initTemp
-       
+               if (init) {
+                       this.temperature = 50
+                       this.currentTemperature = 50
+               } else {
+                       this.temperature = 60
+                       this.currentTemperature = 60
+               }       
                temperatureMeasurements.add(new TemperatureMeasurement(id, label, displayName, this.temperature))
        }
 

diff --git a/Thermostat/Thermostats.groovy b/Thermostat/Thermostats.groovy
index 59d6bcae99c3ebf95208d97f16c974aabda5538a..acbb23ee1975d501e3cb613799d24edcac239973 100644 (file)
--- a/Thermostat/Thermostats.groovy
+++ b/Thermostat/Thermostats.groovy
@@ -2,9 +2,6 @@
 package Thermostat
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class Thermostats{
        int deviceNumbers       
        List thermostats        
@@ -40,68 +37,39 @@ public class Thermostats{
        private int latestHeatingSetPoint = 50
 
 
-       Thermostats(Closure sendEvent, int deviceNumbers) {
+       Thermostats(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.thermostats = []
 
-               def initTemperature = Verify.getIntFromList(60, 66)
-               this.temperature = initTemperature
-               this.currentTemperature = initTemperature
-               
-               def initCoolingSetpoint = Verify.getIntFromList(70, 80)
-               this.currentCoolingSetpoint = initCoolingSetpoint
-               this.coolingSetpoint = initCoolingSetpoint
-               
-               def initHeatingSetpoint = Verify.getIntFromList(35, 50)
-               this.currentHeatingSetpoint = initHeatingSetpoint
-               this.heatingSetpoint = initHeatingSetpoint
-               
-               def initThermostatSetpoint = Verify.getIntFromList(50, 60)
-               this.thermostatSetpoint = initThermostatSetpoint
-               
-               def initFanMode = Verify.getInt(0,4)
-               if (initFanMode == 0) {
+               if (init) {
+                       this.temperature = 60
+                       this.currentTemperature = 60
+                       this.currentCoolingSetpoint = 70
+                       this.coolingSetpoint = 70
+                       this.currentHeatingSetpoint = 35
+                       this.heatingSetpoint = 35
+                       this.thermostatSetpoint = 50
                        this.thermostatFanMode = "auto"
                        this.thermostatLatestFanMode = "auto"
-               } else if (initFanMode == 1) {
-                       this.thermostatFanMode = "fanCirculate"
-                       this.thermostatLatestFanMode = "fanCirculate"
-               } else if (initFanMode == 2) {
-                       this.thermostatFanMode = "circulate"
-                       this.thermostatLatestFanMode = "circulate"
-               } else if (initFanMode == 3) {
-                       this.thermostatFanMode = "fanOn"
-                       this.thermostatLatestFanMode = "fanOn"
-               } else {
-                       this.thermostatFanMode = "on"
-                       this.thermostatLatestFanMode = "on"
-               }
-
-               def initMode = Verify.getInt(0,4)
-               if (initMode == 0) {
                        this.thermostatMode = "auto"
                        this.currentThermostatMode = "auto"
                        this.thermostatLatestMode = "auto"
-               } else if (initMode == 1) {
-                       this.thermostatMode = "cool"
-                       this.currentThermostatMode = "cool"
-                       this.thermostatLatestMode = "cool"
-               } else if (initMode == 2) {
-                       this.thermostatMode = "emergencyHeat"
-                       this.currentThermostatMode = "emergencyHeat"
-                       this.thermostatLatestMode = "emergencyHeat"
-               } else if (initMode == 3) {
-                       this.thermostatMode = "heat"
-                       this.currentThermostatMode = "heat"
-                       this.thermostatLatestMode = "heat"
                } else {
+                       this.temperature = 66
+                       this.currentTemperature = 66
+                       this.currentCoolingSetpoint = 80
+                       this.coolingSetpoint = 80
+                       this.currentHeatingSetpoint = 50
+                       this.heatingSetpoint = 50
+                       this.thermostatSetpoint = 60
+                       this.thermostatFanMode = "circulate"
+                       this.thermostatLatestFanMode = "circulate"
                        this.thermostatMode = "off"
                        this.currentThermostatMode = "off"
-                       this.thermostatLatestMode = "off"
+                       this.thermostatLatestMode = "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,

diff --git a/ThreeAxis/ThreeAxises.groovy b/ThreeAxis/ThreeAxises.groovy
index 6dd02b20cfc584e56d6d061a2121573c8aa517d2..e9c027e5a9a4834d4c9bef865c10945780f745b8 100644 (file)
--- a/ThreeAxis/ThreeAxises.groovy
+++ b/ThreeAxis/ThreeAxises.groovy
@@ -2,9 +2,6 @@
 package ThreeAxis
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class ThreeAxises {
        private int deviceNumbers
        private List threeAxises
@@ -17,11 +14,16 @@ public class ThreeAxises {
        private LinkedHashMap threeAxis = [x:0, y:0, z:0]
        
                
-       ThreeAxises(Closure sendEvent, int deviceNumbers) {
+       ThreeAxises(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.threeAxises = []
-
+               
+               if (init) {
+                       this.threeAxis = [x:0, y:0, z:0]
+               } else {
+                       this.threeAxis = [x:1, y:2, z:3]
+               }
                threeAxises.add(new ThreeAxis(id, label, displayName, threeAxis))
        }
 

diff --git a/Valve/Valves.groovy b/Valve/Valves.groovy
index 0bf0bbce18669e7b7f7489028ff0fe949417bb04..dda58adf7c943f65ff0096440e5893d9c2aead4f 100644 (file)
--- a/Valve/Valves.groovy
+++ b/Valve/Valves.groovy
@@ -2,9 +2,6 @@
 package Valve
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class Valves {
        int deviceNumbers       
        List valves
@@ -18,20 +15,19 @@ public class Valves {
        private String valve = "closed"
        private String valveLatestValue = "closed"
 
-       Valves(Closure sendEvent, int deviceNumbers) {
+       Valves(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent
                this.timers = new SimulatedTimer()
                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 bb8aac0ce22c906faf3cfc593c01765ee6d54a50..10567ae1c822f933c48f2feefe8e165dceef55ee 100644 (file)
--- a/WaterSensor/WaterSensors.groovy
+++ b/WaterSensor/WaterSensors.groovy
@@ -2,9 +2,6 @@
 package WaterSensor
 import Timer.SimulatedTimer
 
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
 public class WaterSensors {
        private int deviceNumbers
        private List waterSensors
@@ -17,17 +14,16 @@ public class WaterSensors {
        private String water = "dry"
 
                
-       WaterSensors(Closure sendEvent, int deviceNumbers) {
+       WaterSensors(Closure sendEvent, int deviceNumbers, boolean init) {
                this.sendEvent = sendEvent              
                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))
        }