import Timer.SimulatedTimer
//GlobalVariables
-@Field def location = new LocationVar()
+@Field def location = new LocationVar({}, true)
//Settings variable defined to settings on purpose
@Field def settings = [app: "app"]
//Global variable for state[mode]
@Field File extractedObjectsConstructorApp1 = new File("Extractor/App1/extractedObjectsConstructorApp1.groovy")
@Field File extractedObjectsConstructorApp2 = new File("Extractor/App2/extractedObjectsConstructorApp2.groovy")
-
+@Field chooseMode = 0
//Empty the files
if (App == "App1") {
globalObjects.write("")
extractedObjectsApp1.write("")
extractedObjectsConstructorApp1.write("")
+ chooseMode = 0
} else if (App == "App2") {
extractedObjectsApp2.write("")
extractedObjectsConstructorApp2.write("")
+ chooseMode = 1
}
case "mode":
//def randomVariable = Math.abs(new Random().nextInt() % 3)
def modes = ["away", "home", "night"]
- def userInput = modes[1]
+ // Always assign a different mode to each app
+ //def userInput = modes[1]
+ def userInput = modes[chooseMode]
+ if (chooseMode < 3)
+ chooseMode++;
+ else
+ chooseMode = chooseMode%3
if (modeVariables == 0) {
mode0 = metaData['name']
GlobalVariablesBothApps.write("")
GlobalVariablesBothApps.append("//Creating Global variables for both apps\n")
GlobalVariablesBothApps.append("@Field def sendEvent = {eventDataMap -> eventHandler(eventDataMap)}\n")
- GlobalVariablesBothApps.append("@Field def locationObject = new LocationVar(sendEvent)\n")
+ GlobalVariablesBothApps.append("@Field def locationObject = new LocationVar(sendEvent, init)\n")
GlobalVariablesBothApps.append("@Field def appObject = new Touched(sendEvent, 0)\n")
globalObjects.withReader { reader ->
private Phrase helloHome
- LocationVar(Closure sendEvent) {
- this.hubs = [[id:0, localIP:"128.195.204.105"]]
- this.modes = [[name: "home"],[name: "away"],[name: "night"]]
- this.mode = "home"
- this.helloHome = new Phrase()
- this.contactBookEnabled = 1
- this.contacts = ['AJ']
- this.phoneNumbers = [9495379373]
- this.sendEvent = sendEvent
- this.timeZone = TimeZone.getTimeZone("America/New_York")
- this.name = "hub0"
- this.temperatureScale = "F"
+ LocationVar(Closure sendEvent, boolean init) {
+
+ if (init) {
+ this.hubs = [[id:0, localIP:"128.195.204.105"]]
+ this.modes = [[name: "home"],[name: "away"],[name: "night"]]
+ this.mode = "away"
+ this.helloHome = new Phrase()
+ this.contactBookEnabled = 1
+ this.contacts = ['AJ']
+ this.phoneNumbers = [9495379373]
+ this.sendEvent = sendEvent
+ this.timeZone = TimeZone.getTimeZone("America/New_York")
+ this.name = "hub0"
+ this.temperatureScale = "F"
+ } else {
+ this.hubs = [[id:0, localIP:"128.195.204.105"]]
+ this.modes = [[name: "home"],[name: "away"],[name: "night"]]
+ this.mode = "home"
+ this.helloHome = new Phrase()
+ this.contactBookEnabled = 1
+ this.contacts = ['AJ']
+ this.phoneNumbers = [9495379373]
+ this.sendEvent = sendEvent
+ this.timeZone = TimeZone.getTimeZone("America/New_York")
+ this.name = "hub0"
+ this.temperatureScale = "F"
+
+ }
}
//By Model Checker
/////////////////////////////////////////////////////////////////////
def setLocationMode(String mode) {
+ log.debug "DEBUG: setLocationMode is called. Current mode is: ${location_mode} and new mode is: ${mode}"
location.setValue([name: "Location", value: "$mode", deviceId: "locationID0", descriptionText: "",
displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}'])
location.setValue([name: "mode", value: "$mode", deviceId: "locationID0", descriptionText: "",
displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}'])
+ location_mode = mode
}
package PresenceSensor
import Timer.SimulatedTimer
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
public class PresenceSensor {
private String id
private String label
this.presence = value
this.currentPresence = value
}
+
+ def statesSince() {
+ eventsSince()
+ }
+
+ def statesSince(String info, Date dateObj) {
+ statesSince()
+ }
+
+ def eventsSince(Date dateObj) {
+ eventsSince()
+ }
+
+ def eventsSince() {
+ def evtActive = [[name: "presence", value: "present", deviceId: "motionSensorID0", descriptionText: "",
+ displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
+ def evtInactive = [[name: "presence", value: "not present", deviceId: "motionSensorID0", descriptionText: "",
+ displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
+ def init = Verify.getInt(0,4)
+ def evtToSend = []
+ if (init == 0) {//return empty set
+ return evtToSend
+ } else if (init == 1) {//send one active event
+ evtActive.each{
+ evtToSend.add(it)
+ }
+ return evtToSend
+ } else if (init == 2) {//send two active events
+ evtActive.each{
+ evtToSend.add(it)
+ }
+ evtActive.each{
+ evtToSend.add(it)
+ }
+ return evtToSend
+ } else if (init == 3) {//send one inactive event
+ evtInactive.each{
+ evtToSend.add(it)
+ }
+ return evtToSend
+ } else if (init == 4) {//send two inactive events
+ evtInactive.each{
+ evtToSend.add(it)
+ }
+ evtInactive.each{
+ evtToSend.add(it)
+ }
+ return evtToSend
+ }
+ }
def currentState(String deviceFeature) {
return [rawDateCreated: [time: System.currentTimeMillis()]]
presenceSensors[0].latestValue(deviceFeature)//It is called if we have only one device
}
+ def statesSince(String info, Date dateObj) {
+ return presenceSensors[0].statesSince()
+ }
+
+ def eventsSince(Date dateObj) {
+ return presenceSensors[0].statesSince()
+ }
+
def getAt(int ix) {
presenceSensors[ix]
}
Out.write("class App1 {\n")
Out.write("\tdef reference\n")
Out.write("\tdef location\n")
+Out.write("\t// A local variable added for conflict detection tool\n")
+Out.write("\tdef location_mode\n")
Out.write("\tdef app\n")
Out.write("\n")
Out.write("\t//Extracted objects for App1\n")
Out.write("class App2 {\n")
Out.write("\tdef reference\n")
Out.write("\tdef location\n")
+Out.write("\t// A local variable added for conflict detection tool\n")
+Out.write("\tdef location_mode\n")
Out.write("\tdef app\n")
Out.write("\n")
Out.write("\t//Extracted objects for App2\n")