ContactSensor/ContactSensors.groovy

   1 //Create a class for contact sensor
   2 package ContactSensor
   3 import Timer.SimulatedTimer
   4
   5 //JPF's Verify API
   6 import gov.nasa.jpf.vm.Verify
   7
   8 public class ContactSensors {
   9         private int deviceNumbers
  10         private List contacts
  11         def sendEvent
  12
  13         //For one device(We cannot have obj.id)-> We should have obj[0].id
  14         private String id = "contactSensorID0"
  15         private String label = "contactSensor0"
  16         private String displayName = "contactSensor0"
  17         private String contactState = "closed"
  18         private String currentContact = "closed"
  19         private String latestValue = "closed"
  20         private String alarmState = "armed"
  21
  22
  23         ContactSensors(Closure sendEvent, int deviceNumbers) {
  24                 this.sendEvent = sendEvent
  25                 this.deviceNumbers = deviceNumbers
  26                 this.contacts = []
  27
  28                 /*def initSensor = Verify.getBoolean()
  29                 if (initSensor) {
  30                         this.contactState = "closed"
  31                         this.currentContact = "closed"
  32                         this.latestValue = "closed"
  33                 } else {
  34                         this.contactState = "open"
  35                         this.currentContact = "open"
  36                         this.latestValue = "open"
  37                 }
  38
  39                 def initAlarm = Verify.getBoolean()
  40                 if (initAlarm) {
  41                         this.alarmState = "armed"
  42                 } else {
  43                         this.alarmState = "not armed"
  44                 }*/
  45                 contacts.add(new ContactSensor(id, label, displayName, this.contactState, this.currentContact, this.alarmState, this.latestValue))
  46         }
  47
  48         //Methods for closures
  49         def count(Closure Input) {
  50                 contacts.count(Input)
  51         }
  52         def size() {
  53                 contacts.size()
  54         }
  55         def each(Closure Input) {
  56                 contacts.each(Input)
  57         }
  58         def find(Closure Input) {
  59                 contacts.find(Input)
  60         }
  61         def sort(Closure Input) {
  62                 contacts.sort(Input)
  63         }
  64         def collect(Closure Input) {
  65                 contacts.collect(Input)
  66         }
  67
  68         //By Model Checker
  69         def setValue(LinkedHashMap eventDataMap) {
  70                 if (eventDataMap["value"] != contacts[0].contactState) {
  71                         this.latestValue = eventDataMap["value"]
  72                         this.contactState = eventDataMap["value"]
  73                         this.currentContact = eventDataMap["value"]
  74                         contacts[0].setValue(eventDataMap["value"])
  75                         sendEvent(eventDataMap)
  76                 }
  77         }
  78
  79         def on() {
  80                 this.alarmState = "armed"
  81                 contacts[0].on()
  82         }
  83
  84         def off() {
  85                 this.alarmState = "not armed"
  86                 contacts[0].off()
  87         }
  88
  89         def currentValue(String deviceFeature) {
  90                 contacts[0].currentValue(deviceFeature)//It is called if we have only one device
  91         }
  92
  93         def currentState(String deviceFeature) {
  94                 contacts[0].currentState(deviceFeature)//It is called if we have only one device
  95         }
  96
  97         def latestValue(String deviceFeature) {
  98                 contacts[0].latestValue(deviceFeature)//It is called if we have only one device
  99         }
 100
 101         def getAt(int ix) {
 102                 contacts[ix]
 103         }
 104 }