1 //Create a class for smoke detector
3 import Timer.SimulatedTimer
6 import gov.nasa.jpf.vm.Verify
8 public class SmokeDetectors {
9 private int deviceNumbers
10 private List smokeDetectors
13 //For one device(We cannot have obj.id)-> We should have obj[0].id
14 private String id = "smokeDetectorID0"
15 private String label = "smokeDetector0"
16 private String displayName = "smokeDetector0"
17 private String smoke = "clear"
18 private String currentSmokeValue = "clear"
19 private String smokeLatestValue = "clear"
20 private String carbonMonoxide = "clear"
21 private String currentCarbonMonoxideValue = "clear"
22 private String carbonMonoxideLatestValue = "clear"
23 private int battery = 50
24 private int batteryLatestValue = 50
27 SmokeDetectors(Closure sendEvent, int deviceNumbers) {
28 this.sendEvent = sendEvent
29 this.deviceNumbers = deviceNumbers
30 this.smokeDetectors = []
32 /*def init = Verify.getInt(0,2)
34 this.currentSmokeValue = "clear"
35 this.smokeLatestValue = "clear"
36 } else if (initSmoke == 1) {
37 this.currentSmokeValue = "detected"
38 this.smokeLatestValue = "detected"
40 this.currentSmokeValue = "tested"
41 this.smokeLatestValue = "tested"
44 def initCarbonMonoxide = Verify.getInt(0,2)
45 if (initCarbonMonoxide == 0) {
46 this.currentCarbonMonoxideValue = "clear"
47 this.carbonMonoxideLatestValue = "clear"
48 } else if (initCarbonMonoxide == 1) {
49 this.currentCarbonMonoxideValue = "detected"
50 this.carbonMonoxideLatestValue = "detected"
52 this.currentCarbonMonoxideValue = "tested"
53 this.carbonMonoxideLatestValue = "tested"
56 smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue))
60 def setValue(LinkedHashMap eventDataMap) {
61 if (eventDataMap["name"].contains("smoke")) {
62 if (eventDataMap["value"] != smokeDetectors[0].currentSmokeValue) {
63 this.smokeLatestValue = eventDataMap["value"]
64 this.smoke = eventDataMap["value"]
65 this.currentSmokeValue = eventDataMap["value"]
66 smokeDetectors[0].setValue(eventDataMap["value"], eventDataMap["name"])
67 sendEvent(eventDataMap)
69 } else if (eventDataMap["name"].contains("carbonMonoxide")) {
70 if (eventDataMap["value"] != smokeDetectors[0].currentCarbonMonoxideValue) {
71 this.carbonMonoxideLatestValue = eventDataMap["value"]
72 this.carbonMonoxide = eventDataMap["value"]
73 this.currentCarbonMonoxideValue = eventDataMap["value"]
74 smokeDetectors[0].setValue(eventDataMap["value"], eventDataMap["name"])
75 sendEvent(eventDataMap)
77 } else if (eventDataMap["name"].contains("battery")) {
78 if (eventDataMap["value"].toInteger() != smokeDetectors[0].battery) {
79 this.battery = eventDataMap["value"].toInteger()
80 this.batteryLatestValue = eventDataMap["value"].toInteger()
81 smokeDetectors[0].setValue(eventDataMap["value"], eventDataMap["name"])
82 sendEvent(eventDataMap)
87 //Methods for closures
88 def count(Closure Input) {
89 smokeDetectors.count(Input)
94 def each(Closure Input) {
95 smokeDetectors.each(Input)
97 def find(Closure Input) {
98 smokeDetectors.find(Input)
100 def sort(Closure Input) {
101 smokeDetectors.sort(Input)
103 def collect(Closure Input) {
104 smokeDetectors.collect(Input)
108 def currentValue(String deviceFeature) {
109 smokeDetectors[0].currentValue(deviceFeature)//It is called if we have only one device
112 def latestValue(String deviceFeature) {
113 smokeDetectors[0].latestValue(deviceFeature)//It is called if we have only one device