//Create a class for music player
package MusicPlayer
import Timer.SimulatedTimer

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

public class MusicPlayers {
	private int deviceNumbers
	private List musicPlayers
	def sendEvent

	//For one device(We cannot have obj.id)-> We should have obj[0].id
	private String id = "musicPlayerID0"
	private String label = "musicPlayer0"
	private String displayName = "musicPlayer0"
	private int level = 20
	private String mute = "unmuted"
	private String status = "paused"
	private int trackNumber = 1
	private String trackData = "someTrack"
	private String trackDescription = "someDescriptions"

	
		
	MusicPlayers(Closure sendEvent, int deviceNumbers) {
		this.sendEvent = sendEvent
		this.deviceNumbers = deviceNumbers
		this.musicPlayers = []

		def initLevel = Verify.getIntFromList(10, 20, 30)
		this.level = initLevel
		def initMute = Verify.getBoolean()
		if (initMute) {
			this.mute = "unmuted"
		} else {
			this.mute = "mute"
		}
		def initStatus = Verify.getBoolean()
		if (initStatus) {
			this.status = "paused"
		} else {
			this.status = "playing"
		}

		musicPlayers.add(new MusicPlayer(id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription))
	}

	//By model checker
	def setValue(LinkedHashMap eventDataMap) {
		if (eventDataMap["name"] == "status") {
			if (eventDataMap["value"] != musicPlayers[0].status) {
				musicPlayers[0].setValue(eventDataMap["value"], "status")
				this.status = musicPlayers[0].status
				sendEvent(eventDataMap)
			}	
		} else if (eventDataMap["name"] == "level") {
			if (eventDataMap["value"] != musicPlayers[0].level) {
				musicPlayers[0].setValue(eventDataMap["value"], "level")
				this.level = musicPlayers[0].level
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "trackDescription") {
			if (eventDataMap["value"] != musicPlayers[0].trackDescription) {
				musicPlayers[0].setValue(eventDataMap["value"], "trackDescription")
				this.trackDescription = musicPlayers[0].trackDescription
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "trackData") {
			if (eventDataMap["value"] != musicPlayers[0].trackData) {
				musicPlayers[0].setValue(eventDataMap["value"], "trackData")
				this.trackData = musicPlayers[0].trackData
				sendEvent(eventDataMap)
			}
		} else if (eventDataMap["name"] == "mute") {
			if (eventDataMap["value"] != musicPlayers[0].mute) {
				musicPlayers[0].setValue(eventDataMap["value"], "mute")
				this.mute = musicPlayers[0].mute
				sendEvent(eventDataMap)
			}
		}
	}

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

	//methods
	def mute() {
		if (mute != "muted") {
			musicPlayers[0].mute()
			this.mute = "muted"
		}
	}
	def nextTrack() {
		musicPlayers[0].nextTrack()
		if (status != "playing") {
			this.status = "playing"
		}
		this.trackNumber = musicPlayers[0].trackNumber
	}
	def pause() {
		if (status != "paused") {
			musicPlayers[0].pause()
			this.status = "paused"
		}
	}
	def play() {
		if (status != "playing") {
			musicPlayers[0].play()
			this.status = "playing"
		}
	}
	def playTrack(String trackToPlay) {
		musicPlayers[0].playTrack(trackToPlay)
		if (status != "playing") {
			this.status = "playing"
		}
		this.trackNumber = musicPlayers[0].trackNumber
	}
	def previousTrack() {
		musicPlayers[0].previousTrack()
		if (status != "playing") {
			this.status = "playing"
		}
		this.trackNumber = musicPlayers[0].trackNumber
	}
	def restoreTrack(String trackToRestore) {
		musicPlayers[0].restoreTrack(trackToRestore)
	}
	def resumeTrack(String trackToResume) {
		musicPlayers[0].resumeTrack(trackToResume)
		if (status != "playing") {
			this.status = "playing"
		}
	}
	def setLevel(int level) {
		if (level != this.level) {		
			musicPlayers[0].setLevel(level)
			this.level = level
		}
	}
	def setTrack(String trackToSet) {
		musicPlayers[0].setTrack(trackToSet)
		if (status != "playing") {
			this.status = "playing"
		}
		this.trackNumber = musicPlayers[0].trackNumber
	}
	def stop() {
		if (status != "stopped") {
			musicPlayers[0].stop()
			this.status = "stopped"
		}
	}

	def currentValue(String deviceFeature) {
		musicPlayers[0].currentValue(deviceFeature)
	}

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