//JPF's Verify API
import gov.nasa.jpf.vm.Verify
+
public class Switches {
int deviceNumbers
List switches
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 = []
- 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"
+ 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))
}
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[0].setLevel(level)
currentLevel = level
+ switches[0].setLevel(level)
}
def on() {
- switches[0].on()
- switchLatestValue = switchState
+ switchLatestValue = "on"
switchState = "on"
currentSwitch = "on"
+ switches[0].on()
}
def on(LinkedHashMap metaData) {
def task = timers.runAfter(metaData["delay"]) {
- switches[0].on()
- switchLatestValue = switchState
+ switchLatestValue = "on"
switchState = "on"
currentSwitch = "on"
+ switches[0].on()
}
}
def off() {
- switches[0].off()
- switchLatestValue = switchState
+ switchLatestValue = "off"
switchState = "off"
currentSwitch = "off"
+ switches[0].off()
}
def off(LinkedHashMap metaData) {
def task = timers.runAfter(metaData["delay"]) {
- switches[0].off()
- switchLatestValue = switchState
+ switchLatestValue = "off"
switchState = "off"
currentSwitch = "off"
+ switches[0].off()
}
}
//By Model Checker
def setValue(LinkedHashMap eventDataMap) {
if (eventDataMap["value"] != switches[0].switchState) {
+ this.switchState = eventDataMap["value"]
+ this.switchLatestValue = eventDataMap["value"]
switches[0].setValue(eventDataMap["value"])
- this.switchState = switches[0].switchState
- this.switchLatestValue = switches[0].switchLatestValue
sendEvent(eventDataMap)
}
}