X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=Switch%2FSwitches.groovy;h=36ba2de02918205039019e374806ad975c3f98ee;hb=01bc90033a262dfb036f903975105398ba90b673;hp=fad05f85676b1dbc14567d66ab8d42ec3533a95e;hpb=3b16c6767366cf912251d0e84f6eb28dc7276660;p=smartthings-infrastructure.git

diff --git a/Switch/Switches.groovy b/Switch/Switches.groovy
index fad05f8..36ba2de 100644
--- a/Switch/Switches.groovy
+++ b/Switch/Switches.groovy
@@ -2,6 +2,9 @@
 package Switch
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class Switches {
 	int deviceNumbers	
 	List switches
@@ -9,9 +12,9 @@ public class Switches {
 	def sendEvent
 
 	//If we have only one device
-	private int id = 40
-	private String label = "switch"
-	private String displayName = "switch"
+	private String id = "switchID0"
+	private String label = "switch0"
+	private String displayName = "switch0"
 	private String switchState = "off"
 	private String currentSwitch = "off"
 	private int currentLevel = 50
@@ -22,9 +25,21 @@ public class Switches {
 		this.timers = new SimulatedTimer()
 		this.deviceNumbers = deviceNumbers
 		this.switches = []
-		for (int i = 0;i < deviceNumbers;i++) {
-			switches.add(new Switch(sendEvent, i+40, label+i.toString(), displayName+i.toString(), this.switchState, this.currentSwitch, this.currentLevel, this.switchLatestValue))
+		
+		def initLevel = Verify.getIntFromList(30, 50, 70)
+		this.currentLevel = initLevel
+		def init = Verify.getBoolean()
+		if (init) {
+			this.switchState = "off"
+			this.currentSwitch = "off"
+			this.switchLatestValue = "off"
+		} else {
+			this.switchState = "on"
+			this.currentSwitch = "on"
+			this.switchLatestValue = "on"
 		}
+
+		switches.add(new Switch(sendEvent, id, label, displayName, this.switchState, this.currentSwitch, this.currentLevel, this.switchLatestValue))
 	}
 
 	//Methods for closures
@@ -37,54 +52,68 @@ public class Switches {
 	def each(Closure Input) {
 		switches.each(Input)
 	}
+	def find(Closure Input) {
+		switches.find(Input)
+	}
+	def collect(Closure Input) {
+		switches.collect(Input)
+	}
 
 	//By Apps
 	def setLevel(int level) {
-		switches*.setLevel(level)
+		switches[0].setLevel(level)
+		currentLevel = level
 	}
 
 	def on() {
-		switches*.on()
+		switches[0].on()
+		switchLatestValue = switchState
+		switchState = "on"
+		currentSwitch = "on"
 	}
 
 	def on(LinkedHashMap metaData) {
 		def task = timers.runAfter(metaData["delay"]) {
-			switches*.on()
+			switches[0].on()
+			switchLatestValue = switchState
+			switchState = "on"
+			currentSwitch = "on"
 		}
 	}
 
 	def off() {
-		switches*.off()
+		switches[0].off()
+		switchLatestValue = switchState
+		switchState = "off"
+		currentSwitch = "off"
 	}
 
 	def off(LinkedHashMap metaData) {
 		def task = timers.runAfter(metaData["delay"]) {
-			switches*.off()
+			switches[0].off()
+			switchLatestValue = switchState
+			switchState = "off"
+			currentSwitch = "off"
 		}
 	}
 
 	//By Model Checker
 	def setValue(LinkedHashMap eventDataMap) {
-		switches[eventDataMap["deviceId"]].setValue(eventDataMap["value"])
-		if (deviceNumbers == 1)
-			this.switchState = switches[eventDataMap["deviceId"]].switchState
-			this.switchLatestValue = switches[eventDataMap["deviceId"]].switchLatestValue
-		sendEvent(eventDataMap)
+		if (eventDataMap["value"] != switches[0].switchState) {
+			switches[0].setValue(eventDataMap["value"])
+			this.switchState = switches[0].switchState
+			this.switchLatestValue = switches[0].switchLatestValue
+			sendEvent(eventDataMap)
+		}
 	}
 
 
 	def currentValue(String deviceFeature) {
-		if (deviceNumbers == 1)
-			switches[0].currentValue(deviceFeature)
-		else
-			switches*.currentValue(deviceFeature)
+		switches[0].currentValue(deviceFeature)
 	}
 
 	def latestValue(String deviceFeature) {
-		if (deviceNumbers == 1)
-			switches[0].latestValue(deviceFeature)
-		else
-			switches*.latestValue(deviceFeature)
+		switches[0].latestValue(deviceFeature)
 	}
 
 	def getAt(int ix) {