package Alarm
import Timer.SimulatedTimer
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
public class Alarms {
int deviceNumbers
List alarms
private String currentAlarm = "off"
private String alarmLatestValue = "off"
- Alarms(Closure sendEvent, int deviceNumbers) {
+ Alarms(Closure sendEvent, int deviceNumbers, boolean init) {
this.sendEvent = sendEvent
this.timers = new SimulatedTimer()
this.deviceNumbers = deviceNumbers
this.alarms = []
- def init = Verify.getBoolean()
if (init) {
this.alarm = "off"
this.currentAlarm = "off"
//By Model Checker
def setValue(LinkedHashMap eventDataMap) {
if (eventDataMap["value"] != alarms[0].alarm) {
+ this.alarmLatestValue = eventDataMap["value"]
+ this.alarm = eventDataMap["value"]
+ this.currentAlarm = eventDataMap["value"]
alarms[0].setValue(eventDataMap["value"])
- this.alarmLatestValue = alarms[0].alarmLatestValue
- this.alarm = alarms[0].alarm
- this.currentAlarm = alarms[0].alarm
sendEvent(eventDataMap)
}
}
def find(Closure Input) {
alarms.find(Input)
}
+ def sort(Closure Input) {
+ alarms.sort(Input)
+ }
def collect(Closure Input) {
alarms.collect(Input)
}
//By Apps
def both() {
- alarms[0].both()
- alarmLatestValue = alarm
- alarm = "both"
- currentAlarm = "both"
+ if (alarm != "both") {
+ alarmLatestValue = "both"
+ alarm = "both"
+ currentAlarm = "both"
+ alarms[0].both()
+ }
}
def off() {
- alarms[0].off()
- alarmLatestValue = alarm
- alarm = "off"
- currentAlarm = "off"
+ if (alarm != "off") {
+ alarmLatestValue = "off"
+ alarm = "off"
+ currentAlarm = "off"
+ alarms[0].off()
+ }
}
def on() {
}
def siren() {
- alarms[0].siren()
- alarmLatestValue = alarm
- alarm = "siren"
- currentAlarm = "siren"
+ if (alarm != "siren") {
+ alarmLatestValue = "siren"
+ alarm = "siren"
+ currentAlarm = "siren"
+ alarms[0].siren()
+ }
}
def strobe() {
- alarms[0].strobe()
- alarmLatestValue = alarm
- alarm = "strobe"
- currentAlarm = "strobe"
+ if (alarm != "strobe") {
+ alarmLatestValue = "strobe"
+ alarm = "strobe"
+ currentAlarm = "strobe"
+ alarms[0].strobe()
+ }
}
def currentValue(String deviceFeature) {