//Create a class for smoke detector
package SmokeDetector
import Timer.SimulatedTimer

//JPF's Verify API
import gov.nasa.jpf.vm.Verify

public class SmokeDetectors {
	private int deviceNumbers
	private List smokeDetectors
	def sendEvent

	//For one device(We cannot have obj.id)-> We should have obj[0].id
	private String id = "smokeDetectorID0"
	private String label = "smokeDetector0"
	private String displayName = "smokeDetector0"
	private String smoke = "clear"
	private String currentSmokeValue = "clear"
	private String smokeLatestValue = "clear"
	private String carbonMonoxide = "clear"
	private String currentCarbonMonoxideValue = "clear"
	private String carbonMonoxideLatestValue = "clear"
	private int battery = 50
	private int batteryLatestValue = 50

		
	SmokeDetectors(Closure sendEvent, int deviceNumbers) {
		this.sendEvent = sendEvent		
		this.deviceNumbers = deviceNumbers
		this.smokeDetectors = []

		/*def init = Verify.getInt(0,2)
		if (init == 0) {
			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.currentCarbonMonoxideValue = "clear"
			this.carbonMonoxideLatestValue = "clear"
		} else if (initCarbonMonoxide == 1) {
			this.currentCarbonMonoxideValue = "detected"
			this.carbonMonoxideLatestValue = "detected"
		} else {
			this.currentCarbonMonoxideValue = "tested"
			this.carbonMonoxideLatestValue = "tested"		
		}
		}*/
		smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue, this.carbonMonoxide, this.carbonMonoxideLatestValue, this.battery))
	}

	//By Model Checker
	def setValue(LinkedHashMap eventDataMap) {
		if (eventDataMap["name"].contains("smoke")) {
			if (eventDataMap["value"] != smokeDetectors[0].currentSmokeValue) {
				this.smokeLatestValue = eventDataMap["value"]
				this.smoke = eventDataMap["value"]
				this.currentSmokeValue = eventDataMap["value"]
				smokeDetectors[0].setValue(eventDataMap["value"], eventDataMap["name"])
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"].contains("carbonMonoxide")) {
			if (eventDataMap["value"] != smokeDetectors[0].currentCarbonMonoxideValue) {
				this.carbonMonoxideLatestValue = eventDataMap["value"]
				this.carbonMonoxide = eventDataMap["value"]
				this.currentCarbonMonoxideValue = eventDataMap["value"]
				smokeDetectors[0].setValue(eventDataMap["value"], eventDataMap["name"])
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"].contains("battery")) {
			if (eventDataMap["value"].toInteger() != smokeDetectors[0].battery) {
				this.battery = eventDataMap["value"].toInteger()
				this.batteryLatestValue = eventDataMap["value"].toInteger()
				smokeDetectors[0].setValue(eventDataMap["value"], eventDataMap["name"])
				sendEvent(eventDataMap)
			}
		}
	}

	//Methods for closures
	def count(Closure Input) {
		smokeDetectors.count(Input)
	}
	def size() {
		smokeDetectors.size()
	}
	def each(Closure Input) {
		smokeDetectors.each(Input)
	}
	def find(Closure Input) {
		smokeDetectors.find(Input)
	}
	def sort(Closure Input) {
		smokeDetectors.sort(Input)
	}
	def collect(Closure Input) {
		smokeDetectors.collect(Input)
	}


	def currentValue(String deviceFeature) {
		smokeDetectors[0].currentValue(deviceFeature)//It is called if we have only one device
	}

	def latestValue(String deviceFeature) {
		smokeDetectors[0].latestValue(deviceFeature)//It is called if we have only one device
	}

	def getAt(int ix) {
		smokeDetectors[ix]
	}
}