From: rtrimana <rtrimana@uci.edu>
Date: Tue, 16 Jul 2019 18:20:47 +0000 (-0700)
Subject: Adding a variable conflict tracker/listener; this is useful for both device and globa... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=0907ba7dd70d7e43923eb812d1e4107f0b8d76c3;p=jpf-core.git

Adding a variable conflict tracker/listener; this is useful for both device and global variable conflict types.
---

diff --git a/examples/Empty.groovy b/examples/Empty.groovy
index 03a7101..e59fa9d 100644
--- a/examples/Empty.groovy
+++ b/examples/Empty.groovy
@@ -9,14 +9,17 @@ class Empty {
 		//int result = x + y;
 		//return result;
 		println "installed() is called!"
-		initialize()
+		boolean thisBoolean = false;
+		initialize(thisBoolean)
 	}
 
 	// This function is where you initialize callbacks for event listeners
-	def initialize() {
+	def initialize(thisBoolean) {
 		// The subscribe function takes a input, a state, and a callback method
 		//subscribe(contact, "contact.open", openHandler)
 		//subscribe(contact, "contact.closed", closedHandler)
+		thisBoolean = true;
+		println "Boolean is now " + thisBoolean
 		println "initialize() is called!"
 	}
 
diff --git a/examples/Racer.java b/examples/Racer.java
index 09c4002..4decefe 100644
--- a/examples/Racer.java
+++ b/examples/Racer.java
@@ -2,15 +2,20 @@ public class Racer implements Runnable {
      int d = 42;
 
      public void run () {
+          System.out.println("Thread 2!");
           doSomething(1001);
-          d = 0;                              // (1)
+          //d = 0;                              // (1)
      }
 
      public static void main (String[] args){
           Racer racer = new Racer();
           Thread t = new Thread(racer);
           t.start();
+          
+          Thread t2 = new Thread(racer);
+          t2.start();
 
+          System.out.println("Thread main!");
           doSomething(1000);
           int c = 420 / racer.d;              // (2)
           System.out.println(c);
diff --git a/examples/main/main.groovy b/examples/main/main.groovy
deleted file mode 100644
index e06f589..0000000
--- a/examples/main/main.groovy
+++ /dev/null
@@ -1,933 +0,0 @@
-//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: []])
-
diff --git a/examples/main/output b/examples/main/output
deleted file mode 100644
index 87b2068..0000000
--- a/examples/main/output
+++ /dev/null
@@ -1,37 +0,0 @@
-Installed with settings: Settings
-Current mode = home
-Settings: Settings
-The application is Touched!
-changeMode, location.mode = home, newMode = away, location.modes = 'home', 'away', 'night'
-Changed the mode to 'away'
-appTouch: Event@3214ee6
-the door with id:0 is unlocked!
-unlock
-4
-the door with id:1 is unlocked!
-unlock
-4
-the switch with id:0 is on!
-Locking the door.
-Locking the door.
-the door with id:0 is locked!
-the door with id:0 is locked!
-lock
-lock
-3
-the door with id:1 is locked!
-3
-the door with id:1 is locked!
-lock
-lock
-3
-3
-Sending Push Notification...
-Sending Push Notification...
-Sending "Locking@4aee8de6 locked after Contacting@1a995c02 was closed for 1 minutes!" to 9495379373
-Sending "Locking@4aee8de6 locked after Contacting@1a995c02 was closed for 1 minutes!" to 9495379373
-Sending text message...
-Sending text message...
-Sending "Locking@4aee8de6 locked after Contacting@1a995c02 was closed for 1 minutes!" to 9495379373
-Sending "Locking@4aee8de6 locked after Contacting@1a995c02 was closed for 1 minutes!" to 9495379373
-the switch with id:0 is off!
diff --git a/run.sh b/run.sh
index 276bd50..b075cb6 100755
--- a/run.sh
+++ b/run.sh
@@ -1,2 +1,4 @@
 #!/bin/bash
-java -Xmx1024m -classpath build/jpf.jar gov.nasa.jpf.JPF +classpath=examples:examples/groovy-2.5.7:examples/main $1
+#java -classpath build/jpf.jar gov.nasa.jpf.JPF +classpath=examples:examples/groovy-2.5.7:../smartthings-infrastructure/bin/main/ +listener=.listener.EventConflictTracker $1
+java -classpath build/jpf.jar gov.nasa.jpf.JPF +classpath=examples:examples/groovy-2.5.7:../smartthings-infrastructure/bin/main/ $1
+#java -Xmx1024m -classpath build/jpf.jar gov.nasa.jpf.JPF +classpath=examples:examples/groovy-2.5.7:../smartthings-infrastructure/bin/main/ $1
diff --git a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
new file mode 100644
index 0000000..77593f4
--- /dev/null
+++ b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
@@ -0,0 +1,269 @@
+/*
+ * 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);
+     }
+  }
+}