Adding direct-direct pair detection; adding missing app lists.

diff --git a/ModelCheck.py b/ModelCheck.py
index d00c6991a2c2c7a710d2f2f5a6106a99bf647b02..1a0c940bb66ff273d3fc6300b4914d8879f940c5 100644 (file)
--- a/ModelCheck.py
+++ b/ModelCheck.py
@@ -17,10 +17,31 @@ def checkResult(logDirName):
                elif "java.lang.RuntimeException: Conflict between apps App1 and App2:" in line:
                        result = "conflict"
                        break
+               elif "Direct-Direct Interaction detected:" in line:
+                       result = "direct-direct"
+                       break
        
        return result
 
-
+# Extract the error from specific error logs
+def extractError():
+       err = ""
+       if os.path.exists("appCreationError.log"):
+               extractError = open("appCreationError.log", "r")
+               for line in extractError:
+                       err = err + line
+               extractError.close()
+               os.system("rm appCreationError.log")
+       return err
+
+# Write error log to the log directory
+# In this case we skip running JPF
+# e.g., in the case of having a direct-direct interaction pair
+def writeErrorLog(jpfLogDir, logName, error):
+       writeError = open(jpfLogDir + logName, "w+")
+       writeError.write(error)
+       writeError.close()
+       
 # Input parameters:
 # - JPF directory
 # - JPF logs directory
@@ -92,12 +113,18 @@ for item in appPairs:
        # Run Runner.py to extract things and create main.groovy, then compile it
        print "==> Compiling the apps ...\n"
        os.system("make Runner")
-       os.system("make main")
-       
-       # Call JPF
-       print "==> Calling JPF and generate logs ...\n"
+       error = extractError()
        logName = item[0] + "--" + item[1] + ".log"
-       os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
+       if error == "":
+               # Compile
+               os.system("make main")
+               # Call JPF
+               print "==> Calling JPF and generate logs ...\n"
+               os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
+       else:
+               # This is for specific error, e.g., direct-direct interaction that we need to skip
+               writeErrorLog(jpfLogDir, logName, error)
+               
        result = checkResult(jpfLogDir + logName)
        writeLogList.write(logName + "\t\t" + result + "\n")
 

diff --git a/appLists/device-interaction/acfanheaterSwitchesAppList b/appLists/device-interaction/acfanheaterSwitchesAppList
new file mode 100644 (file)
index 0000000..bcb0fdd
--- /dev/null
+++ b/appLists/device-interaction/acfanheaterSwitchesAppList
@@ -0,0 +1,3 @@
+its-too-cold.groovy
+its-too-hot.groovy
+virtual-thermostat.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/alarmsAppList b/appLists/device-interaction/alarmsAppList
new file mode 100644 (file)
index 0000000..51487f7
--- /dev/null
+++ b/appLists/device-interaction/alarmsAppList
@@ -0,0 +1,4 @@
+lock-it-at-a-specific-time.groovy
+#lock-it-when-i-leave.groovy
+#make-it-so.groovy
+nfc-tag-toggle.groovy

