package Switch
import Timer.SimulatedTimer
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
+
public class Switches {
int deviceNumbers
List 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
private String switchLatestValue = "off"
- Switches(Closure sendEvent, int deviceNumbers) {
+ Switches(Closure sendEvent, int deviceNumbers, boolean init) {
this.sendEvent = sendEvent
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))
+
+ if (init) {
+ this.switchState = "off"
+ this.currentSwitch = "off"
+ this.switchLatestValue = "off"
+ this.currentLevel = 50
+ } else {
+ this.switchState = "on"
+ this.currentSwitch = "on"
+ this.switchLatestValue = "on"
+ this.currentLevel = 60
}
+ switches.add(new Switch(sendEvent, id, label, displayName, this.switchState, this.currentSwitch, this.currentLevel, this.switchLatestValue))
}
//Methods for closures
def each(Closure Input) {
switches.each(Input)
}
+ def find(Closure Input) {
+ switches.find(Input)
+ }
+ def sort(Closure Input) {
+ switches.sort(Input)
+ }
+ def collect(Closure Input) {
+ switches.collect(Input)
+ }
//By Apps
+ def eventsSince(Date dateObj, LinkedHashMap metaData) {
+ return switches[0].eventsSince()
+ }
+
def setLevel(int level) {
- switches*.setLevel(level)
+ currentLevel = level
+ switches[0].setLevel(level)
}
def on() {
- switches*.on()
+ switchLatestValue = "on"
+ switchState = "on"
+ currentSwitch = "on"
+ switches[0].on()
}
def on(LinkedHashMap metaData) {
def task = timers.runAfter(metaData["delay"]) {
- switches*.on()
+ switchLatestValue = "on"
+ switchState = "on"
+ currentSwitch = "on"
+ switches[0].on()
}
}
def off() {
- switches*.off()
+ switchLatestValue = "off"
+ switchState = "off"
+ currentSwitch = "off"
+ switches[0].off()
}
def off(LinkedHashMap metaData) {
def task = timers.runAfter(metaData["delay"]) {
- switches*.off()
+ switchLatestValue = "off"
+ switchState = "off"
+ currentSwitch = "off"
+ switches[0].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) {
+ this.switchState = eventDataMap["value"]
+ this.switchLatestValue = eventDataMap["value"]
+ switches[0].setValue(eventDataMap["value"])
+ 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) {