Adding a variable conflict tracker/listener; this is useful for both device and globa...
authorrtrimana <rtrimana@uci.edu>
Tue, 16 Jul 2019 18:20:47 +0000 (11:20 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 16 Jul 2019 18:20:47 +0000 (11:20 -0700)
examples/Empty.groovy
examples/Racer.java
examples/main/main.groovy [deleted file]
examples/main/output [deleted file]
run.sh
src/main/gov/nasa/jpf/listener/VariableConflictTracker.java [new file with mode: 0644]

index 03a71018a16fc6540d67ccaf4b8537f0e03d6c2d..e59fa9d476fce32f881989f87b94cd8339b9a7a9 100644 (file)
@@ -9,14 +9,17 @@ class Empty {
                //int result = x + y;
                //return result;
                println "installed() is called!"
                //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
        }
 
        // 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)
                // 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!"
        }
 
                println "initialize() is called!"
        }
 
index 09c40028d4d85a45fc422fee27defbad7f70e08e..4decefe4a991fadf6eb68ae69f74648c182eeee1 100644 (file)
@@ -2,15 +2,20 @@ public class Racer implements Runnable {
      int d = 42;
 
      public void run () {
      int d = 42;
 
      public void run () {
+          System.out.println("Thread 2!");
           doSomething(1001);
           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();
      }
 
      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);
           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 (file)
index e06f589..0000000
+++ /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 (file)
index 87b2068..0000000
+++ /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 276bd504f727ae8cbf4c31094503f46e4f011cf8..b075cb6a7b4e528cf5712abc9b0f2006708598de 100755 (executable)
--- a/run.sh
+++ b/run.sh
@@ -1,2 +1,4 @@
 #!/bin/bash
 #!/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 (file)
index 0000000..77593f4
--- /dev/null
@@ -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);
+     }
+  }
+}