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 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 = []
- /*def init = Verify.getInt(0,2)
- if (init == 0) {
+ 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"
- }
-
- 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.carbonMonoxideValue, this.batteryValue))
+ smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue, this.carbonMonoxide, this.carbonMonoxideLatestValue, this.battery))
}
//By Model Checker