From 6da0a8cedec52b542e0d5046632ae1c166e260cf Mon Sep 17 00:00:00 2001 From: amiraj Date: Tue, 6 Aug 2019 17:16:43 -0700 Subject: [PATCH] Infrastructure compatible with 2 types of switches.(Normal switches and otherVsGeneric switches.) --- EnergyMeter/EnergyMeter.groovy | 18 +++++++++++++++++- EnergyMeter/EnergyMeters.groovy | 16 +++++++++++++++- Location/LocationVar.groovy | 4 +++- MotionSensor/MotionSensor.groovy | 7 +++++++ MotionSensor/MotionSensors.groovy | 7 +++++++ .../TemperatureMeasurement.groovy | 18 ++++++++++++++++++ .../TemperatureMeasurements.groovy | 7 +++++++ 7 files changed, 74 insertions(+), 3 deletions(-) diff --git a/EnergyMeter/EnergyMeter.groovy b/EnergyMeter/EnergyMeter.groovy index c4eca23..83f2283 100644 --- 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 d5a7aea..5d8b74a 100644 --- 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 ca20cff..d006c4e 100644 --- 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 01f1363..931069b 100644 --- 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 c799b0e..5c03ebf 100644 --- 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 afcb768..88c3c8d 100644 --- 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 1f6d932..215894f 100644 --- 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) -- 2.34.1