//Create a class for carbon monoxide detector
package CarbonMonoxideDetector
import Timer.SimulatedTimer

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

public class CarbonMonoxideDetectors {
	private int deviceNumbers
	private List carbonMonoxideDetectors
	def sendEvent

	//For one device(We cannot have obj.id)-> We should have obj[0].id
	private String id = "carbonMonoxideDetectorID0"
	private String label = "carbonMonoxideDetector0"
	private String displayName = "carbonMonoxideDetector0"
	private String carbonMonoxide = "clear"
	private String currentCarbonMonoxideValue = "clear"
	private String carbonMonoxideLatestValue = "clear"

		
	CarbonMonoxideDetectors(Closure sendEvent, int deviceNumbers) {
		this.sendEvent = sendEvent		
		this.deviceNumbers = deviceNumbers
		this.carbonMonoxideDetectors = []
		
		def init = Verify.getInt(0,2)
		if (init == 0) {
			this.carbonMonoxide = "clear"
			this.carbonMonoxideLatestValue = "clear"
		} else if (init == 1) {
			this.carbonMonoxide = "detected"
			this.carbonMonoxideLatestValue = "detected"
		} else {
			this.carbonMonoxide = "tested"
			this.carbonMonoxideLatestValue = "tested"		
		}
		carbonMonoxideDetectors.add(new CarbonMonoxideDetector(id, label, displayName, this.carbonMonoxide, this.carbonMonoxideLatestValue))
	}

	//By Model Checker
	def setValue(LinkedHashMap eventDataMap) {
		if (eventDataMap["value"] != carbonMonoxideDetectors[0].currentCarbonMonoxideValue) {
			carbonMonoxideDetectors[0].setValue(eventDataMap["value"])
			this.carbonMonoxideLatestValue = carbonMonoxideDetectors[0].carbonMonoxideLatestValue
			this.carbonMonoxide = carbonMonoxideDetectors[0].currentCarbonMonoxideValue
			this.currentCarbonMonoxideValue = carbonMonoxideDetectors[0].currentCarbonMonoxideValue
			sendEvent(eventDataMap)
		}
	}

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


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

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

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