package SmokeDetector
import Timer.SimulatedTimer
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
public class SmokeDetectors {
private int deviceNumbers
private List smokeDetectors
private String currentCarbonMonoxideValue = "clear"
private String carbonMonoxideLatestValue = "clear"
private int battery = 50
+ private int batteryValue = 50
private int batteryLatestValue = 50
- SmokeDetectors(Closure sendEvent, int deviceNumbers) {
+ SmokeDetectors(Closure sendEvent, int deviceNumbers, boolean init) {
this.sendEvent = sendEvent
this.deviceNumbers = deviceNumbers
this.smokeDetectors = []
-<<<<<<< HEAD
- def initBattery = Verify.getIntFromList(30, 50, 70)
- this.battery = initBattery
- this.batteryLatestValue = initBattery
-
- def initSmoke = Verify.getInt(0,2)
- if (initSmoke == 0) {
-=======
- /*def init = Verify.getInt(0,2)
- if (init == 0) {
->>>>>>> a02c9807815a35c0f57241ee6510a3d312499049
+ if (init) {
this.currentSmokeValue = "clear"
this.smokeLatestValue = "clear"
- } else if (initSmoke == 1) {
- this.currentSmokeValue = "detected"
- this.smokeLatestValue = "detected"
- } else {
- this.currentSmokeValue = "tested"
- this.smokeLatestValue = "tested"
-<<<<<<< HEAD
- }
-
- def initCarbonMonoxide = Verify.getInt(0,2)
- if (initCarbonMonoxide == 0) {
+ this.carbonMonoxide = "clear"
this.currentCarbonMonoxideValue = "clear"
this.carbonMonoxideLatestValue = "clear"
- } else if (initCarbonMonoxide == 1) {
+ this.battery = 50
+ this.batteryValue = 50
+ this.batteryLatestValue = 50
+ } else {
+ this.currentSmokeValue = "detected"
+ this.smokeLatestValue = "detected"
+ this.carbonMonoxide = "detected"
this.currentCarbonMonoxideValue = "detected"
this.carbonMonoxideLatestValue = "detected"
- } else {
- this.currentCarbonMonoxideValue = "tested"
- this.carbonMonoxideLatestValue = "tested"
+ this.battery = 60
+ this.batteryValue = 60
+ this.batteryLatestValue = 60
}
- smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue, this.currentCarbonMonoxideValue,
- this.carbonMonoxideLatestValue, this.battery))
-=======
- }*/
- smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue))
->>>>>>> a02c9807815a35c0f57241ee6510a3d312499049
+ smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue, this.carbonMonoxide, this.carbonMonoxideLatestValue, this.battery))
}
//By Model Checker