Infrastructure compatible with 2 types of switches.(Normal switches and otherVsGeneri...
authoramiraj <amiraj.95@uci.edu>
Wed, 7 Aug 2019 00:16:43 +0000 (17:16 -0700)
committeramiraj <amiraj.95@uci.edu>
Wed, 7 Aug 2019 00:16:43 +0000 (17:16 -0700)
EnergyMeter/EnergyMeter.groovy
EnergyMeter/EnergyMeters.groovy
Location/LocationVar.groovy
MotionSensor/MotionSensor.groovy
MotionSensor/MotionSensors.groovy
TemperatureMeasurement/TemperatureMeasurement.groovy
TemperatureMeasurement/TemperatureMeasurements.groovy

index c4eca23..83f2283 100644 (file)
@@ -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
index d5a7aea..5d8b74a 100644 (file)
@@ -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
index ca20cff..d006c4e 100644 (file)
@@ -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
index 01f1363..931069b 100644 (file)
@@ -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: "",
index c799b0e..5c03ebf 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
@@ -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]
        }
index afcb768..88c3c8d 100644 (file)
@@ -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!")
index 1f6d932..215894f 100644 (file)
@@ -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)