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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class AccelerationSensors {
        private int deviceNumbers
        private List accelerationSensors
@@ -21,6 +24,14 @@ public class 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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class Alarms {
        int deviceNumbers       
        List alarms
@@ -22,6 +25,16 @@ public class 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))
        }
                

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class Batteries {
        private int deviceNumbers
        private List batteries
@@ -19,6 +22,9 @@ public class 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))
        }

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class BeaconSensors {
        private int deviceNumbers
        private List beaconSensors
@@ -21,6 +24,14 @@ public class 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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class CarbonMonoxideDetectors {
        private int deviceNumbers
        private List carbonMonoxideDetectors
@@ -20,8 +23,19 @@ public class 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

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
 
 public class ColorControls {
        private int deviceNumbers
@@ -21,6 +23,19 @@ public class 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))
        }

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class ContactSensors {
        private int deviceNumbers
        private List contacts
@@ -22,6 +25,23 @@ public class ContactSensors {
                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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class DoorControls {
        int deviceNumbers       
        List doorControls
@@ -20,7 +23,15 @@ public class 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))
        }
 

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 = []
-
+               
+               def init = Verify.getIntFromList(30, 50, 70)
+               this.energy = init
+               
                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 = []
 
+               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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class Locks{
        int deviceNumbers       
        List locks      
@@ -22,6 +25,14 @@ public class 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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class MotionSensors {
        private int deviceNumbers
        private List motionSensors
@@ -21,6 +24,14 @@ public class 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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
 
 public class MusicPlayers {
        private int deviceNumbers
@@ -25,6 +27,35 @@ public class 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))
        }

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class PresenceSensors {
        private int deviceNumbers
        private List presenceSensors
@@ -20,6 +23,14 @@ public class 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))
        }

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class SmokeDetectors {
        private int deviceNumbers
        private List smokeDetectors
@@ -21,6 +24,17 @@ public class 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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class SpeechSynthesises {
        private int deviceNumbers
        private List speechSynthesises
@@ -19,6 +22,9 @@ public class 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))
        }
 

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class Switches {
        int deviceNumbers       
        List switches
@@ -22,6 +25,19 @@ public class 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))
        }

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
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class Thermostats{
        int deviceNumbers       
        List thermostats        
@@ -35,6 +38,51 @@ public class 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,