Infrastructure compatible with 2 types of switches.(Normal switches and otherVsGeneri...

diff --git a/EnergyMeter/EnergyMeter.groovy b/EnergyMeter/EnergyMeter.groovy
index c4eca238f66d6d13e23c209ea9688882523e243e..83f2283c3bdae185c2f27dd7ae8373717c863dbe 100644 (file)
--- a/EnergyMeter/EnergyMeter.groovy
+++ b/EnergyMeter/EnergyMeter.groovy
@@ -8,12 +8,14 @@ public class EnergyMeter {
        private String displayName
        private int energy
        private int currentEnergy
+       private String status
 
-       EnergyMeter(String id, String label, String displayName, int energy) {
+       EnergyMeter(String id, String label, String displayName, int energy, String status) {
                this.id = id
                this.label = label
                this.displayName = displayName
                this.energy = energy
+               this.status = status
        }
 
        //By Model Checker
@@ -23,6 +25,20 @@ public class EnergyMeter {
                this.currentEnergy = value.toInteger()
        }
 
+       def reset() {
+               if (status != "on") {
+                       status = "on"
+                       println("the energy meter is on!")
+               }
+       }
+
+       def off() {
+               if (status != "off") {
+                       status = "off"
+                       println("the energy meter is off!")
+               }
+       }
+
        def currentValue(String deviceFeature) {
                if (deviceFeature == "energy") {
                        return energy

diff --git a/EnergyMeter/EnergyMeters.groovy b/EnergyMeter/EnergyMeters.groovy
index d5a7aea62e626dbb07e35b433d82b52ccd396cff..5d8b74aa73146c8ee7106b8ce993639984354f09 100644 (file)
--- a/EnergyMeter/EnergyMeters.groovy
+++ b/EnergyMeter/EnergyMeters.groovy
@@ -13,6 +13,7 @@ public class EnergyMeters {
        private String displayName = "energyMeter0"
        private int energy = 50
        private int currentEnergy = 50
+       private String status = "off"
 
                
        EnergyMeters(Closure sendEvent, int deviceNumbers, boolean init) {
@@ -27,7 +28,7 @@ public class EnergyMeters {
                        this.energy = 60
                        this.currentEnergy = 60
                }
-               energyMeters.add(new EnergyMeter(id, label, displayName, this.energy))
+               energyMeters.add(new EnergyMeter(id, label, displayName, this.energy, this.status))
        }
 
        //By Model Checker
@@ -60,6 +61,19 @@ public class EnergyMeters {
                energyMeters.collect(Input)
        }
 
+       def reset() {
+               if (status != "on") {
+                       status = "on"
+                       energyMeters[0].reset()
+               }
+       }
+       
+       def off() {
+               if (status != "off") {
+                       status = "off"
+                       energyMeters[0].off()
+               }
+       }
 
        def currentValue(String deviceFeature) {
                energyMeters[0].currentValue(deviceFeature)//It is called if we have only one device

diff --git a/Location/LocationVar.groovy b/Location/LocationVar.groovy
index ca20cff63e615262e02dbc1eed6704091554911b..d006c4e70cdce141529b8038f1c1e838134f2346 100644 (file)
--- a/Location/LocationVar.groovy
+++ b/Location/LocationVar.groovy
@@ -10,8 +10,9 @@ class LocationVar {
        private String name
        private List contacts
        private List phoneNumbers
+       private String temperatureScale 
        def sendEvent
-    
+       
        private Phrase helloHome
 
        LocationVar(Closure sendEvent) {
@@ -25,6 +26,7 @@ class LocationVar {
                this.sendEvent = sendEvent
                this.timeZone = TimeZone.getTimeZone("America/New_York")
                this.name = "hub0"
+               this.temperatureScale = "F"
        }
 
        //By Model Checker

diff --git a/MotionSensor/MotionSensor.groovy b/MotionSensor/MotionSensor.groovy
index 01f1363256190d9c5411bcfc4da8b475c974a588..931069b165234b9182a88fc43ac946169b4fa049 100644 (file)
--- a/MotionSensor/MotionSensor.groovy
+++ b/MotionSensor/MotionSensor.groovy
@@ -2,6 +2,9 @@
 package MotionSensor
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class MotionSensor {
        private String id
        private String label
@@ -27,6 +30,10 @@ public class MotionSensor {
        }
 
        def statesSince() {
+               eventsSince()
+       }
+
+       def eventsSince() {
                def evtActive = [[name: "motion", value: "active", deviceId: "motionSensorID0", descriptionText: "",
                                  displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
                def evtInactive = [[name: "motion", value: "inactive", deviceId: "motionSensorID0", descriptionText: "",

diff --git a/MotionSensor/MotionSensors.groovy b/MotionSensor/MotionSensors.groovy
index c799b0e77766697fd893a67c8bebcdfe314452e5..5c03ebf677c2cf90700d63c2d859e8129b5966a0 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
@@ -80,6 +83,10 @@ public class MotionSensors {
                return motionSensors[0].statesSince()
        }
 
+       def eventsSince(Date dateObj) {
+               return motionSensors[0].statesSince()
+       }
+
        def getAt(int ix) {
                motionSensors[ix]
        }

diff --git a/TemperatureMeasurement/TemperatureMeasurement.groovy b/TemperatureMeasurement/TemperatureMeasurement.groovy
index afcb768b9882ca7f4728396348f2ed19ee22c93c..88c3c8d4191f0f95bc6bdccae105188d622ce897 100644 (file)
--- a/TemperatureMeasurement/TemperatureMeasurement.groovy
+++ b/TemperatureMeasurement/TemperatureMeasurement.groovy
@@ -2,6 +2,9 @@
 package TemperatureMeasurement
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class TemperatureMeasurement {
        private String id
        private String label
@@ -17,6 +20,21 @@ public class TemperatureMeasurement {
                this.currentTemperature = temperature
        }
 
+       def eventsSince() {
+               def evtTemp = [[name: "temperature", value: this.temperature.toString(), deviceId: "temperatureMeasurementID0", descriptionText: "",
+                               displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
+               def init = Verify.getInt(0,1)
+               def evtToSend = []
+               if (init == 0) {//return empty set
+                       return evtToSend
+               } else if (init == 1) {//send one open event
+                       evtTemp.each{
+                               evtToSend.add(it)
+                       }
+                       return evtToSend
+               }
+       }
+
        //By Model Checker
        def setValue(String value) {
                println("the temperature is changed to $value!")

diff --git a/TemperatureMeasurement/TemperatureMeasurements.groovy b/TemperatureMeasurement/TemperatureMeasurements.groovy
index 1f6d932e2ddb569c97d26b3d9ffe569482d58641..215894f89d5cc922e6ae45ef121344207570db00 100644 (file)
--- a/TemperatureMeasurement/TemperatureMeasurements.groovy
+++ b/TemperatureMeasurement/TemperatureMeasurements.groovy
@@ -2,6 +2,9 @@
 package TemperatureMeasurement
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class TemperatureMeasurements {
        private int deviceNumbers
        private List temperatureMeasurements
@@ -39,6 +42,10 @@ public class TemperatureMeasurements {
                }
        }
 
+       def eventsSince(Date dateObj) {
+               return temperatureMeasurements[0].eventsSince()
+       }
+
        //Methods for closures
        def count(Closure Input) {
                temperatureMeasurements.count(Input)