From 7d426cdadcd09717f1c33b740731a4ddb29adb06 Mon Sep 17 00:00:00 2001 From: amiraj Date: Sat, 3 Aug 2019 15:49:27 -0700 Subject: [PATCH] Fixing the previous commit bugs! Adding required classes + required methods --- Button/Button.groovy | 65 ++++++++++++ Button/Buttons.groovy | 65 ++++++++++++ ColorTemperature/ColorTemperature.groovy | 103 +++++++++++++++++++ ColorTemperature/ColorTemperatures.groovy | 117 ++++++++++++++++++++++ Methods/parseJson.groovy | 4 + Methods/unsubscribe.groovy | 6 ++ Runner.py | 16 +++ 7 files changed, 376 insertions(+) create mode 100644 Button/Button.groovy create mode 100644 Button/Buttons.groovy create mode 100644 ColorTemperature/ColorTemperature.groovy create mode 100644 ColorTemperature/ColorTemperatures.groovy create mode 100644 Methods/parseJson.groovy create mode 100644 Methods/unsubscribe.groovy diff --git a/Button/Button.groovy b/Button/Button.groovy new file mode 100644 index 0000000..45123fa --- /dev/null +++ b/Button/Button.groovy @@ -0,0 +1,65 @@ +//Create a class for button +package Button +import Timer.SimulatedTimer + +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + +public class Button { + private String id + private String label + private String displayName + private String button + private int numberOfButtons + + Button(String id, String label, String displayName, String button, int numberOfButtons) { + this.id = id + this.label = label + this.displayName = displayName + this.button = button + this.numberOfButtons = numberOfButtons + } + + def setValue(LinkedHashMap eventDataMap) { + button = eventDataMap["value"] + println("the button is $button!") + } + + def eventsSince() { + def evtHeld = [[name: "button", value: "held", deviceId: "buttonID0", descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']] + def evtPushed = [[name: "button", value: "pushed", deviceId: "buttonID0", descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']] + def init = Verify.getInt(0,4) + def evtToSend = [] + if (init == 0) {//return empty set + return evtToSend + } else if (init == 1) {//send one held event + evtHeld.each{ + evtToSend.add(it) + } + return evtToSend + } else if (init == 2) {//send two held events + evtHeld.each{ + evtToSend.add(it) + } + evtHeld.each{ + evtToSend.add(it) + } + return evtToSend + } else if (init == 3) {//send one pushed event + evtPushed.each{ + evtToSend.add(it) + } + return evtToSend + } else if (init == 4) {//send two pushed events + evtPushed.each{ + evtToSend.add(it) + } + evtPushed.each{ + evtToSend.add(it) + } + return evtToSend + } + } +} diff --git a/Button/Buttons.groovy b/Button/Buttons.groovy new file mode 100644 index 0000000..423b956 --- /dev/null +++ b/Button/Buttons.groovy @@ -0,0 +1,65 @@ +//Create a class for button +package Button +import Timer.SimulatedTimer + +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + +public class Buttons { + private int deviceNumbers + private List buttons + def sendEvent + + //For one device(We cannot have obj.id)-> We should have obj[0].id + private String id = "buttonID0" + private String label = "button0" + private String displayName = "button0" + private String button = "pushed" + private int numberOfButtons = 4 + + + Buttons(Closure sendEvent, int deviceNumbers) { + this.sendEvent = sendEvent + this.deviceNumbers = deviceNumbers + this.buttons = [] + + buttons.add(new Button(id, label, displayName, button, numberOfButtons)) + } + + //By Model Checker + def setValue(LinkedHashMap eventDataMap) { + buttons[0].setValue(eventDataMap) + sendEvent(eventDataMap) + } + + //Methods for closures + def count(Closure Input) { + buttons.count(Input) + } + def size() { + buttons.size() + } + def each(Closure Input) { + buttons.each(Input) + } + def sort(Closure Input) { + buttons.sort(Input) + } + def find(Closure Input) { + buttons.find(Input) + } + def collect(Closure Input) { + buttons.collect(Input) + } + + + //methods + def eventsSince(Date dateObj) { + return buttons[0].eventsSince() + } + + + def getAt(int ix) { + buttons[ix] + } +} diff --git a/ColorTemperature/ColorTemperature.groovy b/ColorTemperature/ColorTemperature.groovy new file mode 100644 index 0000000..d73ed9b --- /dev/null +++ b/ColorTemperature/ColorTemperature.groovy @@ -0,0 +1,103 @@ +//Create a class for color temperature +package ColorTemperature +import Timer.SimulatedTimer + + +public class ColorTemperature { + def sendEvent + private String id + private String label + private String displayName + private String currentSwitch + private int level + private int currentLevel + private int colorTemperature + + ColorTemperature(Closure sendEvent, String id, String label, String displayName, int level, String currentSwitch, int colorTemperature) { + this.id = id + this.label = label + this.displayName = displayName + this.level = level + this.currentLevel = level + this.currentSwitch = currentSwitch + this.colorTemperature = colorTemperature + this.sendEvent = sendEvent + } + + //By model checker + def setValue(String value, String name) { + if ((name == "level") && (value != this.level)) { + this.currentLevel = value.toInteger() + this.level = value.toInteger() + println("The level of the light is changed to $value!") + } else if ((name == "currentSwitch") && (value != this.currentSwitch)) { + this.currentSwitch = value + println("The light is changed to $value!") + } else if ((name == "colorTemperature") && (value != this.colorTemperature)) { + this.colorTemperature = value.toInteger() + println("The color temperature level of the light is changed to $value!") + } + } + + //methods + def setLevel(int level) { + if (level != this.level) { + this.currentLevel = level + this.level = level + println("The level of the light is changed to $level!") + sendEvent([name: "level", value: "$level", deviceId: this.id, descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) + } + } + + def setColorTemperature(int colorTemperature) { + if (colorTemperature != this.colorTemperature) { + this.colorTemperature = colorTemperature + println("The color temperature level of the light is changed to $colorTemperature!") + sendEvent([name: "colorTemperature", value: "$colorTemperature", deviceId: this.id, descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) + } + } + + def on(String currentSwitch) { + if (currentSwitch != this.currentSwitch) { + this.currentSwitch = currentSwitch + println("The light is changed to $currentSwitch!") + sendEvent([name: "switch", value: "$currentSwitch", deviceId: this.id, descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) + sendEvent([name: "switch.on", value: "$currentSwitch", deviceId: this.id, descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) + } + } + + def off(String currentSwitch) { + if (currentSwitch != this.currentSwitch) { + this.currentSwitch = currentSwitch + println("The light is changed to $currentSwitch!") + sendEvent([name: "switch", value: "$currentSwitch", deviceId: this.id, descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) + sendEvent([name: "switch.off", value: "$currentSwitch", deviceId: this.id, descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) + } + } + + def currentValue(String deviceFeature) { + if (deviceFeature == "level") { + return level + } else if (deviceFeature == "colorTemperature") { + return colorTemperature + } else if (deviceFeature == "switch") { + return currentSwitch + } + } + + def latestValue(String deviceFeature) { + if (deviceFeature == "level") { + return level + } else if (deviceFeature == "colorTemperature") { + return colorTemperature + } else if (deviceFeature == "switch") { + return currentSwitch + } + } +} diff --git a/ColorTemperature/ColorTemperatures.groovy b/ColorTemperature/ColorTemperatures.groovy new file mode 100644 index 0000000..952bfcd --- /dev/null +++ b/ColorTemperature/ColorTemperatures.groovy @@ -0,0 +1,117 @@ +//Create a class for color temperature +package ColorTemperature +import Timer.SimulatedTimer + +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + +public class ColorTemperatures { + private int deviceNumbers + private List colorTemperatues + def sendEvent + + //For one device(We cannot have obj.id)-> We should have obj[0].id + private String id = "colorTemperatureID0" + private String label = "colorTemperature0" + private String displayName = "colorTemperature0" + private String currentSwitch = "off" + private int level = 50 + private int currentLevel = 50 + private int colorTemperature = 15000 + + + ColorTemperatures(Closure sendEvent, int deviceNumbers) { + this.sendEvent = sendEvent + this.deviceNumbers = deviceNumbers + this.colorTemperatues = [] + + colorTemperatues.add(new ColorTemperature(sendEvent, id, label, displayName, this.level, this.currentSwitch, this.colorTemperature)) + } + + //Methods for closures + def count(Closure Input) { + colorTemperatues.count(Input) + } + def size() { + colorTemperatues.size() + } + def each(Closure Input) { + colorTemperatues.each(Input) + } + def find(Closure Input) { + colorTemperatues.find(Input) + } + def sort(Closure Input) { + colorTemperatues.sort(Input) + } + def collect(Closure Input) { + colorTemperatues.collect(Input) + } + + //By model checker + def setValue(LinkedHashMap eventDataMap) { + if (eventDataMap["name"] == "switch") { + if (eventDataMap["value"] != colorTemperatues[0].currentSwitch) { + this.currentSwitch = eventDataMap["value"] + colorTemperatues[0].setValue(eventDataMap["value"], "switch") + sendEvent(eventDataMap) + } + } else if (eventDataMap["name"] == "colorTemperature") { + if (eventDataMap["value"].toInteger() != colorTemperatues[0].colorTemperature) { + this.colorTemperature = eventDataMap["value"].toInteger() + colorTemperatues[0].setValue(eventDataMap["value"], "colorTemperature") + sendEvent(eventDataMap) + } + } else if (eventDataMap["name"] == "level") { + if (eventDataMap["value"].toInteger() != colorTemperatues[0].level) { + this.currentLevel = eventDataMap["value"].toInteger() + this.level = eventDataMap["value"].toInteger() + colorTemperatues[0].setValue(eventDataMap["value"], "level") + sendEvent(eventDataMap) + } + } + } + + + //methods + def setLevel(int level) { + if (level != this.level) { + this.currentLevel = level + this.level = level + colorTemperatues[0].setLevel(level) + } + } + + def setColorTemperature(String colorTemperature) { + if (colorTemperature != this.colorTemperature) { + this.colorTemperature = colorTemperature + colorTemperatues[0].setColorTemperature(colorTemperature) + } + } + + def on(String currentSwitch) { + if (currentSwitch != this.currentSwitch) { + this.currentSwitch = currentSwitch + colorTemperatues[0].on(currentSwitch) + } + } + + def off(String currentSwitch) { + if (currentSwitch != this.currentSwitch) { + this.currentSwitch = currentSwitch + colorTemperatues[0].off(currentSwitch) + } + } + + def currentValue(String deviceFeature) { + colorTemperatues[0].currentValue(deviceFeature) + } + + def latestValue(String deviceFeature) { + colorTemperatues[0].latestValue(deviceFeature) + } + + def getAt(int ix) { + colorTemperatues[ix] + } +} diff --git a/Methods/parseJson.groovy b/Methods/parseJson.groovy new file mode 100644 index 0000000..b7de692 --- /dev/null +++ b/Methods/parseJson.groovy @@ -0,0 +1,4 @@ +///////////////////////////////////////////////////////////////////// +def parseJson(String data) { + return new groovy.json.JsonSlurper().parseText(data) +} \ No newline at end of file diff --git a/Methods/unsubscribe.groovy b/Methods/unsubscribe.groovy new file mode 100644 index 0000000..ba20619 --- /dev/null +++ b/Methods/unsubscribe.groovy @@ -0,0 +1,6 @@ +///////////////////////////////////////////////////////////////////// +def unsubscribe() { + objectList.clear() + eventList.clear() + functionList.clear() +} \ No newline at end of file diff --git a/Runner.py b/Runner.py index 6f8bd4d..8e2db79 100644 --- a/Runner.py +++ b/Runner.py @@ -31,6 +31,8 @@ sendNotification = open("Methods/"+"sendNotification.groovy", "r") canSchedule = open("Methods/"+"canSchedule.groovy", "r") createAccessToken = open("Methods/"+"createAccessToken.groovy", "r") runOnce = open("Methods/"+"runOnce.groovy", "r") +parseJson = open("Methods/"+"parseJson.groovy", "r") +unsubscribe = open("Methods/"+"unsubscribe.groovy", "r") App1 = open("Extractor/"+"App1/App1.groovy", "r") extractedObjectsApp1 = open("Extractor/"+"App1/extractedObjectsApp1.groovy", "r") extractedObjectsConstructorApp1 = open("Extractor/"+"App1/extractedObjectsConstructorApp1.groovy", "r") @@ -110,6 +112,10 @@ Out.write("import Valve.Valve\n") Out.write("import Valve.Valves\n") Out.write("import MobilePresence.MobilePresence\n") Out.write("import MobilePresence.MobilePresences\n") +Out.write("import ColorTemperature.ColorTemperature\n") +Out.write("import ColorTemperature.ColorTemperatures\n") +Out.write("import Button.Button\n") +Out.write("import Button.Buttons\n") Out.write("import Event.Event\n") Out.write("import Timer.SimulatedTimer\n") Out.write("\n") @@ -186,6 +192,10 @@ for line in createAccessToken: Out.write("\t"+line) for line in runOnce: Out.write("\t"+line) +for line in parseJson: + Out.write("\t"+line) +for line in unsubscribe: + Out.write("\t"+line) Out.write("\n") Start = 0 for line in App1: @@ -219,6 +229,8 @@ sendNotification = open("Methods/"+"sendNotification.groovy", "r") canSchedule = open("Methods/"+"canSchedule.groovy", "r") createAccessToken = open("Methods/"+"createAccessToken.groovy", "r") runOnce = open("Methods/"+"runOnce.groovy", "r") +parseJson = open("Methods/"+"parseJson.groovy", "r") +unsubscribe = open("Methods/"+"unsubscribe.groovy", "r") App2 = open("Extractor/"+"App2/App2.groovy", "r") extractedObjectsApp2 = open("Extractor/"+"App2/extractedObjectsApp2.groovy", "r") extractedObjectsConstructorApp2 = open("Extractor/"+"App2/extractedObjectsConstructorApp2.groovy", "r") @@ -286,6 +298,10 @@ for line in createAccessToken: Out.write("\t"+line) for line in runOnce: Out.write("\t"+line) +for line in parseJson: + Out.write("\t"+line) +for line in unsubscribe: + Out.write("\t"+line) Out.write("\n") Start = 0 for line in App2: -- 2.34.1