package DoorControl
import Timer.SimulatedTimer
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
public class DoorControls {
int deviceNumbers
List doorControls
private String doorState = "closed"
private String doorLatestValue = "closed"
- DoorControls(Closure sendEvent, int deviceNumbers) {
+ DoorControls(Closure sendEvent, int deviceNumbers, boolean init) {
this.sendEvent = sendEvent
this.timers = new SimulatedTimer()
this.deviceNumbers = deviceNumbers
this.doorControls = []
- def init = Verify.getBoolean()
if (init) {
this.doorState = "closed"
this.doorLatestValue = "closed"
def find(Closure Input) {
doorControls.find(Input)
}
+ def sort(Closure Input) {
+ doorControls.sort(Input)
+ }
def collect(Closure Input) {
doorControls.collect(Input)
}
//By Model Checker
def setValue(LinkedHashMap eventDataMap) {
if (eventDataMap["value"] != doorControls[0].doorState) {
+ this.doorState = eventDataMap["value"]
+ this.doorLatestValue = eventDataMap["value"]
doorControls[0].setValue(eventDataMap["value"])
- this.doorState = doorControls[0].doorState
sendEvent(eventDataMap)
}
}