Merging changes.

diff --git a/AeonKeyFob/AeonKeyFob.groovy b/AeonKeyFob/AeonKeyFob.groovy
index 8ece0c6db1864dafdc25036f103f982618f7b729..72e5afd419614b5789683d8960a4d17ca8cd76e8 100644 (file)
--- a/AeonKeyFob/AeonKeyFob.groovy
+++ b/AeonKeyFob/AeonKeyFob.groovy
@@ -2,12 +2,13 @@
 package AeonKeyFob
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class AeonKeyFob {
        private String id
        private String label
        private String displayName
-       private List events = []
-       private List timeOfEvents = []
 
        AeonKeyFob(String id, String label, String displayName) {
                this.id = id
@@ -19,17 +20,43 @@ public class AeonKeyFob {
                def data = eventDataMap["data"]
                def value = eventDataMap["value"]
                println("the button with number $data is $value!")
-               this.events.add(eventDataMap)
-               this.timeOfEvents.add(System.currentTimeMillis())
        }
 
-       def eventsSince(Date dateObj) {
-               def List happenedEvents = []
-               def sinceThen = dateObj.time
-               for (int i = 0;i < timeOfEvents.size();i++) {
-                       if (timeOfEvents[i]>=sinceThen)
-                               happenedEvents.add(events[i])
+       def eventsSince() {
+               def evtHeld = [[name: "button", value: "held", deviceId: "aeonKeyFobID0", descriptionText: "",
+                               displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
+               def evtPushed = [[name: "button", value: "pushed", deviceId: "aeonKeyFobID0", 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
                }
-               return happenedEvents
        }
 }

diff --git a/AeonKeyFob/AeonKeyFobs.groovy b/AeonKeyFob/AeonKeyFobs.groovy
index bbb1a35be6885713fee4db22984a6b5e6db1f3dd..6383898b5538d9af16ea8f8fc0d6375d628b0d57 100644 (file)
--- a/AeonKeyFob/AeonKeyFobs.groovy
+++ b/AeonKeyFob/AeonKeyFobs.groovy
@@ -2,6 +2,9 @@
 package AeonKeyFob
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class AeonKeyFobs {
        private int deviceNumbers
        private List aeonKeyFobs
@@ -50,7 +53,7 @@ public class AeonKeyFobs {
 
        //methods
        def eventsSince(Date dateObj) {
-               return aeonKeyFobs[0].eventsSince(dateObj)
+               return aeonKeyFobs[0].eventsSince()
        }
 
 

diff --git a/ColorControl/ColorControl.groovy b/ColorControl/ColorControl.groovy
index 53658dce6e3ddb542ee1f616f6a7fa4174fd195d..4d6eaf7ceb53b54aa58ef2627c49ba14b091300a 100644 (file)
--- a/ColorControl/ColorControl.groovy
+++ b/ColorControl/ColorControl.groovy
@@ -4,6 +4,7 @@ import Timer.SimulatedTimer
 
 
 public class ColorControl {
+       def sendEvent
        private String id
        private String label
        private String displayName
@@ -14,7 +15,7 @@ public class ColorControl {
        private int saturation
        private int colorTemperature
        
-       ColorControl(String id, String label, String displayName, String color, int hue, int saturation, int level, String currentSwitch, int colorTemperature) {
+       ColorControl(Closure sendEvent, String id, String label, String displayName, String color, int hue, int saturation, int level, String currentSwitch, int colorTemperature) {
                this.id = id
                this.label = label
                this.displayName = displayName
@@ -24,6 +25,7 @@ public class ColorControl {
                this.level = level
                this.currentSwitch = currentSwitch
                this.colorTemperature = colorTemperature
+               this.sendEvent = sendEvent
        }
        
        //By model checker

diff --git a/ColorControl/ColorControls.groovy b/ColorControl/ColorControls.groovy
index 5b29f55e54eb51d83ebe1e13a7d8f0545eeff57b..5262e91b64b9c9fa69a0dcf87b3041d94f3ec9eb 100644 (file)
--- a/ColorControl/ColorControls.groovy
+++ b/ColorControl/ColorControls.groovy
@@ -40,7 +40,7 @@ public class ColorControls {
                        this.color = "blue"
                }*/
 
-               colorControls.add(new ColorControl(id, label, displayName, this.color, this.hue, this.saturation, this.level, this.currentSwitch, this.colorTemperature))
+               colorControls.add(new ColorControl(sendEvent, id, label, displayName, this.color, this.hue, this.saturation, this.level, this.currentSwitch, this.colorTemperature))
        }
 
        //Methods for closures

diff --git a/ContactSensor/ContactSensor.groovy b/ContactSensor/ContactSensor.groovy
index 413b58ce1f29214abf4608e1b65f7565466ec36c..4a10a5731b291639b34dbad81a34a00156682ba9 100644 (file)
--- a/ContactSensor/ContactSensor.groovy
+++ b/ContactSensor/ContactSensor.groovy
@@ -2,6 +2,9 @@
 package ContactSensor
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class ContactSensor {
        private String id
        private String label
@@ -24,6 +27,52 @@ public class ContactSensor {
                this.alarmState = alarmState
        }
 
+       def eventsSince() {
+               def evtOpen = [[name: "contact.open", value: "open", deviceId: "contactSensorID0", descriptionText: "",
+                               displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}'],
+                              [name: "contact", value: "open", deviceId: "contactSensorID0", descriptionText: "",
+                               displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}'],
+                              [name: "tamper.tampered", value: "open", deviceId: "contactSensorID0", descriptionText: "",
+                               displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
+               def evtClosed = [[name: "contact.closed", value: "closed", deviceId: "contactSensorID0", descriptionText: "",
+                                 displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}'],
+                                [name: "contact", value: "closed", deviceId: "contactSensorID0", descriptionText: "",
+                                 displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}'],
+                                [name: "tamper.tampered", value: "closed", deviceId: "contactSensorID0", 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 open event
+                       evtOpen.each{
+                               evtToSend.add(it)
+                       }
+                       return evtToSend
+               } else if (init == 2) {//send two open events
+                       evtOpen.each{
+                               evtToSend.add(it)
+                       }
+                       evtOpen.each{
+                               evtToSend.add(it)
+                       }
+                       return evtToSend
+               } else if (init == 3) {//send one closed event
+                       evtClosed.each{
+                               evtToSend.add(it)
+                       }
+                       return evtToSend
+               } else if (init == 4) {//send two closed events
+                       evtClosed.each{
+                               evtToSend.add(it)
+                       }
+                       evtClosed.each{
+                               evtToSend.add(it)
+                       }
+                       return evtToSend
+               }
+       }
+
        def setValue(String value) {
                println("the contact sensor with id:$id is triggered to $value!")
                this.contactState = value

diff --git a/ContactSensor/ContactSensors.groovy b/ContactSensor/ContactSensors.groovy
index 74508a8aba0915799114b190407e3961f5c91d6b..5f5f20e97b9ad97e13bcdfd96493de08f0c53141 100644 (file)
--- a/ContactSensor/ContactSensors.groovy
+++ b/ContactSensor/ContactSensors.groovy
@@ -59,6 +59,10 @@ public class ContactSensors {
                }
        }
 
+       def eventsSince(Date dateObj) {
+               return contacts[0].eventsSince()
+       }
+
        def on() {
                this.alarmState = "armed"
                contacts[0].on()

diff --git a/GlobalVariables/GlobalVariablesEachApp.groovy b/GlobalVariables/GlobalVariablesEachApp.groovy
index 8ae34ad07c32e71b31d3b40804f1769ad0b2d582..ae8b936042f5259750bbfa5c5f9791853bec2a30 100644 (file)
--- a/GlobalVariables/GlobalVariablesEachApp.groovy
+++ b/GlobalVariables/GlobalVariablesEachApp.groovy
@@ -8,10 +8,6 @@ def functionList = []
 def objectList = []
 //Create a global variable for Events in Subscribe method
 def eventList = []
-//Create a global list for function schedulers
-def timersFuncList = []
-//Create a global list for timer schedulers
-def timersList = []
 //Create a global variable for settings
 def settings
 //Zip code

diff --git a/Methods/runIn.groovy b/Methods/runIn.groovy
index 6e4bea3284d568e48e775be20a1880cf3e490cc0..1ca8d95b239c0f37d7e1de4ee42f862272bc8e75 100644 (file)
--- a/Methods/runIn.groovy
+++ b/Methods/runIn.groovy
@@ -1,14 +1,15 @@
 /////////////////////////////////////////////////////////////////////
 ////runIn(time, func)
 def runIn(int seconds, Closure functionToCall) {
-       if (timersFuncList.contains(functionToCall)) {
+       /*if (timersFuncList.contains(functionToCall)) {
                timersList[timersFuncList.indexOf(functionToCall)].cancel()
                def task = timersList[timersFuncList.indexOf(functionToCall)].runAfter(1000*seconds*0, functionToCall)
        } else {
                timersFuncList.add(functionToCall)
                timersList.add(new SimulatedTimer())
                def task = timersList[timersFuncList.indexOf(functionToCall)].runAfter(1000*seconds*0, functionToCall)
-       }
+       }*/
+       functionToCall()
 }
 
 def runIn(int seconds, Closure functionToCall, LinkedHashMap metaData) {
@@ -20,9 +21,10 @@ def runIn(int seconds, String nameOfFunction, LinkedHashMap metaData) {
 }
 
 def runIn(int seconds, String nameOfFunction) {
-       timersFuncList.add(nameOfFunction)
+       /*timersFuncList.add(nameOfFunction)
        timersList.add(new SimulatedTimer())
        def task = timersList[timersFuncList.indexOf(nameOfFunction)].runAfter(seconds*1000*0) {
                "$nameOfFunction"()
-       }
+       }*/
+       "$nameOfFunction"()
 }

diff --git a/Methods/runOnce.groovy b/Methods/runOnce.groovy
index 335cc19f2cddaaf3a376657604f78c1c07617215..308f6c34472cdcdcd95c6cc5c991d561f5be59ac 100644 (file)
--- a/Methods/runOnce.groovy
+++ b/Methods/runOnce.groovy
@@ -1,4 +1,4 @@
 /////////////////////////////////////////////////////////////////////
 def runOnce(Date date, Closure methodToCall) {
-       methodTocall()
+       methodToCall()
 }

diff --git a/Methods/schedule.groovy b/Methods/schedule.groovy
index 307b221e25c3f2a89cd3f6f3981ec78648d5252d..1d8c810b7e70c195e8c1372a5ce4c338c00781b0 100644 (file)
--- a/Methods/schedule.groovy
+++ b/Methods/schedule.groovy
@@ -1,49 +1,51 @@
 /////////////////////////////////////////////////////////////////////
 ////schedule(time, nameOfFunction as String)
 def schedule(String time, String nameOfFunction) {
-       //def _inputTime = time.split(':')
-       //Date date = new Date()        
-       //def _currentTime = date.format("HH:mm:ss").split(':')
+       /*def _inputTime = time.split(':')
+       Date date = new Date()  
+       def _currentTime = date.format("HH:mm:ss").split(':')
 
-       //Convert input time and current time to minutes
-       //def inputTime = Integer.parseInt(_inputTime[0])*3600+Integer.parseInt(_inputTime[1])*60
-       //def currentTime = Integer.parseInt(_currentTime[0])*3600+Integer.parseInt(_currentTime[1])*60+Integer.parseInt(_currentTime[2])
-       //def delay
+       Convert input time and current time to minutes
+       def inputTime = Integer.parseInt(_inputTime[0])*3600+Integer.parseInt(_inputTime[1])*60
+       def currentTime = Integer.parseInt(_currentTime[0])*3600+Integer.parseInt(_currentTime[1])*60+Integer.parseInt(_currentTime[2])
+       def delay
 
-       //if (inputTime < currentTime) {
-       //      delay = 24*60*60-inputTime+currentTime
-       //} else {
-       //      delay = inputTime-currentTime
-       //}
+       if (inputTime < currentTime) {
+               delay = 24*60*60-inputTime+currentTime
+       } else {
+               delay = inputTime-currentTime
+       }
        timersFuncList.add(nameOfFunction)
        timersList.add(new SimulatedTimer())
-       def task = timersList[timersFuncList.indexOf(nameOfFunction)].runAfter(/*delay*1000*0*/0) {
+       def task = timersList[timersFuncList.indexOf(nameOfFunction)].runAfter(delay*1000*0) {
                "$nameOfFunction"()
-       }
+       }*/
+       "$nameOfFunction"()
 }
 ////schedule(time, nameOfFunction as Closure)
 def schedule(String time, Closure nameOfFunction) {
-       //def _inputTime = time.split(':')
-       //Date date = new Date()        
-       //def _currentTime = date.format("HH:mm:ss").split(':')
+       /*def _inputTime = time.split(':')
+       Date date = new Date()  
+       def _currentTime = date.format("HH:mm:ss").split(':')
 
-       //Convert input time and current time to minutes
-       //def inputTime = Integer.parseInt(_inputTime[0])*3600+Integer.parseInt(_inputTime[1])*60
-       //def currentTime = Integer.parseInt(_currentTime[0])*3600+Integer.parseInt(_currentTime[1])*60+Integer.parseInt(_currentTime[2])
-       //def delay
+       Convert input time and current time to minutes
+       def inputTime = Integer.parseInt(_inputTime[0])*3600+Integer.parseInt(_inputTime[1])*60
+       def currentTime = Integer.parseInt(_currentTime[0])*3600+Integer.parseInt(_currentTime[1])*60+Integer.parseInt(_currentTime[2])
+       def delay
 
-       //if (inputTime < currentTime) {
-       //      delay = 24*60*60-inputTime+currentTime
-       //} else {
-       //      delay = inputTime-currentTime
-       //}
+       if (inputTime < currentTime) {
+               delay = 24*60*60-inputTime+currentTime
+       } else {
+               delay = inputTime-currentTime
+       }
 
        if (timersFuncList.contains(nameOfFunction)) {
                timersList[timersFuncList.indexOf(nameOfFunction)].cancel()
-               def task = timersList[timersFuncList.indexOf(nameOfFunction)].runAfter(/*delay*0*/0, nameOfFunction0)
+               def task = timersList[timersFuncList.indexOf(nameOfFunction)].runAfter(0, nameOfFunction)
        } else {
                timersFuncList.add(nameOfFunction)
                timersList.add(new SimulatedTimer())
-               def task = timersList[timersFuncList.indexOf(nameOfFunction)].runAfter(/*delay*0*/0, nameOfFunction)
-       }
+               def task = timersList[timersFuncList.indexOf(nameOfFunction)].runAfter(0, nameOfFunction)
+       }*/
+       nameOfFunction()
 }

diff --git a/Methods/unschedule.groovy b/Methods/unschedule.groovy
index 7f6ca1fdf920128f08737d042126e2675a6c810a..22ff9228c2076f687474babaeded680bb2a68f25 100644 (file)
--- a/Methods/unschedule.groovy
+++ b/Methods/unschedule.groovy
@@ -1,29 +1,29 @@
 /////////////////////////////////////////////////////////////////////
 ////unschedule(func)
 def unschedule(Closure functionToUnschedule) {
-       for (int i = 0;i < timersFuncList.size();i++) {
+       /*for (int i = 0;i < timersFuncList.size();i++) {
                if (timersFuncList[i] == functionToUnschedule) {
                        if (timersList != null)
                                timersList[i].cancel()
                }
-       }
+       }*/
 }
 
 def unschedule(String nameOfFunctionToUnschedule) {
-       for (int i = 0;i < timersFuncList.size();i++) {
+       /*for (int i = 0;i < timersFuncList.size();i++) {
                if (timersFuncList[i] instanceof String) {
                        if (timersFuncList[i] == nameOfFunctionToUnschedule) {
                                if (timersList != null)
                                        timersList[i].cancel()
                        }
                }
-       }
+       }*/
 }
 
 
 def unschedule() {
-       for (int i = 0;i < timersFuncList.size();i++) {
+       /*for (int i = 0;i < timersFuncList.size();i++) {
                if (timersList != null)
                        timersList[i].cancel()
-       }
+       }*/
 }

diff --git a/appLists/device-interaction/alarmsAppList b/appLists/device-interaction/alarmsAppList
index 89efabe89cdadf17c433b04c03dd7ccd00ad61ed..dfef01c9325008df2c78c3b9bba49c1fab70a296 100644 (file)
--- a/appLists/device-interaction/alarmsAppList
+++ b/appLists/device-interaction/alarmsAppList
@@ -1,10 +1,10 @@
-#forgiving-security.groovy
-#initial-state-event-streamer.groovy
+forgiving-security.groovy
+initial-state-event-streamer.groovy
 smart-alarm.groovy
-#smart-security.groovy
-#buffered-event-sender.groovy
-#DeviceTamperAlarm.groovy
-#FireCO2Alarm.groovy
-#initial-state-event-sender.groovy
-#initialstate-smart-app-v1.2.0.groovy
-#unbuffered-event-sender.groovy
+smart-security.groovy
+buffered-event-sender.groovy
+DeviceTamperAlarm.groovy
+FireCO2Alarm.groovy
+initial-state-event-sender.groovy
+initialstate-smart-app-v1.2.0.groovy
+unbuffered-event-sender.groovy

diff --git a/run.sh b/run.sh
index c2c9cfa0ad7deab40ea69bddf807bf880066c5e2..d77af37608a2679ba4ecc430cbca06b17162cb3f 100755 (executable)
--- a/run.sh
+++ b/run.sh
@@ -1,7 +1,8 @@
 #!/bin/bash
 
 # Device conflict
-python ModelCheck.py ../jpf-core/ ../logs/alarms/ ../smartapps/ appLists/device-interaction/alarmsAppList appLists/device-interaction/alarmsAppList2
+python ModelCheck.py ../jpf-core/ ../logs/thermostats/ ../smartapps/ appLists/device-interaction/thermostatsAppList appLists/device-interaction/thermostatsAppList2
+#python ModelCheck.py ../jpf-core/ ../logs/alarms/ ../smartapps/ appLists/device-interaction/alarmsAppList appLists/device-interaction/alarmsAppList2
 #python ModelCheck.py ../jpf-core/ ../logs/locks/ ../smartapps/ appLists/device-interaction/locksAppList appLists/device-interaction/locksAppList2
 #python ModelCheck.py ../jpf-core/ ../logs/musicPlayers/ ../smartapps/ appLists/device-interaction/musicPlayersAppList
 #python ModelCheck.py ../jpf-core/ ../logs/relaySwitch/ ../smartapps/ appLists/device-interaction/relaySwitchesAppList