Limiting iteration for now (DFSearch strategy would just go deep unceasingly); Comple...

diff --git a/Extractor/Extractor.groovy b/Extractor/Extractor.groovy
index e3cb88a13cfac87f2040e72f5ad3c053e0ac9a6e..2f308f5e85a864c13fd7acc17c4e14a30d824147 100644 (file)
--- 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)
                        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 userInput = modes[randomVariable]
                        // TODO: We 

-                       def modes = metaData['options']
+                       //def modes = metaData['options']

                        def userInput = modes[0]
        
                        if (enumVariables == 0) {
                        def userInput = modes[0]
        
                        if (enumVariables == 0) {

diff --git a/Extractor/ExtractorScript.py b/Extractor/ExtractorScript.py
index 50bc843c89b97bbdb600f79090cfe11efaeaf8d4..11486bc7301702d1bc5b901f27af3cd275d015e6 100644 (file)
--- a/Extractor/ExtractorScript.py
+++ b/Extractor/ExtractorScript.py
@@ -111,7 +111,8 @@ def AnalyzePhysicalInteraction(app1Capab, app2Capab):
 
 def ExtractEvents(extractedEvents):
        global eventMap
 
 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)):
        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 590054701054db8b793476f7e969cba41a1dfef1..5d14fb1f2b563e85793684d67049312f1bd8b0a8 100644 (file)
--- 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"]
                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']
        
                        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:
  *
  *  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.
  *
  *  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(
 definition(

-    name: "NFC Tag Toggle",
+    name: "Make It So",

     namespace: "smartthings",
     author: "SmartThings",
     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 {
 
 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() {
 }
 
 def installed() {

-       log.debug "Installed with settings: ${settings}"
-
-       initialize()
+       subscribe(location, changedLocationMode)
+       subscribe(app, appTouch)
+       saveState()

 }
 
 def updated() {
 }
 
 def updated() {

-       log.debug "Updated with settings: ${settings}"
-

        unsubscribe()
        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 145bd22857eb59633178bc73938c51dfbc580c3e..82c6adffeffe847fe202635448f8659031b161db 100644 (file)
--- a/ModelCheck.py
+++ b/ModelCheck.py
@@ -24,7 +24,8 @@ appList2 = []
 # Extract the first list
 extractAppList = open(firstList, "r")
 for app in extractAppList:
 # 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
 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:
        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:
        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"
 
 # PART 2: 
 print "PHASE 2: Running JPF ...\n"

+# List down all the log file names
+writeLogList = open(jpfLogDir + "logList", "w+")

 for item in appPairs:
 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")
        # 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"
        
        # 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 a13376610f5f56f26341e4a6cb4f666332c25a2c..cf123be7992dcebbbd6c72c398670ed20d608dbe 100644 (file)
--- a/Timer/SimulatedTimer.groovy
+++ b/Timer/SimulatedTimer.groovy
@@ -10,7 +10,7 @@ public class SimulatedTimer {
 \r
        //By Apps\r
        def runAfter(int delay, Closure closure) {\r
 \r
        //By Apps\r
        def runAfter(int delay, Closure closure) {\r

-               thread = new Thread() {\r
+               /*thread = new Thread() {\r

        \r
                        @Override\r
                        public void run() {\r
        \r
                        @Override\r
                        public void run() {\r


@@ -18,11 +18,12 @@ public class SimulatedTimer {
                                closure()\r
                        }\r
                }.start()\r
                                closure()\r
                        }\r
                }.start()\r

-               return thread\r
+               return thread*/\r
+               closure()\r

        }\r
 \r
        def cancel() {\r
        }\r
 \r
        def cancel() {\r

-               if (thread != null)\r
-                       thread.stop()\r
+               //if (thread != null)\r
+               //      thread.stop()\r

        }\r
 }\r
        }\r
 }\r

diff --git a/run.sh b/run.sh
new file mode 100755 (executable)
index 0000000..7ba9baa
--- /dev/null
+++ b/run.sh
@@ -0,0 +1,2 @@
+#!/bin/bash
+python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ ../smartapps/appList1