diff --git a/appLists/device-interaction/cameraSwitchesAppList b/appLists/device-interaction/cameraSwitchesAppList
new file mode 100644 (file)
index 0000000..26b4300
--- /dev/null
+++ b/appLists/device-interaction/cameraSwitchesAppList
@@ -0,0 +1,2 @@
+camera-power-scheduler.groovy
+cameras-on-when-im-away.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/camerasAppList b/appLists/device-interaction/camerasAppList
new file mode 100644 (file)
index 0000000..b2376c2
--- /dev/null
+++ b/appLists/device-interaction/camerasAppList
@@ -0,0 +1,3 @@
+foscam-connect.groovy
+opent2t-smartapp-test.groovy
+photo-burst-when.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/hueLightsAppList b/appLists/device-interaction/hueLightsAppList
new file mode 100644 (file)
index 0000000..6f94562
--- /dev/null
+++ b/appLists/device-interaction/hueLightsAppList
@@ -0,0 +1,13 @@
+03-sms-to-hue.groovy
+door-state-to-color-light-hue-bulb.groovy
+hue-minimote.groovy
+hue-mood-lighting.groovy
+jenkins-notifier.groovy
+notify-me-with-hue.groovy
+step-notifier.groovy
+tweet-to-hue.groovy
+BetterLaundryMonitor.groovy
+Hue Party Mode.groovy
+mini-hue-controller.groovy
+hue-lights-and-groups-and-scenes-oh-my.groovy
+loft.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/lightSwitchesAppList b/appLists/device-interaction/lightSwitchesAppList
new file mode 100644 (file)
index 0000000..11cab3f
--- /dev/null
+++ b/appLists/device-interaction/lightSwitchesAppList
@@ -0,0 +1,32 @@
+brighten-dark-places.groovy
+brighten-my-path.groovy
+darken-behind-me.groovy
+forgiving-security.groovy
+good-night-house.groovy
+hall-light-welcome-home.groovy
+hue-minimote.groovy
+laundry-monitor.groovy
+let-there-be-dark.groovy
+let-there-be-light.groovy
+Light_Rule.groovy
+light-follows-me.groovy
+lighting-director.groovy
+lights-off-with-no-motion-and-presence.groovy
+light-up-the-night.groovy
+mood-cube.groovy
+my-light-toggle.groovy
+smart-light-timer-x-minutes-unless-already-on.groovy
+smart-nightlight.groovy
+smart-security.groovy
+step-notifier.groovy
+turn-on-at-sunset.groovy
+turn-on-before-sunset.groovy
+turn-on-by-zip-code.groovy
+turn-it-on-when-im-here.groovy
+turn-it-on-when-it-opens.groovy
+turn-off-with-motion.groovy
+turn-on-only-if-i-arrive-after-sunset.groovy
+undead-early-warning.groovy
+vacation-lighting-director.groovy
+ecobeeAwayFromHome.groovy
+FireCO2Alarm.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/locksAppList b/appLists/device-interaction/locksAppList
new file mode 100644 (file)
index 0000000..f07a963
--- /dev/null
+++ b/appLists/device-interaction/locksAppList
@@ -0,0 +1,21 @@
+##beacon-control.groovy
+#enhanced-auto-lock-door.groovy
+good-night-house.groovy
+##initial-state-event-streamer.groovy
+#lock-it-at-a-specific-time.groovy
+#lock-it-when-i-leave.groovy
+#make-it-so.groovy
+nfc-tag-toggle.groovy
+##single-button-controller.groovy
+##smart-auto-lock-unlock.groovy
+#unlock-it-when-i-arrive.groovy
+#auto-lock-door.smartapp.groovy
+##buffered-event-sender.groovy
+##ecobeeAwayFromHome.groovy
+#FireCO2Alarm.groovy
+##groveStreams.groovy
+##influxdb-logger.groovy
+##initial-state-event-sender.groovy
+##initialstate-smart-app-v1.2.0.groovy
+#NotifyIfLeftUnlocked.groovy
+##unbuffered-event-sender.groovy

