Adding path explorations for initializations.

[smartthings-infrastructure.git] / Thermostat / Thermostats.groovy

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,