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                 contacts.add(new ContactSensor(id, label, displayName, this.contactState, this.currentContact, this.alarmState, this.latestValue))
  29         }
  30
  31         //Methods for closures
  32         def count(Closure Input) {
  33                 contacts.count(Input)
  34         }
  35         def size() {
  36                 contacts.size()
  37         }
  38         def each(Closure Input) {
  39                 contacts.each(Input)
  40         }
  41         def find(Closure Input) {
  42                 contacts.find(Input)
  43         }
  44         def sort(Closure Input) {
  45                 contacts.sort(Input)
  46         }
  47         def collect(Closure Input) {
  48                 contacts.collect(Input)
  49         }
  50
  51         //By Model Checker
  52         def setValue(LinkedHashMap eventDataMap) {
  53                 if (eventDataMap["value"] != contacts[0].contactState) {
  54                         this.latestValue = eventDataMap["value"]
  55                         this.contactState = eventDataMap["value"]
  56                         this.currentContact = eventDataMap["value"]
  57                         contacts[0].setValue(eventDataMap["value"])
  58                         sendEvent(eventDataMap)
  59                 }
  60         }
  61
  62         def on() {
  63                 this.alarmState = "armed"
  64                 contacts[0].on()
  65         }
  66
  67         def off() {
  68                 this.alarmState = "not armed"
  69                 contacts[0].off()
  70         }
  71
  72         def currentValue(String deviceFeature) {
  73                 contacts[0].currentValue(deviceFeature)//It is called if we have only one device
  74         }
  75
  76         def currentState(String deviceFeature) {
  77                 contacts[0].currentState(deviceFeature)//It is called if we have only one device
  78         }
  79
  80         def latestValue(String deviceFeature) {
  81                 contacts[0].latestValue(deviceFeature)//It is called if we have only one device
  82         }
  83
  84         def getAt(int ix) {
  85                 contacts[ix]
  86         }
  87 }