Adding path explorations for initializations.
authorrtrimana <rtrimana@uci.edu>
Fri, 26 Jul 2019 21:13:47 +0000 (14:13 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 26 Jul 2019 21:13:47 +0000 (14:13 -0700)
18 files changed:
AccelerationSensor/AccelerationSensors.groovy
Alarm/Alarms.groovy
Battery/Batteries.groovy
BeaconSensor/BeaconSensors.groovy
CarbonMonoxideDetector/CarbonMonoxideDetectors.groovy
ColorControl/ColorControls.groovy
ContactSensor/ContactSensors.groovy
DoorControl/DoorControls.groovy
EnergyMeter/EnergyMeters.groovy
ImageCapture/ImageCaptures.groovy
Lock/Locks.groovy
MotionSensor/MotionSensors.groovy
MusicPlayer/MusicPlayers.groovy
PresenceSensor/PresenceSensors.groovy
SmokeDetector/SmokeDetectors.groovy
SpeechSynthesis/SpeechSynthesises.groovy
Switch/Switches.groovy
Thermostat/Thermostats.groovy

index 0d3c14f..8c1992c 100644 (file)
@@ -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))
        }
 
index 2eb775e..b2759bd 100644 (file)
@@ -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))
        }
                
index ce4a187..6e40e12 100644 (file)
@@ -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))
        }
index 24bcfc8..33dd1fe 100644 (file)
@@ -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))
        }
 
index 7e848e3..511d031 100644 (file)
@@ -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
index b3a6471..6eb5ac6 100644 (file)
@@ -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))
        }
index 1de8c76..489200d 100644 (file)
@@ -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))
        }
 
index 9210899..444154d 100644 (file)
@@ -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))
        }
 
index caec875..5967084 100644 (file)
@@ -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))
        }
 
index 2a63a3e..9e5bd9a 100644 (file)
@@ -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))
        }
 
index f792c6c..f2b9d75 100644 (file)
@@ -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))
        }
 
index 863903c..8516713 100644 (file)
@@ -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))
        }
 
index bf733db..847dd1c 100644 (file)
@@ -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))
        }
index 2408a5a..cb13242 100644 (file)
@@ -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))
        }
index 95bcb3c..e9d5da2 100644 (file)
@@ -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))
        }
 
index 033db31..bcdbbd7 100644 (file)
@@ -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))
        }
 
index 9007388..36ba2de 100644 (file)
@@ -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))
        }
index cc955d1..66957dd 100644 (file)
@@ -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,