Fixing the previous commit bugs! Adding required classes + required methods

diff --git a/Button/Button.groovy b/Button/Button.groovy
new file mode 100644 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 6f8bd4def5599b5c28792704c7248d8e5fae598e..8e2db793888869dbbfceb0df17383282fb43caf2 100644 (file)
--- 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")
 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")
 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 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")
 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)
        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:
 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")
 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")
 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)
        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:
 Out.write("\n")
 Start = 0
 for line in App2: