//Create a class for thermostat device
package Thermostat
import Timer.SimulatedTimer

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

public class Thermostats{
	int deviceNumbers	
	List thermostats	
	def sendEvent	
	def timers

	//When we have only one device
	private String id = "thermostatID0"
	private String label = "thermostat0"
	private String displayName = "thermostat0"
	private int temperature = 66
	private int currentCoolingSetpoint = 70
	private int currentHeatingSetpoint = 50
	private int coolingSetpoint = 70
	private int thermostatSetpoint = 60
	private int heatingSetpoint = 50
	private coolingSetpointRange = [70, 90]
	private thermostatSetpointRange = [50, 70]
	private heatingSetpointRange = [20, 50]
	private supportedThermostatFanModes = ["auto", "fanCirculate", "circulate", "fanOn", "on"]
	private supportedThermostatModes = ["auto", "cool", "emergencyHeat", "heat", "off"]
	private String thermostatOperatingState = "cooling"
	private String thermostatFanMode = "auto"
	private String thermostatMode = "auto"
	private String currentThermostatMode = "auto"
	private String climateName = ""

	Thermostats(Closure sendEvent, int deviceNumbers) {
		this.sendEvent = sendEvent
		this.timers = new SimulatedTimer()
		this.deviceNumbers = deviceNumbers
		this.thermostats = []

		def initTemperature = Verify.getIntFromList(60, 66, 70)
		this.temperature = initTemperature
		
		def initCoolingSetpoint = Verify.getIntFromList(70, 80, 90)
		this.currentCoolingSetpoint = initCoolingSetpoint
		this.coolingSetpoint = initCoolingSetpoint
		
		def initHeatingSetpoint = Verify.getIntFromList(20, 35, 50)
		this.currentHeatingSetpoint = initHeatingSetpoint
		this.heatingSetpoint = initHeatingSetpoint
		
		def initThermostatSetpoint = Verify.getIntFromList(50, 60, 70)
		this.thermostatSetpoint = initThermostatSetpoint
		
		def initFanMode = Verify.getInt(0,4)
		if (initFanMode == 0) {
			this.thermostatFanMode = "auto"
		} else if (initFanMode == 1) {
			this.thermostatFanMode = "fanCirculate"
		} else if (initFanMode == 2) {
			this.thermostatFanMode = "circulate"
		} else if (initFanMode == 3) {
			this.thermostatFanMode = "fanOn"
		} else {
			this.thermostatFanMode = "on"
		}

		def initMode = Verify.getInt(0,4)
		if (initMode == 0) {
			this.thermostatMode = "auto"
			this.currentThermostatMode = "auto"
		} else if (initMode == 1) {
			this.thermostatMode = "cool"
			this.currentThermostatMode = "cool"
		} else if (initMode == 2) {
			this.thermostatMode = "emergencyHeat"
			this.currentThermostatMode = "emergencyHeat"
		} else if (initMode == 3) {
			this.thermostatMode = "heat"
			this.currentThermostatMode = "heat"
		} else {
			this.thermostatMode = "off"
			this.currentThermostatMode = "off"
		}

		thermostats.add(new Thermostat(sendEvent, id, label, displayName, this.temperature, this.currentCoolingSetpoint, 
                                               this.currentHeatingSetpoint, this.coolingSetpoint, this.thermostatSetpoint, this.heatingSetpoint, this.coolingSetpointRange,
                                               this.thermostatSetpointRange, this.heatingSetpointRange, this.supportedThermostatFanModes, this.supportedThermostatModes,
                                               this.thermostatOperatingState, this.thermostatFanMode,  this.thermostatMode, this.climateName))
	}

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

	//By Apps
	def setCoolingSetpoint(int coolingSetpoint) {
		if (coolingSetpoint != this.coolingSetpoint) {
			thermostats[0].setCoolingSetpoint(coolingSetpoint)
			this.currentCoolingSetpoint = coolingSetpoint
			this.coolingSetpoint = coolingSetpoint
		}
	}

	def setHeatingSetpoint(int heatingSetpoint) {
		if (heatingSetpoint != this.heatingSetpoint) {
			thermostats[0].setHeatingSetpoint(heatingSetpoint)
			this.currentHeatingSetpoint = heatingSetpoint
			this.heatingSetpoint = heatingSetpoint
		}
	}

