From: rtrimana Date: Thu, 25 Jul 2019 18:37:29 +0000 (-0700) Subject: Limiting iteration for now (DFSearch strategy would just go deep unceasingly); Comple... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=smartthings-infrastructure.git;a=commitdiff_plain;h=4f9a1209b0c1ca5caf60a0f811e18dde6a92e9e9 Limiting iteration for now (DFSearch strategy would just go deep unceasingly); Completing the model-checking automation script; Removing thread from the Timer for now (this creates a lot of permutations for JPF); Hardcoding a few values for the extractor scripts (need to double-check later); Adding a run script for automation. --- diff --git a/Extractor/Extractor.groovy b/Extractor/Extractor.groovy index e3cb88a..2f308f5 100644 --- a/Extractor/Extractor.groovy +++ b/Extractor/Extractor.groovy @@ -828,10 +828,10 @@ def input(LinkedHashMap metaData) { break case "enum": def randomVariable = Math.abs(new Random().nextInt() % 2) - //def modes = ["Yes", "No"] + def modes = ["Yes", "No"] //def userInput = modes[randomVariable] // TODO: We - def modes = metaData['options'] + //def modes = metaData['options'] def userInput = modes[0] if (enumVariables == 0) { diff --git a/Extractor/ExtractorScript.py b/Extractor/ExtractorScript.py index 50bc843..11486bc 100644 --- a/Extractor/ExtractorScript.py +++ b/Extractor/ExtractorScript.py @@ -111,7 +111,8 @@ def AnalyzePhysicalInteraction(app1Capab, app2Capab): def ExtractEvents(extractedEvents): global eventMap - extractedEvents.write("while(true) {\n") + #extractedEvents.write("while(true) {\n") + extractedEvents.write("for(int i=0; i<100; i++) {\n") extractedEvents.write("\tdef eventNumber = Verify.getInt(0,%d)\n" % (len(eventMap) - 1)) extractedEvents.write("\tswitch(eventNumber) {\n") for i in range(len(eventMap)): diff --git a/Extractor/extractorFile.groovy b/Extractor/extractorFile.groovy index 5900547..5d14fb1 100644 --- a/Extractor/extractorFile.groovy +++ b/Extractor/extractorFile.groovy @@ -832,7 +832,10 @@ def input(LinkedHashMap metaData) { case "enum": def randomVariable = Math.abs(new Random().nextInt() % 2) def modes = ["Yes", "No"] - def userInput = modes[randomVariable] + //def userInput = modes[randomVariable] + // TODO: We + //def modes = metaData['options'] + def userInput = modes[0] if (enumVariables == 0) { enum0 = metaData['name'] @@ -1064,9 +1067,7 @@ def section(LinkedHashMap metaData, Closure inputData) { /** - * NFC Tag Toggle - * - * Copyright 2014 SmartThings + * Copyright 2015 SmartThings * * 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: @@ -1077,132 +1078,128 @@ def section(LinkedHashMap metaData, Closure inputData) { * 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. * + * Make it So + * + * Author: SmartThings + * Date: 2013-03-06 */ - definition( - name: "NFC Tag Toggle", + name: "Make It So", namespace: "smartthings", author: "SmartThings", - description: "Allows toggling of a switch, lock, or garage door based on an NFC Tag touch event", - category: "SmartThings Internal", - iconUrl: "https://s3.amazonaws.com/smartapp-icons/Developers/nfc-tag-executor.png", - iconX2Url: "https://s3.amazonaws.com/smartapp-icons/Developers/nfc-tag-executor@2x.png", - iconX3Url: "https://s3.amazonaws.com/smartapp-icons/Developers/nfc-tag-executor@2x.png") - + description: "Saves the states of a specified set switches and thermostat setpoints and restores them at each mode change. To use 1) Set the mode, 2) Change switches and setpoint to where you want them for that mode, and 3) Install or update the app. Changing to that mode or touching the app will set the devices to the saved state.", + category: "Convenience", + iconUrl: "https://s3.amazonaws.com/smartapp-icons/Meta/light_thermo-switch.png", + iconX2Url: "https://s3.amazonaws.com/smartapp-icons/Meta/light_thermo-switch@2x.png" +) preferences { - page(name: "pageOne", title: "Device selection", uninstall: true, nextPage: "pageTwo") { - section("Select an NFC tag") { - input "tag", "capability.touchSensor", title: "NFC Tag" - } - section("Select devices to control") { - input "switch1", "capability.switch", title: "Light or switch", required: false, multiple: true - input "lock", "capability.lock", title: "Lock", required: false, multiple: true - input "garageDoor", "capability.doorControl", title: "Garage door controller", required: false, multiple: true - } - } - - page(name: "pageTwo", title: "Master devices", install: true, uninstall: true) -} - -def pageTwo() { - dynamicPage(name: "pageTwo") { - section("If set, the state of these devices will be toggled each time the tag is touched, " + - "e.g. a light that's on will be turned off and one that's off will be turned on, " + - "other devices of the same type will be set to the same state as their master device. " + - "If no master is designated then the majority of devices of the same type will be used " + - "to determine whether to turn on or off the devices.") { - - if (switch1 || masterSwitch) { - input "masterSwitch", "enum", title: "Master switch", options: switch1.collect{[(it.id): it.displayName]}, required: false - } - if (lock || masterLock) { - input "masterLock", "enum", title: "Master lock", options: lock.collect{[(it.id): it.displayName]}, required: false - } - if (garageDoor || masterDoor) { - input "masterDoor", "enum", title: "Master door", options: garageDoor.collect{[(it.id): it.displayName]}, required: false - } - } - section([mobileOnly:true]) { - label title: "Assign a name", required: false - mode title: "Set for specific mode(s)", required: false - } - } + section("Switches") { + input "switches", "capability.switch", multiple: true, required: false + } + section("Thermostats") { + input "thermostats", "capability.thermostat", multiple: true, required: false + } + section("Locks") { + input "locks", "capability.lock", multiple: true, required: false + } } def installed() { - log.debug "Installed with settings: ${settings}" - - initialize() + subscribe(location, changedLocationMode) + subscribe(app, appTouch) + saveState() } def updated() { - log.debug "Updated with settings: ${settings}" - unsubscribe() - initialize() + subscribe(location, changedLocationMode) + subscribe(app, appTouch) + saveState() } -def initialize() { - subscribe tag, "nfcTouch", touchHandler - subscribe app, touchHandler +def appTouch(evt) +{ + restoreState(currentMode) } -private currentStatus(devices, master, attribute) { - log.trace "currentStatus($devices, $master, $attribute)" - def result = null - if (master) { - result = devices.find{it.id == master}?.currentValue(attribute) - } - else { - def map = [:] - devices.each { - def value = it.currentValue(attribute) - map[value] = (map[value] ?: 0) + 1 - log.trace "$it.displayName: $value" - } - log.trace map - result = map.collect{it}.sort{it.value}[-1].key - } - log.debug "$attribute = $result" - result +def changedLocationMode(evt) +{ + restoreState(evt.value) } -def touchHandler(evt) { - log.trace "touchHandler($evt.descriptionText)" - if (switch1) { - def status = currentStatus(switch1, masterSwitch, "switch") - switch1.each { - if (status == "on") { - it.off() - } - else { - it.on() - } - } - } - - if (lock) { - def status = currentStatus(lock, masterLock, "lock") - lock.each { - if (status == "locked") { - lock.unlock() - } - else { - lock.lock() - } - } - } - - if (garageDoor) { - def status = currentStatus(garageDoor, masterDoor, "status") - garageDoor.each { - if (status == "open") { - it.close() - } - else { - it.open() - } - } - } +private restoreState(mode) +{ + log.info "restoring state for mode '$mode'" + def map = state[mode] ?: [:] + switches?.each { + def value = map[it.id] + if (value?.switch == "on") { + def level = value.level + if (level) { + log.debug "setting $it.label level to $level" + it.setLevel(level) + } + else { + log.debug "turning $it.label on" + it.on() + } + } + else if (value?.switch == "off") { + log.debug "turning $it.label off" + it.off() + } + } + + thermostats?.each { + def value = map[it.id] + if (value?.coolingSetpoint) { + log.debug "coolingSetpoint = $value.coolingSetpoint" + it.setCoolingSetpoint(value.coolingSetpoint) + } + if (value?.heatingSetpoint) { + log.debug "heatingSetpoint = $value.heatingSetpoint" + it.setHeatingSetpoint(value.heatingSetpoint) + } + } + + locks?.each { + def value = map[it.id] + if (value) { + if (value?.locked) { + it.lock() + } + else { + it.unlock() + } + } + } +} + + +private saveState() +{ + def mode = currentMode + def map = state[mode] ?: [:] + + switches?.each { + map[it.id] = [switch: it.currentSwitch, level: it.currentLevel] + } + + thermostats?.each { + map[it.id] = [coolingSetpoint: it.currentCoolingSetpoint, heatingSetpoint: it.currentHeatingSetpoint] + } + + locks?.each { + map[it.id] = [locked: it.currentLock == "locked"] + } + + state[mode] = map + log.debug "saved state for mode ${mode}: ${state[mode]}" + log.debug "state: $state" } + +private getCurrentMode() +{ + location.mode ?: "_none_" +} \ No newline at end of file diff --git a/ModelCheck.py b/ModelCheck.py index 145bd22..82c6adf 100644 --- a/ModelCheck.py +++ b/ModelCheck.py @@ -24,7 +24,8 @@ appList2 = [] # Extract the first list extractAppList = open(firstList, "r") for app in extractAppList: - appList1.append(app.strip()) + if '#' not in app: + appList1.append(app.strip()) extractAppList.close() # Try to create pairs @@ -34,7 +35,8 @@ if (len(sys.argv) == 6): secondList = sys.argv[5] extractAppList = open(secondList, "r") for app in extractAppList: - appList2.append(app.strip()) + if '#' not in app: + appList2.append(app.strip()) extractAppList.close() # Just copy the first list to the second list else: @@ -47,7 +49,10 @@ for i in range(len(appList1)): # PART 2: print "PHASE 2: Running JPF ...\n" +# List down all the log file names +writeLogList = open(jpfLogDir + "logList", "w+") for item in appPairs: + # Copy apps into Extractor/App1 and Extractor/App2 os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy") os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy") @@ -59,4 +64,8 @@ for item in appPairs: # Call JPF print "==> Calling JPF and generate logs ...\n" - os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + item[0] + "--" + item[1] + ".log" + " main.jpf") + logName = jpfLogDir + item[0] + "--" + item[1] + ".log" + writeLogList.write(logName + "\n") + os.system("cd " + jpfDir + ";./run.sh " + logName + " main.jpf") + +writeLogList.close() diff --git a/Timer/SimulatedTimer.groovy b/Timer/SimulatedTimer.groovy index a133766..cf123be 100644 --- a/Timer/SimulatedTimer.groovy +++ b/Timer/SimulatedTimer.groovy @@ -10,7 +10,7 @@ public class SimulatedTimer { //By Apps def runAfter(int delay, Closure closure) { - thread = new Thread() { + /*thread = new Thread() { @Override public void run() { @@ -18,11 +18,12 @@ public class SimulatedTimer { closure() } }.start() - return thread + return thread*/ + closure() } def cancel() { - if (thread != null) - thread.stop() + //if (thread != null) + // thread.stop() } } diff --git a/run.sh b/run.sh new file mode 100755 index 0000000..7ba9baa --- /dev/null +++ b/run.sh @@ -0,0 +1,2 @@ +#!/bin/bash +python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ ../smartapps/appList1