diff --git a/appLists/device-interaction/musicPlayersAppList b/appLists/device-interaction/musicPlayersAppList
new file mode 100644 (file)
index 0000000..9c5b6f8
--- /dev/null
+++ b/appLists/device-interaction/musicPlayersAppList
@@ -0,0 +1,5 @@
+initial-state-event-streamer.groovy
+buffered-event-sender.groovy
+influxdb-logger.groovy
+initialstate-smart-app-v1.2.0.groovy
+unbuffered-event-sender.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/nonHueLightsAppList b/appLists/device-interaction/nonHueLightsAppList
new file mode 100644 (file)
index 0000000..7d58810
--- /dev/null
+++ b/appLists/device-interaction/nonHueLightsAppList
@@ -0,0 +1,11 @@
+color-coordinator.groovy
+initial-state-event-streamer.groovy
+medicine-management-contact-sensor.groovy
+medicine-management-temp-motion.groovy
+buffered-event-sender.groovy
+circadian-daylight.groovy
+influxdb-logger.groovy
+initial-state-event-sender.groovy
+initialstate-smart-app-v1.2.0.groovy
+unbuffered-event-sender.groovy
+hue-minimote.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/relaySwitchesAppList b/appLists/device-interaction/relaySwitchesAppList
new file mode 100644 (file)
index 0000000..75b2486
--- /dev/null
+++ b/appLists/device-interaction/relaySwitchesAppList
@@ -0,0 +1,5 @@
+initial-state-event-streamer.groovy
+buffered-event-sender.groovy
+initial-state-event-sender.groovy
+initialstate-smart-app-v1.2.0.groovy
+unbuffered-event-sender.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/speechesAppList b/appLists/device-interaction/speechesAppList
new file mode 100644 (file)
index 0000000..a232cd6
--- /dev/null
+++ b/appLists/device-interaction/speechesAppList
@@ -0,0 +1,3 @@
+BetterLaundryMonitor.groovy
+FireCO2Alarm.groovy
+WindowOrDoorOpen.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/switchesAppList b/appLists/device-interaction/switchesAppList
new file mode 100644 (file)
index 0000000..fdadf64
--- /dev/null
+++ b/appLists/device-interaction/switchesAppList
@@ -0,0 +1,24 @@
+01-control-lights-and-locks-with-contact-sensor.groovy
+beacon-control.groovy
+big-turn-off.groovy
+big-turn-on.groovy
+control-switch-with-contact-sensor.groovy
+double-tap.groovy
+energy-saver.groovy
+gentle-wake-up.groovy
+good-night.groovy
+humidity-alert.groovy
+jenkins-notifier.groovy
+make-it-so.groovy
+monitor-on-sense.groovy
+nfc-tag-toggle.groovy
+once-a-day.groovy
+power-allowance.groovy
+rise-and-shine.groovy
+smart-turn-it-on.groovy
+sunrise-sunset.groovy
+the-big-switch.groovy
+turn-it-on-for-5-minutes.groovy
+BetterLaundryMonitor.groovy
+garage-switch.groovy
+loft.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/thermostatsAppList b/appLists/device-interaction/thermostatsAppList
new file mode 100644 (file)
index 0000000..f0a6573
--- /dev/null
+++ b/appLists/device-interaction/thermostatsAppList
@@ -0,0 +1,19 @@
+initial-state-event-streamer.groovy
+keep-me-cozy.groovy
+keep-me-cozy-ii.groovy
+make-it-so.groovy
+talking-alarm-clock.groovy
+thermostat.groovy
+thermostat-auto-off.groovy
+thermostat-mode-director.groovy
+thermostat-window-check.groovy
+whole-house-fan.groovy
+buffered-event-sender.groovy
+FireCO2Alarm.groovy
+groveStreams.groovy
+hvac-auto-off.smartapp.groovy
+influxdb-logger.groovy
+initial-state-event-sender.groovy
+initialstate-smart-app-v1.2.0.groovy
+unbuffered-event-sender.groovy
+WindowOrDoorOpen.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/valvesAppList b/appLists/device-interaction/valvesAppList
new file mode 100644 (file)
index 0000000..2d2ba98
--- /dev/null
+++ b/appLists/device-interaction/valvesAppList
@@ -0,0 +1,7 @@
+close-the-valve.groovy
+initial-state-event-streamer.groovy
+buffered-event-sender.groovy
+influxdb-logger.groovy
+initial-state-event-sender.groovy
+initialstate-smart-app-v1.2.0.groovy
+unbuffered-event-sender.groovy
\ No newline at end of file

diff --git a/appLists/device-interaction/ventfanSwitchesAppList b/appLists/device-interaction/ventfanSwitchesAppList
new file mode 100644 (file)
index 0000000..b827486
--- /dev/null
+++ b/appLists/device-interaction/ventfanSwitchesAppList
@@ -0,0 +1,3 @@
+auto-humidity-vent.groovy
+smart-home-ventilation.groovy
+whole-house-fan.groovy
\ No newline at end of file

