X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=MusicPlayer%2FMusicPlayers.groovy;h=c2d8b75dda55204f5742f4e6e637a5004931eea3;hb=9a9f34091fe2231e5f0010987ac3a24800aaae78;hp=9968595e27ba6fa88bb7cbac2261c262aa4e0f34;hpb=2c464dd719752b34106af7eb1e7451e6e03072f6;p=smartthings-infrastructure.git

diff --git a/MusicPlayer/MusicPlayers.groovy b/MusicPlayer/MusicPlayers.groovy
index 9968595..c2d8b75 100644
--- a/MusicPlayer/MusicPlayers.groovy
+++ b/MusicPlayer/MusicPlayers.groovy
@@ -2,6 +2,8 @@
 package MusicPlayer
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
 
 public class MusicPlayers {
 	private int deviceNumbers
@@ -14,9 +16,10 @@ public class MusicPlayers {
 	private String displayName = "musicPlayer0"
 	private int level = 20
 	private String mute = "unmuted"
-	private String status = "pause"
-	private int trackNumber = 0
-	private List trackData = ["track1", "track2", "track3", "track4"]
+	private String status = "paused"
+	private int trackNumber = 1
+	private String trackData = "someTrack"
+	private String trackDescription = "someDescriptions"
 
 	
 		
@@ -25,7 +28,72 @@ public class MusicPlayers {
 		this.deviceNumbers = deviceNumbers
 		this.musicPlayers = []
 
-		musicPlayers.add(new MusicPlayer(id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData))
+		/*def initLevel = Verify.getIntFromList(10, 20, 30)
+		this.level = initLevel
+		def initMute = Verify.getBoolean()
+		if (initMute) {
+			this.mute = "unmuted"
+		} else {
+			this.mute = "muted"
+		}
+		def initStatus = Verify.getInt(0,2)
+		if (initStatus == 0) {
+			this.status = "paused"
+		} else if (initStatus == 1) {
+			this.status = "playing"
+		} else {
+			this.status = "stopped"
+		}
+		def initTrack = Verify.getIntFromList(1, 2, 3)
+		this.trackNumber = initTrack 
+		def initData = Verify.getBoolean()
+		if (initData) {
+			this.trackData = "someTrack"
+		} else {
+			this.trackData = "someOtherTrack"
+		}
+		def initDesc = Verify.getBoolean()
+		if (initDesc) {
+			this.trackDescription = "someDescriptions"
+		} else {
+			this.trackDescription = "someOtherDescriptions"
+		}*/
+		musicPlayers.add(new MusicPlayer(sendEvent, 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) {
+				this.status = eventDataMap["value"]
+				musicPlayers[0].setValue(eventDataMap["value"], "status")
+				sendEvent(eventDataMap)
+			}	
+		} else if (eventDataMap["name"] == "level") {
+			if (eventDataMap["value"].toInteger() != musicPlayers[0].level) {
+				this.level = eventDataMap["value"].toInteger()
+				musicPlayers[0].setValue(eventDataMap["value"], "level")
+				sendEvent(eventDataMap)
+			}
+		} else if (eventDataMap["name"] == "trackDescription") {
+			if (eventDataMap["value"] != musicPlayers[0].trackDescription) {
+				this.trackDescription = eventDataMap["value"]
+				musicPlayers[0].setValue(eventDataMap["value"], "trackDescription")
+				sendEvent(eventDataMap)
+			}
+		} else if (eventDataMap["name"] == "trackData") {
+			if (eventDataMap["value"] != musicPlayers[0].trackData) {
+				this.trackData = eventDataMap["value"]
+				musicPlayers[0].setValue(eventDataMap["value"], "trackData")				
+				sendEvent(eventDataMap)
+			}
+		} else if (eventDataMap["name"] == "mute") {
+			if (eventDataMap["value"] != musicPlayers[0].mute) {
+				this.mute = eventDataMap["value"]
+				musicPlayers[0].setValue(eventDataMap["value"], "mute")
+				sendEvent(eventDataMap)
+			}
+		}
 	}
 
 	//Methods for closures
@@ -41,49 +109,95 @@ public class MusicPlayers {
 	def find(Closure Input) {
 		musicPlayers.find(Input)
 	}
+	def sort(Closure Input) {
+		musicPlayers.sort(Input)
+	}
 	def collect(Closure Input) {
 		musicPlayers.collect(Input)
 	}
 
 	//methods
 	def mute() {
-		musicPlayers[0].mute()
+		if (mute != "muted") {
+			this.mute = "muted"
+			musicPlayers[0].mute()
+		}
 	}
 	def nextTrack() {
+		if (status != "playing") {
+			this.status = "playing"
+		}
+		this.trackNumber = this.trackNumber+1
 		musicPlayers[0].nextTrack()
 	}
 	def pause() {
-		musicPlayers[0].pause()
+		if (status != "paused") {
+			this.status = "paused"
+			musicPlayers[0].pause()			
+		}
 	}
 	def play() {
-		musicPlayers[0].play()
+		if (status != "playing") {
+			this.status = "playing"
+			musicPlayers[0].play()
+		}
 	}
 	def playTrack(String trackToPlay) {
+		if (status != "playing") {
+			this.status = "playing"
+		}
 		musicPlayers[0].playTrack(trackToPlay)
 	}
 	def previousTrack() {
+		if (status != "playing") {
+			this.status = "playing"
+		}
+		if (this.trackNumber != 1)
+			this.trackNumber = this.trackNumber-1
 		musicPlayers[0].previousTrack()
 	}
 	def restoreTrack(String trackToRestore) {
 		musicPlayers[0].restoreTrack(trackToRestore)
 	}
 	def resumeTrack(String trackToResume) {
+		if (status != "playing") {
+			this.status = "playing"
+		}
 		musicPlayers[0].resumeTrack(trackToResume)
 	}
 	def setLevel(int level) {
-		musicPlayers[0].setLevel(level)
+		if (level != this.level) {
+			this.level = level	
+			musicPlayers[0].setLevel(level)
+		}
 	}
 	def setTrack(String trackToSet) {
+		if (status != "playing") {
+			this.status = "playing"
+		}
 		musicPlayers[0].setTrack(trackToSet)
 	}
 	def stop() {
-		musicPlayers[0].stop()
+		if (status != "stopped") {
+			this.status = "stopped"
+			musicPlayers[0].stop()
+		}
+	}
+	def playText(String text) {
+		if (status != "playing") {
+			this.status = "playing"
+		}
+		musicPlayers[0].playText(text)
 	}
 
 	def currentValue(String deviceFeature) {
 		musicPlayers[0].currentValue(deviceFeature)
 	}
 
+	def latestValue(String deviceFeature) {
+		musicPlayers[0].latestValue(deviceFeature)
+	}
+
 	def getAt(int ix) {
 		musicPlayers[ix]
 	}