+++ /dev/null
-//Infrastructure for SmartThings Application
-//Importing Libraries
-import groovy.transform.Field
-
-//Importing Classes
-///////////////////
-public class Touched{
- def sendEvent
- private int isTouched
-
- Touched(Closure sendEvent, int isTouched) {
- this.sendEvent = sendEvent
- this.isTouched = isTouched
- }
-
- //By Model Checker
- def setValue(LinkedHashMap eventDataMap) {
- println("The application is Touched!")
- this.isTouched = 1 //Do we need this?
- sendEvent(eventDataMap)
- }
-}
-///////////////////
-public class Contacting{
- private int deviceNumbers
- private List contacts
- def sendEvent
-
- Contacting(Closure sendEvent, int deviceNumbers) {
- this.sendEvent = sendEvent
- this.deviceNumbers = deviceNumbers
- this.contacts = []
- if (deviceNumbers == 1) {
- contacts = [new Contacts(0, "contact0", "closed", "closed")]
- } else if (deviceNumbers == 2) {
- contacts = [new Contacts(0, "contact0", "closed", "closed"), new Contacts(1, "contact1", "closed", "closed")]
- } else if (deviceNumbers == 3) {
- contacts = [new Contacts(0, "contact0", "closed", "closed"), new Contacts(1, "contact1", "closed", "closed")
- ,new Contacts(2, "contact2", "closed", "closed")]
- }
- }
-
- //By Model Checker
- def setValue(LinkedHashMap eventDataMap) {
- contacts[eventDataMap["deviceId"]].setValue(eventDataMap["value"])
- sendEvent(eventDataMap)
- }
-
- def currentValue(String deviceFeature) {
- if (deviceNumbers == 1)
- contacts[0].currentValue(deviceFeature)//It is called if we have only one device
- else
- contacts*.currentValue(deviceFeature)
- }
-
- def latestValue(String deviceFeature) {
- if (deviceNumbers == 1)
- contacts[0].latestValue(deviceFeature)//It is called if we have only one device
- else
- contacts*.latestValue(deviceFeature)
- }
-
- def getAt(int ix) {
- contacts[ix]
- }
-}
-///////////////////
-public class Contacts {
- private int id
- private String displayName
- private String contactCurrentValue
- private String contactLatestValue
-
- Contacts(int id, String displayName, String contactCurrentValue, String contactLatestValue) {
- this.id = id
- this.displayName = displayName
- this.contactCurrentValue = contactCurrentValue
- this.contactLatestValue = contactLatestValue
- }
-
- def setValue(String value) {
- this.contactLatestValue = contactCurrentValue
- println("the contact sensor with id:$id is triggered to $value!")
- this.contactCurrentValue = value
- }
-
- def currentValue(String deviceFeature) {
- if (deviceFeature == "contact") {
- return contactCurrentValue
- }
- }
-
- def latestValue(String deviceFeature) {
- if (deviceFeature == "contact") {
- return contactLatestValue
- }
- }
-}
-///////////////////
-public class Event {
- private int deviceId
- private String value
- private String linkText
- private String displayName
- private boolean displayed
- private String name
- private String descriptionText
- private boolean isStateChange
- private String unit
- private LinkedHashMap data
-
- Event() {
- this.deviceId = 0
- this.linkText = ""
- this.value = ""
- this.displayName = ""
- this.name = ""
- this.descriptionText = ""
- this.isStateChange = false
- this.unit = ""
- this.data = []
- this.displayed = false
- }
-}
-///////////////////
-class LocationVar {
- private int contactBookEnabled
- private String modes
- private String mode
- private List contacts
- private List phoneNumbers
-
- private Phrase helloHome
-
- LocationVar() {
- this.modes = "'home', 'away', 'night'"
- this.mode = "home"
- this.helloHome = new Phrase()
- this.contactBookEnabled = 1
- this.contacts = ['AJ']
- this.phoneNumbers = [9495379373]
- }
-}
-///////////////////
-class Phrase {
- private LinkedHashMap phrases
-
- Phrase() {
- this.phrases = [id:0, label:"Good Morning!"]
- }
- def getPhrases() {
- return this.phrases
- }
-}
-///////////////////
-public class Locking{
- int deviceNumbers
- List locks
- def sendEvent
- def timers
-
- Locking(Closure sendEvent, int deviceNumbers) {
- this.sendEvent = sendEvent
- this.timers = new Timer()
- this.deviceNumbers = deviceNumbers
- this.locks = []
- if (deviceNumbers == 1) {
- locks = [new Locks(sendEvent, 0, "lock0", "locked", "locked")]
- } else if (deviceNumbers == 2) {
- locks = [new Locks(sendEvent, 0, "lock0", "locked", "locked"), new Locks(sendEvent, 1, "lock1", "locked", "locked")]
- } else if (deviceNumbers == 3) {
- locks = [new Locks(sendEvent, 0, "lock0", "locked", "locked"), new Locks(sendEvent, 1, "lock1", "locked", "locked")
- ,new Locks(sendEvent, 2, "lock2", "locked", "locked")]
- }
- }
-
- //By Apps
- def lock() {
- locks*.lock()
- }
-
- def lock(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- locks*.lock()
- }
- }
-
- def unlock() {
- locks*.unlock()
- }
-
- def unlock(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- locks*.unlock()
- }
- }
-
- //By Model Checker
- def setValue(LinkedHashMap eventDataMap) {
- locks[eventDataMap["deviceId"]].setValue(eventDataMap["value"])
- sendEvent(eventDataMap)
- }
-
- def currentValue(String deviceFeature) {
- if (deviceNumbers == 1)
- locks[0].currentValue(deviceFeature)
- else
- locks*.currentValue(deviceFeature)
- }
-
- def latestValue(String deviceFeature) {
- if (deviceNumbers == 1)
- locks[0].latestValue(deviceFeature)
- else
- locks*.latestValue(deviceFeature)
- }
-
- def getAt(int ix) {
- locks[ix]
- }
-}
-///////////////////
-public class Locks {
- private int id
- private String displayName
- private String lockCurrentValue
- private String lockLatestValue
- def sendEvent
- def timers
-
-
- Locks(Closure sendEvent, int id, String displayName, String lockCurrentValue, String lockLatestValue) {
- this.id = id
- this.sendEvent = sendEvent
- this.displayName = displayName
- this.lockCurrentValue = lockCurrentValue
- this.lockLatestValue = lockLatestValue
- this.timers = new Timer()
- }
-
- //By Apps
- def lock() {
- println("the door with id:$id is locked!")
- this.lockLatestValue = this.lockCurrentValue
- this.lockCurrentValue = "locked"
- sendEvent([name: "lock", value: "locked", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
-
- def lock(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- println("the door with id:$id is locked!")
- this.lockLatestValue = this.lockCurrentValue
- this.lockCurrentValue = "locked"
- sendEvent([name: "lock", value: "locked", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
- }
-
- def unlock() {
- println("the door with id:$id is unlocked!")
- this.lockLatestValue = this.lockCurrentValue
- this.lockCurrentValue = "unlocked"
- sendEvent([name: "unlock", value: "unlocked", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
-
- def unlock(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- println("the door with id:$id is locked!")
- this.lockLatestValue = this.lockCurrentValue
- this.lockCurrentValue = "locked"
- sendEvent([name: "unlock", value: "unlocked", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
- }
-
- //By Model Checker
- def setValue(String value) {
- println("the door with id:$id is $value!")
- this.lockLatestValue = this.lockCurrentValue
- this.lockCurrentValue = value
- }
-
- def currentValue(String deviceFeature) {
- if (deviceFeature == "lock") {
- return lockCurrentValue
- }
- }
-
- def latestValue(String deviceFeature) {
- if (deviceFeature == "lock") {
- return lockLatestValue
- }
- }
-}
-///////////////////
-class Logger {
- private boolean printToConsole = true
-
- def methodMissing(String name, args) {
- def messsage = args[0]
- if (printToConsole) {
- println messsage
- }
- }
-}
-///////////////////
-public class Switches {
- private int id = 0
- private String displayName
- private String switchCurrentValue
- private String switchLatestValue
- def sendEvent
- def timers
-
-
- Switches(Closure sendEvent, int id, String displayName, String switchCurrentValue, String switchLatestValue) {
- this.sendEvent = sendEvent
- this.timers = new Timer()
-
- this.id = id
- this.displayName = displayName
- this.switchCurrentValue = switchCurrentValue
- this.switchLatestValue = switchLatestValue
- }
-
- //By Apps
- def on() {
- println("the switch with id:$id is on!")
- this.switchLatestValue = this.switchCurrentValue
- this.switchCurrentValue = "on"
- sendEvent([name: "switch", value: "on", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
-
- def on(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- println("the switch with id:$id is on!")
- this.switchLatestValue = this.switchCurrentValue
- this.switchCurrentValue = "on"
- sendEvent([name: "switch", value: "on", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
- }
-
- def off() {
- println("the switch with id:$id is off!")
- this.switchLatestValue = this.switchCurrentValue
- this.switchCurrentValue = "off"
- sendEvent([name: "switch", value: "off", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
-
- def off(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- println("the switch with id:$id is off!")
- this.switchLatestValue = this.switchCurrentValue
- this.switchCurrentValue = "off"
- sendEvent([name: "switch", value: "off", deviceId: this.id, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
- }
- }
-
- //By Model Checker
- def setValue(String value) {
- println("the switch with id:$id is $value!")
- this.switchLatestValue = this.switchCurrentValue
- this.switchCurrentValue = value
- }
-
- def currentValue(String deviceFeature) {
- if (deviceFeature == "switch") {
- return switchCurrentValue
- }
- }
-
- def latestValue(String deviceFeature) {
- if (deviceFeature == "switch") {
- return switchLatestValue
- }
- }
-}
-///////////////////
-public class Switching{
- int deviceNumbers
- List switches
- def timers
- def sendEvent
-
- Switching(Closure sendEvent, int deviceNumbers) {
- this.sendEvent = sendEvent
- this.timers = new Timer()
- this.deviceNumbers = deviceNumbers
- this.switches = []
- if (deviceNumbers == 1) {
- switches = [new Switches(sendEvent, 0, "switch0", "off", "off")]
- } else if (deviceNumbers == 2) {
- switches = [new Switches(sendEvent, 0, "switch0", "off", "off"), new Switches(sendEvent, 1, "switch1", "off", "off")]
- } else if (deviceNumbers == 3) {
- switches = [new Switches(sendEvent, 0, "switch0", "off", "off"), new Switches(sendEvent, 1, "switch1", "off", "off")
- ,new Switches(sendEvent, 2, "switch2", "off", "off")]
- }
- }
-
- //By Apps
- def on() {
- switches*.on()
- }
-
- def on(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- switches*.on()
- }
- }
-
- def off() {
- switches*.off()
- }
-
- def off(LinkedHashMap metaData) {
- def task = timers.runAfter(metaData["delay"]) {
- switches*.off()
- }
- }
-
- //By Model Checker
- def setValue(LinkedHashMap eventDataMap) {
- switches[eventDataMap["deviceId"]].setValue(eventDataMap["value"])
- sendEvent(eventDataMap)
- }
-
-
- def currentValue(String deviceFeature) {
- if (deviceNumbers == 1)
- switches[0].currentValue(deviceFeature)
- else
- switches*.currentValue(deviceFeature)
- }
-
- def latestValue(String deviceFeature) {
- if (deviceNumbers == 1)
- switches[0].latestValue(deviceFeature)
- else
- switches*.latestValue(deviceFeature)
- }
-
- def getAt(int ix) {
- switches[ix]
- }
-}
-
-//Global variable for sendEvent
-@Field def sendEvent = {eventDataMap ->
- app1.eventHandler(eventDataMap)
- app2.eventHandler(eventDataMap)
- }
-
-//Objects for classes
-//Object for class switch!
-@Field def switchObject = new Switching(sendEvent, 1)//not ok
-//Object for class lock!
-@Field def lockObject = new Locking(sendEvent, 2)//not ok
-//Object for location
-@Field def locationObject = new LocationVar()//not ok
-//Object for touch
-@Field def appObject = new Touched(sendEvent, 0)//not ok
-//Object for contact sensor
-@Field def contactObject = new Contacting(sendEvent, 1)//not ok
-
-
-//Application #1
-class App1 {
- def reference
-
- //extracted objs
- def location
- //Object for class Touched!
- def app
- //Object for class switch!
- def switchesoff
- //Object for class switch!
- def switcheson
- //Object for class lock!
- def lock1
- //Variable for mode!
- def newMode = "away"
- //Variable for number!
- def waitfor = 10
- //Global Object for functions in subscribe method!
- def installed = this.&installed
- //Global Object for functions in subscribe method!
- def updated = this.&updated
- //Global Object for functions in subscribe method!
- def appTouch = this.&appTouch
-
- App1(Object obj) {
- reference = obj
- location = obj.locationObject
- app = obj.appObject
- //should be created in python
- switchesoff = obj.switchObject
- switcheson = obj.switchObject
- lock1 = obj.lockObject
- }
- //GlobalVariables
- //Settings variable defined to settings on purpose
- def settings = "Settings"
- //Global variable for state[mode]
- def state = [home:[],away:[],night:[]]
- //Create a global logger object for methods
- def log = new Logger()
- //Create a global variable for Functions in Subscribe method
- def functionList = []
- //Create a global variable for Objects in Subscribe method
- 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 list for events
- def evt = []
-
-
-
-
-
- //Methods
- /////////////////////////////////////////////////////////////////////
- def definition(LinkedHashMap metaData) {
- println("IGNORE -- JUST SOME DEFINITION")
- }
-
- /////////////////////////////////////////////////////////////////////
- def preferences(Closure metaData) {
- println("IGNORE -- JUST SOME DEFINITION")
- }
- /////////////////////////////////////////////////////////////////////
- def setLocationMode(String mode) {
- location.mode = mode
- }
-
- /////////////////////////////////////////////////////////////////////
- ////subscribe(obj, func)
- def subscribe(Object obj, Closure FunctionToCall) {
- objectList.add(obj)
- eventList.add("Touched")
- functionList.add(FunctionToCall)
- }
- ////subscribe(obj, event, func)
- def subscribe(Object obj, String event, Closure FunctionToCall) {
- objectList.add(obj)
- eventList.add(event)
- functionList.add(FunctionToCall)
- }
- ////subscribe(obj, event, func, data)
- def subscribe(Object obj, String event, Closure FunctionToCall, LinkedHashMap metaData) {
- objectList.add(obj)
- eventList.add(event)
- functionList.add(FunctionToCall)
- }
-
- /////////////////////////////////////////////////////////////////////
- ////runIn(time, func)
- def runIn(int seconds, Closure functionToCall) {
- timersFuncList.add(functionToCall)
- timersList.add(new Timer())
- def task = timersList[-1].runAfter(1000*seconds, functionToCall)
- }
- /////////////////////////////////////////////////////////////////////
- ////unschedule(func)
- def unschedule(Closure functionToUnschedule) {
- for (int i = 0;i < timersFuncList.size();i++) {
- if (timersFuncList[i] == functionToUnschedule) {
- timersList[i].cancel()
- }
- }
- }
- /////////////////////////////////////////////////////////////////////
- ////sendNotificationToContacts(text, recipients)
- def sendNotificationToContacts(String text, List recipients) {
- for (int i = 0;i < recipients.size();i++) {
- for (int j = 0;j < location.contacts.size();j++) {
- if (recipients[i] == location.contacts[j]) {
- println("Sending \""+text+"\" to "+location.phoneNumbers[j].toString())
- }
- }
- }
- }
- /////////////////////////////////////////////////////////////////////
- ////sendSms(phone, text)
- def sendSms(long phoneNumber, String text) {
- println("Sending \""+text+"\" to "+phoneNumber.toString())
- }
- /////////////////////////////////////////////////////////////////////
- def eventHandler(LinkedHashMap eventDataMap) {
- def value = eventDataMap["value"]
- def name = eventDataMap["name"]
- def deviceId = eventDataMap["deviceId"]
- def descriptionText = eventDataMap["descriptionText"]
- def displayed = eventDataMap["displayed"]
- def linkText = eventDataMap["linkText"]
- def isStateChange = eventDataMap["isStateChange"]
- def unit = eventDataMap["unit"]
- def data = eventDataMap["data"]
-
- for (int i = 0;i < eventList.size();i++) {
- if (eventList[i] == name) {
- evt.add(new Event())
- evt[-1].value = value
- evt[-1].name = name
- evt[-1].deviceId = deviceId
- evt[-1].descriptionText = descriptionText
- evt[-1].displayed = displayed
- evt[-1].linkText = linkText
- evt[-1].displayName = linkText
- evt[-1].isStateChange = isStateChange
- evt[-1].unit = unit
- evt[-1].data = data
- functionList[i](evt[-1])
- }
- }
- }
-
- def installed()
- {
- log.debug "Installed with settings: ${settings}"
- log.debug "Current mode = ${location.mode}"
- subscribe(app, appTouch)
- }
-
-
- def updated()
- {
- log.debug "Updated with settings: ${settings}"
- log.debug "Current mode = ${location.mode}"
- unsubscribe()
- subscribe(app, appTouch)
- }
-
- def appTouch(evt) {
- log.debug "changeMode, location.mode = $location.mode, newMode = $newMode, location.modes = $location.modes"
- //int i = Verify.getInt(0,2);
- //list = ['home', 'away', 'night']
- //location.mode = list[i]
- if (location.mode != newMode) {
- setLocationMode(newMode)
- log.debug "Changed the mode to '${newMode}'"
- } else {
- log.debug "New mode is the same as the old mode, leaving it be"
- }
- log.debug "appTouch: $evt"
- lock1.unlock()
- switcheson.on()
- def delay = (waitfor != null && waitfor != "") ? waitfor * 1000 : 120000
- switchesoff.off(delay: delay)
- }
-
-
-}
-
-
-
-//Application #2
-class App2 {
- def reference
-
- //extractedObjects
- //extracted objs
- def location
- //Object for class Touched!
- def app
- //Global Object for class lock!
- def lock1
- //Global Object for class contactSensor!
- def contact
- //Global variable for number!
- def minutesLater = 1
- //Global variable for number!
- def secondsLater = 10
- //Global variable for recipients!
- def recipients = ['AJ']
- //Global variable for phone number!
- def phoneNumber = 9495379373
- //Global Object for functions in subscribe method!
- def installed = this.&installed
- //Global Object for functions in subscribe method!
- def updated = this.&updated
- //Global Object for functions in subscribe method!
- def initialize = this.&initialize
- //Global Object for functions in subscribe method!
- def lockDoor = this.&lockDoor
- //Global Object for functions in subscribe method!
- def unlockDoor = this.&unlockDoor
- //Global Object for functions in subscribe method!
- def doorHandler = this.&doorHandler
-
-
- App2(Object obj) {
- reference = obj
- location = obj.locationObject
- app = obj.appObject
- //should be created in python
- contact = obj.contactObject
- lock1 = obj.lockObject
- }
- //GlobalVariables
- //Settings variable defined to settings on purpose
- def settings = "Settings"
- //Global variable for state[mode]
- def state = [home:[],away:[],night:[]]
- //Create a global logger object for methods
- def log = new Logger()
- //Create a global variable for Functions in Subscribe method
- def functionList = []
- //Create a global variable for Objects in Subscribe method
- 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 list for events
- def evt = []
-
-
-
-
-
- //Methods
- /////////////////////////////////////////////////////////////////////
- def definition(LinkedHashMap metaData) {
- println("IGNORE -- JUST SOME DEFINITION")
- }
-
- /////////////////////////////////////////////////////////////////////
- def preferences(Closure metaData) {
- println("IGNORE -- JUST SOME DEFINITION")
- }
- /////////////////////////////////////////////////////////////////////
- def setLocationMode(String mode) {
- location.mode = mode
- }
-
- /////////////////////////////////////////////////////////////////////
- ////subscribe(obj, func)
- def subscribe(Object obj, Closure FunctionToCall) {
- objectList.add(obj)
- eventList.add("Touched")
- functionList.add(FunctionToCall)
- }
- ////subscribe(obj, event, func)
- def subscribe(Object obj, String event, Closure FunctionToCall) {
- objectList.add(obj)
- eventList.add(event)
- functionList.add(FunctionToCall)
- }
- ////subscribe(obj, event, func, data)
- def subscribe(Object obj, String event, Closure FunctionToCall, LinkedHashMap metaData) {
- objectList.add(obj)
- eventList.add(event)
- functionList.add(FunctionToCall)
- }
-
- /////////////////////////////////////////////////////////////////////
- ////runIn(time, func)
- def runIn(int seconds, Closure functionToCall) {
- timersFuncList.add(functionToCall)
- timersList.add(new Timer())
- def task = timersList[-1].runAfter(1000*seconds, functionToCall)
- }
- /////////////////////////////////////////////////////////////////////
- ////unschedule(func)
- def unschedule(Closure functionToUnschedule) {
- for (int i = 0;i < timersFuncList.size();i++) {
- if (timersFuncList[i] == functionToUnschedule) {
- timersList[i].cancel()
- }
- }
- }
- /////////////////////////////////////////////////////////////////////
- ////sendNotificationToContacts(text, recipients)
- def sendNotificationToContacts(String text, List recipients) {
- for (int i = 0;i < recipients.size();i++) {
- for (int j = 0;j < location.contacts.size();j++) {
- if (recipients[i] == location.contacts[j]) {
- println("Sending \""+text+"\" to "+location.phoneNumbers[j].toString())
- }
- }
- }
- }
- /////////////////////////////////////////////////////////////////////
- ////sendSms(phone, text)
- def sendSms(long phoneNumber, String text) {
- println("Sending \""+text+"\" to "+phoneNumber.toString())
- }
- /////////////////////////////////////////////////////////////////////
- def eventHandler(LinkedHashMap eventDataMap) {
- def value = eventDataMap["value"]
- def name = eventDataMap["name"]
- def deviceId = eventDataMap["deviceId"]
- def descriptionText = eventDataMap["descriptionText"]
- def displayed = eventDataMap["displayed"]
- def linkText = eventDataMap["linkText"]
- def isStateChange = eventDataMap["isStateChange"]
- def unit = eventDataMap["unit"]
- def data = eventDataMap["data"]
-
- for (int i = 0;i < eventList.size();i++) {
- if (eventList[i] == name) {
- println eventList[i]
- evt.add(new Event())
- evt[-1].value = value
- evt[-1].name = name
- evt[-1].deviceId = deviceId
- evt[-1].descriptionText = descriptionText
- evt[-1].displayed = displayed
- evt[-1].linkText = linkText
- evt[-1].displayName = linkText
- evt[-1].isStateChange = isStateChange
- evt[-1].unit = unit
- evt[-1].data = data
- functionList[i](evt[-1])
- }
- }
- }
-
- def installed(){
- initialize()
- }
-
- def updated(){
- unsubscribe()
- unschedule()
- initialize()
- }
-
- def initialize(){
- log.debug "Settings: ${settings}"
- subscribe(lock1, "lock", doorHandler, [filterEvents: false])
- subscribe(lock1, "unlock", doorHandler, [filterEvents: false])
- subscribe(contact, "contact.open", doorHandler)
- subscribe(contact, "contact.closed", doorHandler)
- }
-
- def lockDoor(){
- log.debug "Locking the door."
- lock1.lock()
- if(location.contactBookEnabled) {
- if ( recipients ) {
- log.debug ( "Sending Push Notification..." )
- sendNotificationToContacts( "${lock1} locked after ${contact} was closed for ${minutesLater} minutes!", recipients)
- }
- }
- if (phoneNumber) {
- log.debug("Sending text message...")
- sendSms( phoneNumber, "${lock1} locked after ${contact} was closed for ${minutesLater} minutes!")
- }
- }
-
- def unlockDoor(){
- log.debug "Unlocking the door."
- lock1.unlock()
- if(location.contactBookEnabled) {
- if ( recipients ) {
- log.debug ( "Sending Push Notification..." )
- sendNotificationToContacts( "${lock1} unlocked after ${contact} was opened for ${secondsLater} seconds!", recipients)
- }
- }
- if ( phoneNumber ) {
- log.debug("Sending text message...")
- sendSms( phoneNumber, "${lock1} unlocked after ${contact} was opened for ${secondsLater} seconds!")
- }
- }
-
- def doorHandler(evt){
- if ((contact.latestValue("contact") == "open") && (evt.value == "locked")) { // If the door is open and a person locks the door then...
- //def delay = (secondsLater) // runIn uses seconds
- runIn( secondsLater, unlockDoor ) // ...schedule (in minutes) to unlock... We don't want the door to be closed while the lock is engaged.
- println(1)
- }
- else if ((contact.latestValue("contact") == "open") && (evt.value == "unlocked")) { // If the door is open and a person unlocks it then...
- unschedule( unlockDoor ) // ...we don't need to unlock it later.
- println(2)
- }
- else if ((contact.latestValue("contact") == "closed") && (evt.value == "locked")) { // If the door is closed and a person manually locks it then...
- unschedule( lockDoor ) // ...we don't need to lock it later.
- println(3)
- }
- else if ((contact.latestValue("contact") == "closed") && (evt.value == "unlocked")) { // If the door is closed and a person unlocks it then...
- //def delay = (minutesLater * 60) // runIn uses seconds
- runIn( (minutesLater * 2), lockDoor )
- //runIn( (minutesLater * 60), lockDoor ) // ...schedule (in minutes) to lock.
- println(4)
- }
- else if ((lock1.latestValue("lock") == "unlocked") && (evt.value == "open")) { // If a person opens an unlocked door...
- unschedule( lockDoor ) // ...we don't need to lock it later.
- println(5)
- }
- else if ((lock1.latestValue("lock") == "unlocked") && (evt.value == "closed")) { // If a person closes an unlocked door...
- //def delay = (minutesLater * 60) // runIn uses seconds
- runIn( (minutesLater * 60), lockDoor ) // ...schedule (in minutes) to lock.
- println(6)
- }
- else { //Opening or Closing door when locked (in case you have a handle lock)
- log.debug "Unlocking the door."
- lock1.unlock()
- println(7)
- if(location.contactBookEnabled) {
- if ( recipients ) {
- log.debug ( "Sending Push Notification..." )
- sendNotificationToContacts( "${lock1} unlocked after ${contact} was opened or closed when ${lock1} was locked!", recipients)
- }
- }
- if ( phoneNumber ) {
- log.debug("Sending text message...")
- sendSms( phoneNumber, "${lock1} unlocked after ${contact} was opened or closed when ${lock1} was locked!")
- }
- }
- }
-}
-
-
-@Field def app1 = new App1(this)
-@Field def app2 = new App2(this)
-app1.installed()
-app2.installed()
-appObject.setValue([name: "Touched", value: "Touched", deviceId: 0, descriptionText: "",
- displayed: true, linkText: "", isStateChange: false, unit: "", data: []])
-
--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package gov.nasa.jpf.listener;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.jvm.bytecode.*;
+import gov.nasa.jpf.vm.*;
+import gov.nasa.jpf.vm.bytecode.WriteInstruction;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+
+// TODO: Fix for Groovy's model-checking
+// TODO: This is a listener created to detect device conflicts and global variable conflicts
+/**
+ * Simple listener tool to track conflicts between 2 apps.
+ * A conflict is defined as one app trying to change the state of a variable
+ * into its opposite value after being set by the other app,
+ * e.g., app1 attempts to change variable A to false after A has been set by app2 to true earlier.
+ */
+public class VariableConflictTracker extends ListenerAdapter {
+
+ private final HashMap<String, VarChange> executionMap = new HashMap<>();
+ private final HashSet<String> conflictSet = new HashSet<>();
+ private final HashSet<String> appSet = new HashSet<>();
+
+ public VariableConflictTracker(Config config) {
+ String[] conflictVars = config.getStringArray("variables");
+ for(String var : conflictVars) {
+ conflictSet.add(var);
+ }
+ String[] apps = config.getStringArray("apps");
+ for(String var : apps) {
+ appSet.add(var);
+ }
+ }
+
+ @Override
+ public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+ String varId = "";
+
+ if (executedInsn instanceof WriteInstruction){
+
+ varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+ for(String var : conflictSet) {
+
+ if (varId.contains(var)) {
+ // Get variable info
+ byte type = getType(ti, executedInsn);
+ String value = getValue(ti, executedInsn, type);
+ String writer = getWriter(ti.getStack());
+ // Just return if the writer is not one of the listed apps in the .jpf file
+ if (writer == null)
+ return;
+
+ if (executionMap.containsKey(var)) {
+ // Subsequent accesses to the variable
+ VarChange current = executionMap.get(var);
+ if (current.writer != writer) {
+ // Conflict is declared when:
+ // 1) Current writer != previous writer, e.g., App1 vs. App2
+ // 2) Current value != previous value, e.g., "locked" vs. "unlocked"
+ if (!current.value.equals(value)) {
+
+ String msg = "Conflict between apps " + current.writer + " and " +
+ writer + " for variable " + var;
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", msg);
+ ti.setNextPC(nextIns);
+ }
+ } else {
+ // No conflict is declared if this variable is accessed subsequently by the same writer
+ current.writer = writer;
+ current.value = value;
+ }
+ } else {
+ // First access to the variable
+ VarChange change = new VarChange(writer, value);
+ executionMap.put(var, change);
+ }
+ }
+ }
+ }
+ }
+
+ class VarChange {
+ String writer;
+ String value;
+
+ VarChange(String writer, String value) {
+ this.writer = writer;
+ this.value = value;
+ }
+ }
+
+ // Find the variable writer
+ // It should be one of the apps listed in the .jpf file
+ private String getWriter(List<StackFrame> sfList) {
+
+ for(StackFrame sf : sfList) {
+ MethodInfo mi = sf.getMethodInfo();
+ if(!mi.isJPFInternal()) {
+ String method = mi.getStackTraceName();
+ // Check against the apps in the appSet
+ for(String app : appSet) {
+ if (method.contains(app)) {
+ return app;
+ }
+ }
+ }
+ }
+
+ return null;
+ }
+
+ private byte getType(ThreadInfo ti, Instruction inst) {
+ StackFrame frame;
+ FieldInfo fi;
+ String type;
+
+ frame = ti.getTopFrame();
+ if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
+ return (Types.T_REFERENCE);
+ }
+
+ type = null;
+
+ if (inst instanceof JVMLocalVariableInstruction) {
+ type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
+ } else if (inst instanceof JVMFieldInstruction){
+ fi = ((JVMFieldInstruction) inst).getFieldInfo();
+ type = fi.getType();
+ }
+
+ if (inst instanceof JVMArrayElementInstruction) {
+ return (getTypeFromInstruction(inst));
+ }
+
+ if (type == null) {
+ return (Types.T_VOID);
+ }
+
+ return (decodeType(type));
+ }
+
+ private final static byte getTypeFromInstruction(Instruction inst) {
+ if (inst instanceof JVMArrayElementInstruction)
+ return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
+
+ return(Types.T_VOID);
+ }
+
+ private final static byte getTypeFromInstruction(JVMArrayElementInstruction inst) {
+ String name;
+
+ name = inst.getClass().getName();
+ name = name.substring(name.lastIndexOf('.') + 1);
+
+ switch (name.charAt(0)) {
+ case 'A': return(Types.T_REFERENCE);
+ case 'B': return(Types.T_BYTE); // Could be a boolean but it is better to assume a byte.
+ case 'C': return(Types.T_CHAR);
+ case 'F': return(Types.T_FLOAT);
+ case 'I': return(Types.T_INT);
+ case 'S': return(Types.T_SHORT);
+ case 'D': return(Types.T_DOUBLE);
+ case 'L': return(Types.T_LONG);
+ }
+
+ return(Types.T_VOID);
+ }
+
+ private final static String encodeType(byte type) {
+ switch (type) {
+ case Types.T_BYTE: return("B");
+ case Types.T_CHAR: return("C");
+ case Types.T_DOUBLE: return("D");
+ case Types.T_FLOAT: return("F");
+ case Types.T_INT: return("I");
+ case Types.T_LONG: return("J");
+ case Types.T_REFERENCE: return("L");
+ case Types.T_SHORT: return("S");
+ case Types.T_VOID: return("V");
+ case Types.T_BOOLEAN: return("Z");
+ case Types.T_ARRAY: return("[");
+ }
+
+ return("?");
+ }
+
+ private final static byte decodeType(String type) {
+ if (type.charAt(0) == '?'){
+ return(Types.T_REFERENCE);
+ } else {
+ return Types.getBuiltinType(type);
+ }
+ }
+
+ private String getValue(ThreadInfo ti, Instruction inst, byte type) {
+ StackFrame frame;
+ int lo, hi;
+
+ frame = ti.getTopFrame();
+
+ if ((inst instanceof JVMLocalVariableInstruction) ||
+ (inst instanceof JVMFieldInstruction))
+ {
+ if (frame.getTopPos() < 0)
+ return(null);
+
+ lo = frame.peek();
+ hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
+
+ return(decodeValue(type, lo, hi));
+ }
+
+ return(null);
+ }
+
+ private final static String decodeValue(byte type, int lo, int hi) {
+ switch (type) {
+ case Types.T_ARRAY: return(null);
+ case Types.T_VOID: return(null);
+
+ case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
+ case Types.T_BYTE: return(String.valueOf(lo));
+ case Types.T_CHAR: return(String.valueOf((char) lo));
+ case Types.T_DOUBLE: return(String.valueOf(Types.intsToDouble(lo, hi)));
+ case Types.T_FLOAT: return(String.valueOf(Types.intToFloat(lo)));
+ case Types.T_INT: return(String.valueOf(lo));
+ case Types.T_LONG: return(String.valueOf(Types.intsToLong(lo, hi)));
+ case Types.T_SHORT: return(String.valueOf(lo));
+
+ case Types.T_REFERENCE:
+ ElementInfo ei = VM.getVM().getHeap().get(lo);
+ if (ei == null)
+ return(null);
+
+ ClassInfo ci = ei.getClassInfo();
+ if (ci == null)
+ return(null);
+
+ if (ci.getName().equals("java.lang.String"))
+ return('"' + ei.asString() + '"');
+
+ return(ei.toString());
+
+ default:
+ System.err.println("Unknown type: " + type);
+ return(null);
+ }
+ }
+}