SwitchLevel/SwitchLevels.groovy

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