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 collect(Closure Input) {
  62                 contacts.collect(Input)
  63         }
  64
  65         //By Model Checker
  66         def setValue(LinkedHashMap eventDataMap) {
  67                 if (eventDataMap["value"] != contacts[0].contactState) {
  68                         contacts[0].setValue(eventDataMap["value"])
  69                         this.latestValue = contacts[0].latestValue
  70                         this.contactState = contacts[0].contactState
  71                         this.currentContact = contacts[0].contactState
  72                         sendEvent(eventDataMap)
  73                 }
  74         }
  75
  76         def on() {
  77                 contacts[0].on()
  78                 this.alarmState = "armed"
  79         }
  80
  81         def off() {
  82                 contacts[0].off()
  83                 this.alarmState = "not armed"
  84         }
  85
  86         def currentValue(String deviceFeature) {
  87                 contacts[0].currentValue(deviceFeature)//It is called if we have only one device
  88         }
  89
  90         def latestValue(String deviceFeature) {
  91                 contacts[0].latestValue(deviceFeature)//It is called if we have only one device
  92         }
  93
  94         def getAt(int ix) {
  95                 contacts[ix]
  96         }
  97 }