Lock/Locks.groovy

   1 //Create a class for lock device
   2 package Lock
   3 import Timer.SimulatedTimer
   4
   5 //JPF's Verify API
   6 import gov.nasa.jpf.vm.Verify
   7
   8 public class Locks{
   9         int deviceNumbers
  10         List locks
  11         def sendEvent
  12         def timers
  13
  14         //When we have only one device
  15         private String id = "lockID0"
  16         private String label = "lock0"
  17         private String displayName = "lock0"
  18         private String lockState = "locked"
  19         private String currentLock = "locked"
  20         private String lockLatestValue = "locked"
  21
  22         Locks(Closure sendEvent, int deviceNumbers) {
  23                 this.sendEvent = sendEvent
  24                 this.timers = new SimulatedTimer()
  25                 this.deviceNumbers = deviceNumbers
  26                 this.locks = []
  27
  28                 def init = Verify.getBoolean()
  29                 if (init) {
  30                         this.lockState = "locked"
  31                         this.currentLock = "locked"
  32                         this.lockLatestValue = "locked"
  33                 } else {
  34                         this.lockState = "unlocked"
  35                         this.currentLock = "unlocked"
  36                         this.lockLatestValue = "unlocked"
  37                 }
  38                 locks.add(new Lock(sendEvent,id, label, displayName, this.lockState, this.lockLatestValue))
  39         }
  40
  41         //By Apps
  42         def lock() {
  43                 if (lockState != "locked") {
  44                         //lockLatestValue = lockState
  45                         lockLatestValue = "locked"
  46                         lockState = "locked"
  47                         currentLock = "locked"
  48                         locks[0].lock()
  49                 }
  50         }
  51
  52         def lock(LinkedHashMap metaData) {
  53                 if (lockState != "locked") {
  54                         def task = timers.runAfter(metaData["delay"]) {
  55                                 //lockLatestValue = lockState
  56                                 lockLatestValue = "locked"
  57                                 lockState = "locked"
  58                                 currentLock = "locked"
  59                                 locks[0].lock()
  60                         }
  61                 }
  62         }
  63
  64         def unlock() {
  65                 if (lockState != "unlocked") {
  66                         //lockLatestValue = lockState
  67                         lockLatestValue = "unlocked"
  68                         lockState = "unlocked"
  69                         currentLock = "unlocked"
  70                         locks[0].unlock()
  71                 }
  72         }
  73
  74
  75         def unlock(LinkedHashMap metaData) {
  76                 if (lockState != "unlocked") {
  77                         def task = timers.runAfter(metaData["delay"]) {
  78                                 //lockLatestValue = lockState
  79                                 lockLatestValue = "unlocked"
  80                                 lockState = "unlocked"
  81                                 currentLock = "unlocked"
  82                                 locks[0].unlock()
  83                         }
  84                 }
  85         }
  86
  87         //Methods for closures
  88         def count(Closure Input) {
  89                 locks.count(Input)
  90         }
  91         def size() {
  92                 locks.size()
  93         }
  94         def each(Closure Input) {
  95                 locks.each(Input)
  96         }
  97         def find(Closure Input) {
  98                 locks.find(Input)
  99         }
 100         def sort(Closure Input) {
 101                 locks.sort(Input)
 102         }
 103         def collect(Closure Input) {
 104                 locks.collect(Input)
 105         }
 106
 107         //By Model Checker
 108         def setValue(LinkedHashMap eventDataMap) {
 109                 if (eventDataMap["value"] != locks[0].lockState) {
 110                         locks[0].setValue(eventDataMap["value"])
 111                         this.lockState = locks[0].lockState
 112                         this.currentLock = locks[0].lockState
 113                         this.lockLatestValue = locks[0].lockLatestValue
 114                         sendEvent(eventDataMap)
 115                 }
 116         }
 117
 118         def currentValue(String deviceFeature) {
 119                 locks[0].currentValue(deviceFeature)
 120         }
 121
 122         def latestValue(String deviceFeature) {
 123                 locks[0].latestValue(deviceFeature)
 124         }
 125
 126         def getAt(int ix) {
 127                 locks[ix]
 128         }
 129 }
 130