diff --git a/appLists/global-state-variable-interaction/globalstatevariableAppList b/appLists/global-state-variable-interaction/globalstatevariableAppList
new file mode 100644 (file)
index 0000000..04c4d0a
--- /dev/null
+++ b/appLists/global-state-variable-interaction/globalstatevariableAppList
@@ -0,0 +1,47 @@
+beacon-control.groovy
+bon-voyage.groovy
+bose-soundtouch-control.groovy
+bright-when-dark-and-or-bright-after-sunset.groovy
+button-controller.groovy
+forgiving-security.groovy
+gentle-wake-up.groovy
+good-night.groovy
+good-night-house.groovy
+greetings-earthling.groovy
+hello-home-phrase-director.groovy
+hue-mood-lighting.groovy
+keep-me-cozy.groovy
+lighting-director.groovy
+make-it-so.groovy
+nobody-home.groovy
+notify-me-with-hue.groovy
+rise-and-shine.groovy
+routine-director.groovy
+scheduled-mode-change.groovy
+simple-sync-trigger.groovy
+single-button-controller.groovy
+smart-alarm.groovy
+smart-home-ventilation.groovy
+smart-security.groovy
+sonos-music-modes.groovy
+speaker-control.groovy
+speaker-mood-music.groovy
+speaker-notify-with-sound.groovy
+speaker-weather-forecast.groovy
+sunrise-sunset.groovy
+switch-activates-home-phrase-or-mode.groovy
+switch-changes-mode.groovy
+talking-alarm-clock.groovy
+thermostat-mode-director.groovy
+vacation-lighting-director.groovy
+working-from-home.groovy
+button-controller-for-hlgs.groovy
+circadian-daylight.groovy
+ecobeeChangeMode.groovy
+ecobeeGenerateWeeklyStats.groovy
+ecobeeManageClimate.groovy
+ecobeeResumeProg.groovy
+MonitorAndSetEcobeeHumidity.groovy
+SmartPresence.groovy
+Switches.groovy
+WorkingFromHome.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/illuminancesensorAppList b/appLists/physical-interaction/illuminancesensorAppList
new file mode 100644 (file)
index 0000000..07f39ee
--- /dev/null
+++ b/appLists/physical-interaction/illuminancesensorAppList
@@ -0,0 +1,5 @@
+brighten-dark-places.groovy
+bright-when-dark-and-or-bright-after-sunset.groovy
+lighting-director.groovy
+light-up-the-night.groovy
+smart-nightlight.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/lightAppList b/appLists/physical-interaction/lightAppList
new file mode 100644 (file)
index 0000000..e5fac4e
--- /dev/null
+++ b/appLists/physical-interaction/lightAppList
@@ -0,0 +1,42 @@
+brighten-dark-places.groovy
+brighten-my-path.groovy
+darken-behind-me.groovy
+forgiving-security.groovy
+good-night-house.groovy
+hall-light-welcome-home.groovy
+hue-minimote.groovy
+laundry-monitor.groovy
+let-there-be-dark.groovy
+let-there-be-light.groovy
+Light_Rule.groovy
+light-follows-me.groovy
+lighting-director.groovy
+lights-off-with-no-motion-and-presence.groovy
+light-up-the-night.groovy
+mood-cube.groovy
+my-light-toggle.groovy
+smart-light-timer-x-minutes-unless-already-on.groovy
+smart-nightlight.groovy
+smart-security.groovy
+step-notifier.groovy
+turn-on-at-sunset.groovy
+turn-on-before-sunset.groovy
+turn-on-by-zip-code.groovy
+turn-it-on-when-im-here.groovy
+turn-it-on-when-it-opens.groovy
+turn-off-with-motion.groovy
+turn-on-only-if-i-arrive-after-sunset.groovy
+undead-early-warning.groovy
+vacation-lighting-director.groovy
+ecobeeAwayFromHome.groovy
+FireCO2Alarm.groovy
+bright-when-dark-and-or-bright-after-sunset.groovy
+03-sms-to-hue.groovy
+color-coordinator.groovy
+door-state-to-color-light-hue-bulb.groovy
+hue-mood-lighting.groovy
+medicine-management-contact-sensor.groovy
+medicine-management-temp-motion.groovy
+notify-me-with-hue.groovy
+tweet-to-hue.groovy
+gentle-wake-up.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/motionAppList b/appLists/physical-interaction/motionAppList
new file mode 100644 (file)
index 0000000..149e456
--- /dev/null
+++ b/appLists/physical-interaction/motionAppList
@@ -0,0 +1,2 @@
+coffee-after-shower.groovy
+neato-connect.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/motionsensorAppList b/appLists/physical-interaction/motionsensorAppList
new file mode 100644 (file)
index 0000000..1b8ca82
--- /dev/null
+++ b/appLists/physical-interaction/motionsensorAppList
@@ -0,0 +1,37 @@
+bose-soundtouch-control.groovy
+brighten-my-path.groovy
+bright-when-dark-and-or-bright-after-sunset.groovy
+curling-iron.groovy
+darken-behind-me.groovy
+elder-care-daily-routine.groovy
+elder-care-slip-fall.groovy
+forgiving-security.groovy
+good-night.groovy
+hue-mood-lighting.groovy
+light-follows-me.groovy
+lights-off-with-no-motion-and-presence.groovy
+my-light-toggle.groovy
+notify-me-when.groovy
+notify-me-with-hue.groovy
+photo-burst-when.groovy        rise-and-shine.groovy
+safe-watch.groovy
+send-ham-bridge-command-when.groovy
+simple-sync-trigger.groovy
+smart-alarm.groovy
+smart-light-timer-x-minutes-unless-already-on.groovy
+smart-nightlight.groovy        smart-security.groovy
+speaker-control.groovy
+speaker-mood-music.groovy
+speaker-notify-with-sound.groovy
+speaker-weather-forecast.groovy
+text-me-when-theres-motion-and-im-not-here.groovy
+the-flasher.groovy
+turn-off-with-motion.groovy
+ubi.groovy
+virtual-thermostat.groovy
+camera-motion.groovy
+ecobeeAwayFromHome.groovy
+ecobeeResumeProg.groovy
+loft.groovy
+MonitorAndSetEcobeeTemp.groovy
+it-moved.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/soundAppList b/appLists/physical-interaction/soundAppList
new file mode 100644 (file)
index 0000000..635b0d2
--- /dev/null
+++ b/appLists/physical-interaction/soundAppList
@@ -0,0 +1,23 @@
+bose-soundtouch-control.groovy
+forgiving-security.groovy
+ifttt.groovy
+initial-state-event-streamer.groovy
+logitech-harmony-connect.groovy
+smart-alarm.groovy
+smart-security.groovy
+initial-state-event-streamer.groovy
+simple-control.groovy
+single-button-controller.groovy
+sonos-music-modes.groovy
+sonos-remote-control.groovy
+step-notifier.groovy
+talking-alarm-clock.groovy
+buffered-event-sender.groovy
+influxdb-logger.groovy
+initialstate-smart-app-v1.2.0.groovy
+Sonos.groovy
+unbuffered-event-sender.groovy
+BetterLaundryMonitor.groovy
+FireCO2Alarm.groovy
+loft.groovy
+WindowOrDoorOpen.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/soundsensorAppList b/appLists/physical-interaction/soundsensorAppList
new file mode 100644 (file)
index 0000000..afc906c
--- /dev/null
+++ b/appLists/physical-interaction/soundsensorAppList
@@ -0,0 +1 @@
+influxdb-logger.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/watersensorAppList b/appLists/physical-interaction/watersensorAppList
new file mode 100644 (file)
index 0000000..f036a84
--- /dev/null
+++ b/appLists/physical-interaction/watersensorAppList
@@ -0,0 +1,11 @@
+bose-soundtouch-control.groovy
+close-the-valve.groovy
+dry-the-wetspot.groovy
+flood-alert.groovy
+hue-mood-lighting.groovy
+notify-me-when.groovy
+notify-me-with-hue.groovy
+speaker-control.groovy
+speaker-mood-music.groovy
+speaker-notify-with-sound.groovy
+speaker-weather-forecast.groovy
\ No newline at end of file