	def setSchedule() {
		//Not implemented yet
	}

	def setThermostatFanMode(String thermostatFanMode) {
		if (thermostatFanMode != this.thermostatFanMode) {
			thermostats[0].setThermostatFanMode(thermostatFanMode)
			this.thermostatFanMode = thermostatFanMode
		}
	}

	def setThermostatMode(String thermostatMode) {
		if (thermostatMode != this.thermostatMode) {
			thermostats[0].setThermostatMode(thermostatMode)
			this.thermostatMode = thermostatMode
			this.currentThermostatMode = currentThermostatMode
		}
	}

	def cool() {
		if (thermostatMode != "cool") {
			thermostats[0].cool()
			this.thermostatMode = "cool"
			this.currentThermostatMode = "cool"
		}
	}

	def heat() {
		if (thermostatMode != "heat") {
			thermostats[0].heat()
			this.thermostatMode = "heat"
			this.currentThermostatMode = "heat"
		}
	}

	def auto() {
		if (thermostatMode != "auto") {
			thermostats[0].auto()
			this.thermostatMode = "auto"
			this.currentThermostatMode = "auto"
		}
	}

	def off() {
		if (thermostatMode != "off") {
			thermostats[0].off()
			this.thermostatMode = "off"
			this.currentThermostatMode = "off"
		}
	}

	def setClimate(String info, String givenClimateName) {
		if (givenClimateName != climateName) {
			thermostats[0].setClimate(info, givenClimateName)
			this.climateName = givenClimateName
		}
	}

	def setHold(String info1, int coolingSetpoint, int heatingSetpoint, String info2, String info3) {
		if ((coolingSetpoint != this.coolingSetpoint) || (heatingSetpoint != this.heatingSetpoint)) {
			thermostats[0].setHold(info1, coolingSetpoint, heatingSetpoint, info2, info3)
			this.currentCoolingSetpoint = coolingSetpoint
			this.coolingSetpoint = coolingSetpoint
			this.currentHeatingSetpoint = heatingSetpoint
			this.heatingSetpoint = heatingSetpoint
		}
	}

	//By Model Checker
	def setValue(LinkedHashMap eventDataMap) {
		if (eventDataMap["name"] == "temperature") {
			if (eventDataMap["value"] != thermostats[0].temperature) {
				thermostats[0].setValue(eventDataMap["value"], "temperature")
				this.temperature = thermostats[0].temperature
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "heatingSetpoint") {
			if (eventDataMap["value"] != thermostats[0].heatingSetpoint) {
				thermostats[0].setValue(eventDataMap["value"], "heatingSetpoint")
				this.heatingSetpoint = thermostats[0].heatingSetpoint
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "coolingSetpoint") {
			if (eventDataMap["value"] != thermostats[0].coolingSetpoint) {
				thermostats[0].setValue(eventDataMap["value"], "coolingSetpoint")
				this.coolingSetpoint = thermostats[0].coolingSetpoint
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "thermostatSetpoint") {
			if (eventDataMap["value"] != thermostats[0].thermostatSetpoint) {
				thermostats[0].setValue(eventDataMap["value"], "thermostatSetpoint")
				this.thermostatSetpoint = thermostats[0].thermostatSetpoint
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "thermostatMode") {
			if (eventDataMap["value"] != thermostats[0].thermostatMode) {
				thermostats[0].setValue(eventDataMap["value"], "thermostatMode")
				this.thermostatMode = thermostats[0].thermostatMode
				this.currentThermostatMode = thermostats[0].currentThermostatMode
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "thermostatFanMode") {
			if (eventDataMap["value"] != thermostats[0].thermostatFanMode) {
				thermostats[0].setValue(eventDataMap["value"], "thermostatFanMode")
				this.thermostatFanMode = thermostats[0].thermostatFanMode
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "thermostatOperatingState") {
			if (eventDataMap["value"] != thermostats[0].thermostatOperatingState) {
				thermostats[0].setValue(eventDataMap["value"], "thermostatOperatingState")
				this.thermostatOperatingState = thermostats[0].thermostatOperatingState
				sendEvent(eventDataMap)
			}
		}
	}

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