From: amiraj Date: Thu, 8 Aug 2019 20:47:30 +0000 (-0700) Subject: Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/smartthings-infrastructure X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=22b95e00013e33aa669f7430cb25153f0b1192e2;hp=f04c0d554014884a077470b372be0e0c7d3398fe;p=smartthings-infrastructure.git Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/smartthings-infrastructure --- diff --git a/Extractor/Extractor.groovy b/Extractor/Extractor.groovy index 16038e3..b5f3194 100644 --- a/Extractor/Extractor.groovy +++ b/Extractor/Extractor.groovy @@ -81,7 +81,7 @@ import Momentary.Momentaries import Timer.SimulatedTimer //GlobalVariables -@Field def location = new LocationVar() +@Field def location = new LocationVar({}, true) //Settings variable defined to settings on purpose @Field def settings = [app: "app"] //Global variable for state[mode] @@ -101,15 +101,17 @@ import Timer.SimulatedTimer @Field File extractedObjectsConstructorApp1 = new File("Extractor/App1/extractedObjectsConstructorApp1.groovy") @Field File extractedObjectsConstructorApp2 = new File("Extractor/App2/extractedObjectsConstructorApp2.groovy") - +@Field chooseMode = 0 //Empty the files if (App == "App1") { globalObjects.write("") extractedObjectsApp1.write("") extractedObjectsConstructorApp1.write("") + chooseMode = 0 } else if (App == "App2") { extractedObjectsApp2.write("") extractedObjectsConstructorApp2.write("") + chooseMode = 1 } @@ -1639,7 +1641,13 @@ def input(LinkedHashMap metaData) { case "mode": //def randomVariable = Math.abs(new Random().nextInt() % 3) def modes = ["away", "home", "night"] - def userInput = modes[1] + // Always assign a different mode to each app + //def userInput = modes[1] + def userInput = modes[chooseMode] + if (chooseMode < 3) + chooseMode++; + else + chooseMode = chooseMode%3 if (modeVariables == 0) { mode0 = metaData['name'] @@ -2105,7 +2113,7 @@ def preferences(Closure inputData) { GlobalVariablesBothApps.write("") GlobalVariablesBothApps.append("//Creating Global variables for both apps\n") GlobalVariablesBothApps.append("@Field def sendEvent = {eventDataMap -> eventHandler(eventDataMap)}\n") - GlobalVariablesBothApps.append("@Field def locationObject = new LocationVar(sendEvent)\n") + GlobalVariablesBothApps.append("@Field def locationObject = new LocationVar(sendEvent, init)\n") GlobalVariablesBothApps.append("@Field def appObject = new Touched(sendEvent, 0)\n") globalObjects.withReader { reader -> diff --git a/Location/LocationVar.groovy b/Location/LocationVar.groovy index 3f28a0b..a114c1f 100644 --- a/Location/LocationVar.groovy +++ b/Location/LocationVar.groovy @@ -15,18 +15,34 @@ class LocationVar { private Phrase helloHome - LocationVar(Closure sendEvent) { - this.hubs = [[id:0, localIP:"128.195.204.105"]] - this.modes = [[name: "home"],[name: "away"],[name: "night"]] - this.mode = "home" - this.helloHome = new Phrase() - this.contactBookEnabled = 1 - this.contacts = ['AJ'] - this.phoneNumbers = [9495379373] - this.sendEvent = sendEvent - this.timeZone = TimeZone.getTimeZone("America/New_York") - this.name = "hub0" - this.temperatureScale = "F" + LocationVar(Closure sendEvent, boolean init) { + + if (init) { + this.hubs = [[id:0, localIP:"128.195.204.105"]] + this.modes = [[name: "home"],[name: "away"],[name: "night"]] + this.mode = "away" + this.helloHome = new Phrase() + this.contactBookEnabled = 1 + this.contacts = ['AJ'] + this.phoneNumbers = [9495379373] + this.sendEvent = sendEvent + this.timeZone = TimeZone.getTimeZone("America/New_York") + this.name = "hub0" + this.temperatureScale = "F" + } else { + this.hubs = [[id:0, localIP:"128.195.204.105"]] + this.modes = [[name: "home"],[name: "away"],[name: "night"]] + this.mode = "home" + this.helloHome = new Phrase() + this.contactBookEnabled = 1 + this.contacts = ['AJ'] + this.phoneNumbers = [9495379373] + this.sendEvent = sendEvent + this.timeZone = TimeZone.getTimeZone("America/New_York") + this.name = "hub0" + this.temperatureScale = "F" + + } } //By Model Checker diff --git a/Methods/setLocationMode.groovy b/Methods/setLocationMode.groovy index aa7424b..12433ab 100644 --- a/Methods/setLocationMode.groovy +++ b/Methods/setLocationMode.groovy @@ -1,8 +1,10 @@ ///////////////////////////////////////////////////////////////////// def setLocationMode(String mode) { + log.debug "DEBUG: setLocationMode is called. Current mode is: ${location_mode} and new mode is: ${mode}" location.setValue([name: "Location", value: "$mode", deviceId: "locationID0", descriptionText: "", displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) location.setValue([name: "mode", value: "$mode", deviceId: "locationID0", descriptionText: "", displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']) + location_mode = mode } diff --git a/PresenceSensor/PresenceSensor.groovy b/PresenceSensor/PresenceSensor.groovy index b370736..7040a76 100644 --- a/PresenceSensor/PresenceSensor.groovy +++ b/PresenceSensor/PresenceSensor.groovy @@ -2,6 +2,9 @@ package PresenceSensor import Timer.SimulatedTimer +//JPF's Verify API +import gov.nasa.jpf.vm.Verify + public class PresenceSensor { private String id private String label @@ -25,6 +28,56 @@ public class PresenceSensor { this.presence = value this.currentPresence = value } + + def statesSince() { + eventsSince() + } + + def statesSince(String info, Date dateObj) { + statesSince() + } + + def eventsSince(Date dateObj) { + eventsSince() + } + + def eventsSince() { + def evtActive = [[name: "presence", value: "present", deviceId: "motionSensorID0", descriptionText: "", + displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']] + def evtInactive = [[name: "presence", value: "not present", deviceId: "motionSensorID0", 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 active event + evtActive.each{ + evtToSend.add(it) + } + return evtToSend + } else if (init == 2) {//send two active events + evtActive.each{ + evtToSend.add(it) + } + evtActive.each{ + evtToSend.add(it) + } + return evtToSend + } else if (init == 3) {//send one inactive event + evtInactive.each{ + evtToSend.add(it) + } + return evtToSend + } else if (init == 4) {//send two inactive events + evtInactive.each{ + evtToSend.add(it) + } + evtInactive.each{ + evtToSend.add(it) + } + return evtToSend + } + } def currentState(String deviceFeature) { return [rawDateCreated: [time: System.currentTimeMillis()]] diff --git a/PresenceSensor/PresenceSensors.groovy b/PresenceSensor/PresenceSensors.groovy index fd88b33..782e25c 100644 --- a/PresenceSensor/PresenceSensors.groovy +++ b/PresenceSensor/PresenceSensors.groovy @@ -76,6 +76,14 @@ public class PresenceSensors { presenceSensors[0].latestValue(deviceFeature)//It is called if we have only one device } + def statesSince(String info, Date dateObj) { + return presenceSensors[0].statesSince() + } + + def eventsSince(Date dateObj) { + return presenceSensors[0].statesSince() + } + def getAt(int ix) { presenceSensors[ix] } diff --git a/Runner.py b/Runner.py index ad8dff0..81efa7a 100644 --- a/Runner.py +++ b/Runner.py @@ -142,6 +142,8 @@ Out.write("//Application #1\n") Out.write("class App1 {\n") Out.write("\tdef reference\n") Out.write("\tdef location\n") +Out.write("\t// A local variable added for conflict detection tool\n") +Out.write("\tdef location_mode\n") Out.write("\tdef app\n") Out.write("\n") Out.write("\t//Extracted objects for App1\n") @@ -251,6 +253,8 @@ Out.write("//Application #2\n") Out.write("class App2 {\n") Out.write("\tdef reference\n") Out.write("\tdef location\n") +Out.write("\t// A local variable added for conflict detection tool\n") +Out.write("\tdef location_mode\n") Out.write("\tdef app\n") Out.write("\n") Out.write("\t//Extracted objects for App2\n")