diff --git a/appLists/physical-interaction/watervalveAppList b/appLists/physical-interaction/watervalveAppList
new file mode 100644 (file)
index 0000000..b3e5dfc
--- /dev/null
+++ b/appLists/physical-interaction/watervalveAppList
@@ -0,0 +1,2 @@
+close-the-valve.groovy
+sprayer-controller-2.groovy
\ No newline at end of file

diff --git a/run.sh b/run.sh
index 7ba9baab7a537e4ceec7da58119e316524bf0c12..6c955cea6e3c8df18fec04372294c46ec3951e92 100755 (executable)
--- a/run.sh
+++ b/run.sh
@@ -1,2 +1,10 @@
 #!/bin/bash
-python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ ../smartapps/appList1
+
+# Device conflict
+python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ appLists/device-interaction/locksAppList
+
+# Physical conflict
+#python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ appLists/physical-interaction/soundsensorAppList appLists/physical-interaction/soundAppList
+#python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ appLists/physical-interaction/motionsensorAppList appLists/physical-interaction/motionAppList
+#python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ appLists/physical-interaction/illuminancesensorAppList appLists/physical-interaction/lightAppList
+#python ModelCheck.py ../jpf-core/ ../logs/ ../smartapps/ appLists/physical-interaction/watersensorAppList appLists/physical-interaction/watervalveAppList