Adding path explorations for initializations.

diff --git a/AccelerationSensor/AccelerationSensors.groovy b/AccelerationSensor/AccelerationSensors.groovy
index 0d3c14f84f607d41b00ac83debd27893bf49857c..8c1992cd4065996444a755ce629826dbc1a2ca02 100644 (file)
--- a/AccelerationSensor/AccelerationSensors.groovy
+++ b/AccelerationSensor/AccelerationSensors.groovy
@@ -2,6 +2,9 @@
 package AccelerationSensor
 import Timer.SimulatedTimer
 
 package AccelerationSensor
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class AccelerationSensors {
        private int deviceNumbers
        private List accelerationSensors
 public class AccelerationSensors {
        private int deviceNumbers
        private List accelerationSensors


@@ -21,6 +24,14 @@ public class AccelerationSensors {
                this.deviceNumbers = deviceNumbers
                this.accelerationSensors = []
 
                this.deviceNumbers = deviceNumbers
                this.accelerationSensors = []
 

+               def init = Verify.getBoolean()
+               if (init) {
+                       this.acceleration = "inactive"
+                       this.accelerationLatestValue = "inactive"
+               } else {
+                       this.acceleration = "active"
+                       this.accelerationLatestValue = "active"
+               }

                accelerationSensors.add(new AccelerationSensor(id, label, displayName, this.acceleration, this.accelerationLatestValue))
        }
 
                accelerationSensors.add(new AccelerationSensor(id, label, displayName, this.acceleration, this.accelerationLatestValue))
        }
 

diff --git a/Alarm/Alarms.groovy b/Alarm/Alarms.groovy
index 2eb775e253434122396de4f3d19ca3da336121b1..b2759bde5235e87bce5129cfa5264ecd0443916d 100644 (file)
--- a/Alarm/Alarms.groovy
+++ b/Alarm/Alarms.groovy
@@ -2,6 +2,9 @@
 package Alarm
 import Timer.SimulatedTimer
 
 package Alarm
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class Alarms {
        int deviceNumbers       
        List alarms
 public class Alarms {
        int deviceNumbers       
        List alarms


@@ -22,6 +25,16 @@ public class Alarms {
                this.deviceNumbers = deviceNumbers
                this.alarms = []
 
                this.deviceNumbers = deviceNumbers
                this.alarms = []
 

+               def init = Verify.getBoolean()
+               if (init) {
+                       this.alarm = "off"
+                       this.currentAlarm = "off"
+                       this.alarmLatestValue = "off"
+               } else {
+                       this.alarm = "on"
+                       this.currentAlarm = "on"
+                       this.alarmLatestValue = "on"
+               }

                alarms.add(new Alarm(sendEvent, id, label, displayName, this.alarm, this.currentAlarm, this.alarmLatestValue))
        }
                
                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 ce4a187d3a4b06040fc940f902b73b39b6805fa6..6e40e12f672508a254a0cb22fc0b90ebcc9162ce 100644 (file)
--- a/Battery/Batteries.groovy
+++ b/Battery/Batteries.groovy
@@ -2,6 +2,9 @@
 package Battery
 import Timer.SimulatedTimer
 
 package Battery
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class Batteries {
        private int deviceNumbers
        private List batteries
 public class Batteries {
        private int deviceNumbers
        private List batteries


@@ -19,6 +22,9 @@ public class Batteries {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.batteries = []
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.batteries = []

+               
+               def init = Verify.getIntFromList(30, 50, 70)
+               this.battery = init

 
                batteries.add(new Battery(id, label, displayName, this.battery))
        }
 
                batteries.add(new Battery(id, label, displayName, this.battery))
        }

diff --git a/BeaconSensor/BeaconSensors.groovy b/BeaconSensor/BeaconSensors.groovy
index 24bcfc8dfa3e6c57b3de0afced91b174442ded63..33dd1fe65d39c1bed0a933ef177a7f36029eaee0 100644 (file)
--- a/BeaconSensor/BeaconSensors.groovy
+++ b/BeaconSensor/BeaconSensors.groovy
@@ -2,6 +2,9 @@
 package BeaconSensor
 import Timer.SimulatedTimer
 
 package BeaconSensor
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class BeaconSensors {
        private int deviceNumbers
        private List beaconSensors
 public class BeaconSensors {
        private int deviceNumbers
        private List beaconSensors


@@ -21,6 +24,14 @@ public class BeaconSensors {
                this.deviceNumbers = deviceNumbers
                this.beaconSensors = []
 
                this.deviceNumbers = deviceNumbers
                this.beaconSensors = []
 

+               def init = Verify.getBoolean()
+               if (init) {
+                       this.presence = "not present"
+                       this.presenceLatestValue = "not present"
+               } else {
+                       this.presence = "present"
+                       this.presenceLatestValue = "present"
+               }

                beaconSensors.add(new BeaconSensor(id, label, displayName, this.presence, this.presenceLatestValue))
        }
 
                beaconSensors.add(new BeaconSensor(id, label, displayName, this.presence, this.presenceLatestValue))
        }
 

diff --git a/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy b/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy
index 7e848e3afb66c93c1312c6d2651098f8da72ff7c..511d0312f542c998b03753a4afdbbd0aed153476 100644 (file)
--- a/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy
+++ b/CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy
@@ -2,6 +2,9 @@
 package CarbonMonoxideDetector
 import Timer.SimulatedTimer
 
 package CarbonMonoxideDetector
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class CarbonMonoxideDetectors {
        private int deviceNumbers
        private List carbonMonoxideDetectors
 public class CarbonMonoxideDetectors {
        private int deviceNumbers
        private List carbonMonoxideDetectors


@@ -20,8 +23,19 @@ public class CarbonMonoxideDetectors {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.carbonMonoxideDetectors = []
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.carbonMonoxideDetectors = []

-
-               carbonMonoxideDetectors.add(new CarbonMonoxideDetector(id, label, displayName, this.currentCarbonMonoxideValue, this.carbonMonoxideLatestValue))
+               
+               def init = Verify.getInt(0,2)
+               if (init == 0) {
+                       this.carbonMonoxide = "clear"
+                       this.carbonMonoxideLatestValue = "clear"
+               } else if (init == 1) {
+                       this.carbonMonoxide = "detected"
+                       this.carbonMonoxideLatestValue = "detected"
+               } else {
+                       this.carbonMonoxide = "tested"
+                       this.carbonMonoxideLatestValue = "tested"               
+               }
+               carbonMonoxideDetectors.add(new CarbonMonoxideDetector(id, label, displayName, this.carbonMonoxide, this.carbonMonoxideLatestValue))

        }
 
        //By Model Checker
        }
 
        //By Model Checker

diff --git a/ColorControl/ColorControls.groovy b/ColorControl/ColorControls.groovy
index b3a6471926b18f34043c81a7353b6b470400070f..6eb5ac65f9f26a3e597cc07c72c7e9d86c9b86d1 100644 (file)
--- a/ColorControl/ColorControls.groovy
+++ b/ColorControl/ColorControls.groovy
@@ -2,6 +2,8 @@
 package ColorControl
 import Timer.SimulatedTimer
 
 package ColorControl
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify

 
 public class ColorControls {
        private int deviceNumbers
 
 public class ColorControls {
        private int deviceNumbers


@@ -21,6 +23,19 @@ public class ColorControls {
                this.sendEvent = sendEvent
                this.deviceNumbers = deviceNumbers
                this.colorControls = []
                this.sendEvent = sendEvent
                this.deviceNumbers = deviceNumbers
                this.colorControls = []

+               
+               def initHue = Verify.getIntFromList(30, 50, 70)
+               this.hue = initHue
+               def initSat = Verify.getIntFromList(40, 50, 60)
+               this.saturation = initSat
+               def init = Verify.getInt(0,2)
+               if (init == 0) {
+                       this.color = "red"
+               } else if (init == 1) {
+                       this.color = "green"
+               } else {
+                       this.color = "blue"
+               }

 
                colorControls.add(new ColorControl(id, label, displayName, this.color, this.hue, this.saturation))
        }
 
                colorControls.add(new ColorControl(id, label, displayName, this.color, this.hue, this.saturation))
        }

diff --git a/ContactSensor/ContactSensors.groovy b/ContactSensor/ContactSensors.groovy
index 1de8c76dccd1ec2a90c08319dbf11236ba12333c..489200dbf0a43907d3556cef56f50c528d7a5834 100644 (file)
--- a/ContactSensor/ContactSensors.groovy
+++ b/ContactSensor/ContactSensors.groovy
@@ -2,6 +2,9 @@
 package ContactSensor
 import Timer.SimulatedTimer
 
 package ContactSensor
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class ContactSensors {
        private int deviceNumbers
        private List contacts
 public class ContactSensors {
        private int deviceNumbers
        private List contacts


@@ -22,6 +25,23 @@ public class ContactSensors {
                this.deviceNumbers = deviceNumbers
                this.contacts = []
 
                this.deviceNumbers = deviceNumbers
                this.contacts = []
 

+               def initSensor = Verify.getBoolean()
+               if (initSensor) {
+                       this.contactState = "closed"
+                       this.currentContact = "closed"
+                       this.latestValue = "closed"
+               } else {
+                       this.contactState = "open"
+                       this.currentContact = "open"
+                       this.latestValue = "open"
+               }
+
+               def initAlarm = Verify.getBoolean()
+               if (initAlarm) {
+                       this.alarmState = "armed"
+               } else {
+                       this.alarmState = "not armed"
+               }

                contacts.add(new ContactSensor(id, label, displayName, this.contactState, this.currentContact, this.alarmState, this.latestValue))
        }
 
                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 921089977d70655e594c2363ba63bf9cc519dc21..444154da8319bd8a20615aaf75e59e02c4d15137 100644 (file)
--- a/DoorControl/DoorControls.groovy
+++ b/DoorControl/DoorControls.groovy
@@ -2,6 +2,9 @@
 package DoorControl
 import Timer.SimulatedTimer
 
 package DoorControl
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class DoorControls {
        int deviceNumbers       
        List doorControls
 public class DoorControls {
        int deviceNumbers       
        List doorControls


@@ -20,7 +23,15 @@ public class DoorControls {
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.doorControls = []
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.doorControls = []

-               
+
+               def init = Verify.getBoolean()
+               if (init) {
+                       this.doorState = "closed"
+                       this.doorLatestValue = "closed"
+               } else {
+                       this.doorState = "open"
+                       this.doorLatestValue = "open"
+               }

                doorControls.add(new DoorControl(sendEvent, id, label, displayName, this.doorState, this.doorLatestValue))
        }
 
                doorControls.add(new DoorControl(sendEvent, id, label, displayName, this.doorState, this.doorLatestValue))
        }
 

diff --git a/EnergyMeter/EnergyMeters.groovy b/EnergyMeter/EnergyMeters.groovy
index caec87591a4e041efd6f47cd1aa5f6bfdf155157..59670840b327d7dfd8d8a9f8e993d3d6abbe64e5 100644 (file)
--- a/EnergyMeter/EnergyMeters.groovy
+++ b/EnergyMeter/EnergyMeters.groovy
@@ -18,7 +18,10 @@ public class EnergyMeters {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.energyMeters = []
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.energyMeters = []

-
+               
+               def init = Verify.getIntFromList(30, 50, 70)
+               this.energy = init
+               

                energyMeters.add(new EnergyMeter(id, label, displayName, this.energy))
        }
 
                energyMeters.add(new EnergyMeter(id, label, displayName, this.energy))
        }
 

diff --git a/ImageCapture/ImageCaptures.groovy b/ImageCapture/ImageCaptures.groovy
index 2a63a3e8fa806a31611a8b649496870cdfaa3229..9e5bd9ab09d5574e297560db551e06f0af47df9d 100644 (file)
--- a/ImageCapture/ImageCaptures.groovy
+++ b/ImageCapture/ImageCaptures.groovy
@@ -20,6 +20,12 @@ public class ImageCaptures {
                this.deviceNumbers = deviceNumbers
                this.imageCaptureSensors = []
 
                this.deviceNumbers = deviceNumbers
                this.imageCaptureSensors = []
 

+               def initAlarm = Verify.getBoolean()
+               if (initAlarm) {
+                       this.alarmState = "armed"
+               } else {
+                       this.alarmState = "not armed"
+               }

                imageCaptureSensors.add(new ImageCapture(id, label, displayName, this.image, this.alarmState))
        }
 
                imageCaptureSensors.add(new ImageCapture(id, label, displayName, this.image, this.alarmState))
        }
 

diff --git a/Lock/Locks.groovy b/Lock/Locks.groovy
index f792c6ccfda41d3f5d36d8ec77ae1436ffc85a7d..f2b9d75fdf688071f50198b3727e1104d3f4409a 100644 (file)
--- a/Lock/Locks.groovy
+++ b/Lock/Locks.groovy
@@ -2,6 +2,9 @@
 package Lock
 import Timer.SimulatedTimer
 
 package Lock
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class Locks{
        int deviceNumbers       
        List locks      
 public class Locks{
        int deviceNumbers       
        List locks      


@@ -22,6 +25,14 @@ public class Locks{
                this.deviceNumbers = deviceNumbers
                this.locks = []
 
                this.deviceNumbers = deviceNumbers
                this.locks = []
 

+               def init = Verify.getBoolean()
+               if (init) {
+                       this.lockState = "locked"
+                       this.lockLatestValue = "locked"
+               } else {
+                       this.lockState = "unlocked"
+                       this.lockLatestValue = "unlocked"
+               }

                locks.add(new Lock(sendEvent,id, label, displayName, this.lockState, this.lockLatestValue))
        }
 
                locks.add(new Lock(sendEvent,id, label, displayName, this.lockState, this.lockLatestValue))
        }
 

diff --git a/MotionSensor/MotionSensors.groovy b/MotionSensor/MotionSensors.groovy
index 863903c5017090867a58f7ca2b3e5bf676986e59..85167131551b73f787be48e6525bb806a5e2db8c 100644 (file)
--- a/MotionSensor/MotionSensors.groovy
+++ b/MotionSensor/MotionSensors.groovy
@@ -2,6 +2,9 @@
 package MotionSensor
 import Timer.SimulatedTimer
 
 package MotionSensor
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class MotionSensors {
        private int deviceNumbers
        private List motionSensors
 public class MotionSensors {
        private int deviceNumbers
        private List motionSensors


@@ -21,6 +24,14 @@ public class MotionSensors {
                this.deviceNumbers = deviceNumbers
                this.motionSensors = []
 
                this.deviceNumbers = deviceNumbers
                this.motionSensors = []
 

+               def init = Verify.getBoolean()
+               if (init) {
+                       this.motion = "inactive"
+                       this.motionLatestValue = "inactive"
+               } else {
+                       this.motion = "active"
+                       this.motionLatestValue = "active"
+               }

                motionSensors.add(new MotionSensor(id, label, displayName, this.motion, this.motionLatestValue))
        }
 
                motionSensors.add(new MotionSensor(id, label, displayName, this.motion, this.motionLatestValue))
        }
 

diff --git a/MusicPlayer/MusicPlayers.groovy b/MusicPlayer/MusicPlayers.groovy
index bf733db3a93bc327219d4f273b507eaf708cc6bd..847dd1cd86cc65666177668766bdeddef05ae32d 100644 (file)
--- a/MusicPlayer/MusicPlayers.groovy
+++ b/MusicPlayer/MusicPlayers.groovy
@@ -2,6 +2,8 @@
 package MusicPlayer
 import Timer.SimulatedTimer
 
 package MusicPlayer
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify

 
 public class MusicPlayers {
        private int deviceNumbers
 
 public class MusicPlayers {
        private int deviceNumbers


@@ -25,6 +27,35 @@ public class MusicPlayers {
                this.sendEvent = sendEvent
                this.deviceNumbers = deviceNumbers
                this.musicPlayers = []
                this.sendEvent = sendEvent
                this.deviceNumbers = deviceNumbers
                this.musicPlayers = []

+               
+               def initLevel = Verify.getIntFromList(10, 20, 30)
+               this.level = initLevel
+               def initTrack = Verify.getIntFromList(1, 2, 3)
+               this.trackNumber = initTrack
+               def initMute = Verify.getBoolean()
+               if (initMute) {
+                       this.mute = "unmuted"
+               } else {
+                       this.mute = "mute"
+               }
+               def initStatus = Verify.getBoolean()
+               if (initStatus) {
+                       this.status = "pause"
+               } else {
+                       this.status = "play"
+               }
+               def initTrackData = Verify.getBoolean()
+               if (initTrackData) {
+                       this.trackData = "someTrack"
+               } else {
+                       this.trackData = "someOtherTrack"
+               }
+               def initTrackDesc = Verify.getBoolean()
+               if (initTrackDesc) {
+                       this.trackDescription = "someDescriptions"
+               } else {
+                       this.trackDescription = "someOtherDescriptions"
+               }

 
                musicPlayers.add(new MusicPlayer(id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription))
        }
 
                musicPlayers.add(new MusicPlayer(id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription))
        }

diff --git a/PresenceSensor/PresenceSensors.groovy b/PresenceSensor/PresenceSensors.groovy
index 2408a5aa5c726535b7efd4bc5267bc600b8545a3..cb13242c3d622d9087797f570186379cc923aaa7 100644 (file)
--- a/PresenceSensor/PresenceSensors.groovy
+++ b/PresenceSensor/PresenceSensors.groovy
@@ -2,6 +2,9 @@
 package PresenceSensor
 import Timer.SimulatedTimer
 
 package PresenceSensor
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class PresenceSensors {
        private int deviceNumbers
        private List presenceSensors
 public class PresenceSensors {
        private int deviceNumbers
        private List presenceSensors


@@ -20,6 +23,14 @@ public class PresenceSensors {
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.presenceSensors = []
                this.sendEvent = sendEvent              
                this.deviceNumbers = deviceNumbers
                this.presenceSensors = []

+               def init = Verify.getBoolean()
+               if (init) {
+                       this.presence = "not present"
+                       this.presenceLatestValue = "not present"
+               } else {
+                       this.presence = "present"
+                       this.presenceLatestValue = "present"
+               }

 
                presenceSensors.add(new PresenceSensor(id, label, displayName, this.presence, this.presenceLatestValue))
        }
 
                presenceSensors.add(new PresenceSensor(id, label, displayName, this.presence, this.presenceLatestValue))
        }

diff --git a/SmokeDetector/SmokeDetectors.groovy b/SmokeDetector/SmokeDetectors.groovy
index 95bcb3c265a95b4072fbc02095f2abcc32f51c12..e9d5da2f67b6c87057cc915d970fb9dbb83a1dc1 100644 (file)
--- a/SmokeDetector/SmokeDetectors.groovy
+++ b/SmokeDetector/SmokeDetectors.groovy
@@ -2,6 +2,9 @@
 package SmokeDetector
 import Timer.SimulatedTimer
 
 package SmokeDetector
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class SmokeDetectors {
        private int deviceNumbers
        private List smokeDetectors
 public class SmokeDetectors {
        private int deviceNumbers
        private List smokeDetectors


@@ -21,6 +24,17 @@ public class SmokeDetectors {
                this.deviceNumbers = deviceNumbers
                this.smokeDetectors = []
 
                this.deviceNumbers = deviceNumbers
                this.smokeDetectors = []
 

+               def init = Verify.getInt(0,2)
+               if (init == 0) {
+                       this.currentSmokeValue = "clear"
+                       this.smokeLatestValue = "clear"
+               } else if (init == 1) {
+                       this.currentSmokeValue = "detected"
+                       this.smokeLatestValue = "detected"
+               } else {
+                       this.currentSmokeValue = "tested"
+                       this.smokeLatestValue = "tested"                
+               }

                smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue))
        }
 
                smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue))
        }
 

diff --git a/SpeechSynthesis/SpeechSynthesises.groovy b/SpeechSynthesis/SpeechSynthesises.groovy
index 033db31f6325f4e0b3fd6668bd13f9f340c147ef..bcdbbd7a835d9a4bb76f7f314944cb9fa2164da9 100644 (file)
--- a/SpeechSynthesis/SpeechSynthesises.groovy
+++ b/SpeechSynthesis/SpeechSynthesises.groovy
@@ -2,6 +2,9 @@
 package SpeechSynthesis
 import Timer.SimulatedTimer
 
 package SpeechSynthesis
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class SpeechSynthesises {
        private int deviceNumbers
        private List speechSynthesises
 public class SpeechSynthesises {
        private int deviceNumbers
        private List speechSynthesises


@@ -19,6 +22,9 @@ public class SpeechSynthesises {
                this.deviceNumbers = deviceNumbers
                this.speechSynthesises = []
 
                this.deviceNumbers = deviceNumbers
                this.speechSynthesises = []
 

+               def init = Verify.getIntFromList(30, 50, 70)
+               this.level = init
+

                speechSynthesises.add(new SpeechSynthesis(id, label, displayName, this.level))
        }
 
                speechSynthesises.add(new SpeechSynthesis(id, label, displayName, this.level))
        }
 

diff --git a/Switch/Switches.groovy b/Switch/Switches.groovy
index 9007388794254b1decf95d3eca6d96aae4978df7..36ba2de02918205039019e374806ad975c3f98ee 100644 (file)
--- a/Switch/Switches.groovy
+++ b/Switch/Switches.groovy
@@ -2,6 +2,9 @@
 package Switch
 import Timer.SimulatedTimer
 
 package Switch
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class Switches {
        int deviceNumbers       
        List switches
 public class Switches {
        int deviceNumbers       
        List switches


@@ -22,6 +25,19 @@ public class Switches {
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.switches = []
                this.timers = new SimulatedTimer()
                this.deviceNumbers = deviceNumbers
                this.switches = []

+               
+               def initLevel = Verify.getIntFromList(30, 50, 70)
+               this.currentLevel = initLevel
+               def init = Verify.getBoolean()
+               if (init) {
+                       this.switchState = "off"
+                       this.currentSwitch = "off"
+                       this.switchLatestValue = "off"
+               } else {
+                       this.switchState = "on"
+                       this.currentSwitch = "on"
+                       this.switchLatestValue = "on"
+               }

 
                switches.add(new Switch(sendEvent, id, label, displayName, this.switchState, this.currentSwitch, this.currentLevel, this.switchLatestValue))
        }
 
                switches.add(new Switch(sendEvent, id, label, displayName, this.switchState, this.currentSwitch, this.currentLevel, this.switchLatestValue))
        }

diff --git a/Thermostat/Thermostats.groovy b/Thermostat/Thermostats.groovy
index cc955d17e74849d1c73c6b8c333f8827c6c13180..66957ddff3d8de686730634a06b58ce967ee6f94 100644 (file)
--- a/Thermostat/Thermostats.groovy
+++ b/Thermostat/Thermostats.groovy
@@ -2,6 +2,9 @@
 package Thermostat
 import Timer.SimulatedTimer
 
 package Thermostat
 import Timer.SimulatedTimer
 

+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+

 public class Thermostats{
        int deviceNumbers       
        List thermostats        
 public class Thermostats{
        int deviceNumbers       
        List thermostats        


@@ -35,6 +38,51 @@ public class Thermostats{
                this.deviceNumbers = deviceNumbers
                this.thermostats = []
 
                this.deviceNumbers = deviceNumbers
                this.thermostats = []
 

+               def initTemperature = Verify.getIntFromList(60, 66, 70)
+               this.temperature = initTemperature
+               
+               def initCoolingSetpoint = Verify.getIntFromList(70, 80, 90)
+               this.currentCoolingSetpoint = initCoolingSetpoint
+               this.coolingSetpoint = initCoolingSetpoint
+               
+               def initHeatingSetpoint = Verify.getIntFromList(20, 35, 50)
+               this.currentHeatingSetpoint = initHeatingSetpoint
+               this.heatingSetpoint = initHeatingSetpoint
+               
+               def initThermostatSetpoint = Verify.getIntFromList(50, 60, 70)
+               this.currentHeatingSetpoint = initThermostatSetpoint
+               
+               def initFanMode = Verify.getInt(0,4)
+               if (initFanMode == 0) {
+                       this.thermostatFanMode = "auto"
+               } else if (initFanMode == 1) {
+                       this.thermostatFanMode = "fanCirculate"
+               } else if (initFanMode == 2) {
+                       this.thermostatFanMode = "circulate"
+               } else if (initFanMode == 3) {
+                       this.thermostatFanMode = "fanOn"
+               } else {
+                       this.thermostatFanMode = "on"
+               }
+
+               def initMode = Verify.getInt(0,4)
+               if (initMode == 0) {
+                       this.thermostatMode = "auto"
+                       this.currentThermostatMode = "auto"
+               } else if (initMode == 1) {
+                       this.thermostatMode = "cool"
+                       this.currentThermostatMode = "cool"
+               } else if (initMode == 2) {
+                       this.thermostatMode = "emergencyHeat"
+                       this.currentThermostatMode = "emergencyHeat"
+               } else if (initMode == 3) {
+                       this.thermostatMode = "heat"
+                       this.currentThermostatMode = "heat"
+               } else {
+                       this.thermostatMode = "off"
+                       this.currentThermostatMode = "off"
+               }
+

                thermostats.add(new Thermostat(sendEvent, id, label, displayName, this.temperature, this.currentCoolingSetpoint, 
                                                this.currentHeatingSetpoint, this.coolingSetpoint, this.thermostatSetpoint, this.heatingSetpoint, this.coolingSetpointRange,
                                                this.thermostatSetpointRange, this.heatingSetpointRange, this.supportedThermostatFanModes, this.supportedThermostatModes,
                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,