package Lock
import Timer.SimulatedTimer
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
public class Locks{
int deviceNumbers
List locks
this.deviceNumbers = deviceNumbers
this.locks = []
+ def init = Verify.getBoolean()
+ if (init) {
+ this.lockState = "locked"
+ this.lockLatestValue = "locked"
+ } else {
+ this.lockState = "unlocked"
+ this.lockLatestValue = "unlocked"
+ }
locks.add(new Lock(sendEvent,id, label, displayName, this.lockState, this.lockLatestValue))
}