MusicPlayer/MusicPlayers.groovy

   1 //Create a class for music player
   2 package MusicPlayer
   3 import Timer.SimulatedTimer
   4
   5 //JPF's Verify API
   6 import gov.nasa.jpf.vm.Verify
   7
   8 public class MusicPlayers {
   9         private int deviceNumbers
  10         private List musicPlayers
  11         def sendEvent
  12
  13         //For one device(We cannot have obj.id)-> We should have obj[0].id
  14         private String id = "musicPlayerID0"
  15         private String label = "musicPlayer0"
  16         private String displayName = "musicPlayer0"
  17         private int level = 20
  18         private String mute = "unmuted"
  19         private String status = "paused"
  20         private int trackNumber = 1
  21         private String trackData = "someTrack"
  22         private String trackDescription = "someDescriptions"
  23
  24
  25
  26         MusicPlayers(Closure sendEvent, int deviceNumbers) {
  27                 this.sendEvent = sendEvent
  28                 this.deviceNumbers = deviceNumbers
  29                 this.musicPlayers = []
  30
  31                 def initLevel = Verify.getIntFromList(10, 20, 30)
  32                 this.level = initLevel
  33                 def initMute = Verify.getBoolean()
  34                 if (initMute) {
  35                         this.mute = "unmuted"
  36                 } else {
  37                         this.mute = "mute"
  38                 }
  39                 def initStatus = Verify.getBoolean()
  40                 if (initStatus) {
  41                         this.status = "paused"
  42                 } else {
  43                         this.status = "playing"
  44                 }
  45
  46                 musicPlayers.add(new MusicPlayer(sendEvent, id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription))
  47         }
  48
  49         //By model checker
  50         def setValue(LinkedHashMap eventDataMap) {
  51                 if (eventDataMap["name"] == "status") {
  52                         if (eventDataMap["value"] != musicPlayers[0].status) {
  53                                 this.status = eventDataMap["value"]
  54                                 musicPlayers[0].setValue(eventDataMap["value"], "status")
  55                                 sendEvent(eventDataMap)
  56                         }
  57                 } else if (eventDataMap["name"] == "level") {
  58                         if (eventDataMap["value"].toInteger() != musicPlayers[0].level) {
  59                                 this.level = eventDataMap["value"].toInteger()
  60                                 musicPlayers[0].setValue(eventDataMap["value"], "level")
  61                                 sendEvent(eventDataMap)
  62                         }
  63                 } else if (eventDataMap["name"] == "trackDescription") {
  64                         if (eventDataMap["value"] != musicPlayers[0].trackDescription) {
  65                                 this.trackDescription = eventDataMap["value"]
  66                                 musicPlayers[0].setValue(eventDataMap["value"], "trackDescription")
  67                                 sendEvent(eventDataMap)
  68                         }
  69                 } else if (eventDataMap["name"] == "trackData") {
  70                         if (eventDataMap["value"] != musicPlayers[0].trackData) {
  71                                 this.trackData = eventDataMap["value"]
  72                                 musicPlayers[0].setValue(eventDataMap["value"], "trackData")
  73                                 sendEvent(eventDataMap)
  74                         }
  75                 } else if (eventDataMap["name"] == "mute") {
  76                         if (eventDataMap["value"] != musicPlayers[0].mute) {
  77                                 this.mute = eventDataMap["value"]
  78                                 musicPlayers[0].setValue(eventDataMap["value"], "mute")
  79                                 sendEvent(eventDataMap)
  80                         }
  81                 }
  82         }
  83
  84         //Methods for closures
  85         def count(Closure Input) {
  86                 musicPlayers.count(Input)
  87         }
  88         def size() {
  89                 musicPlayers.size()
  90         }
  91         def each(Closure Input) {
  92                 musicPlayers.each(Input)
  93         }
  94         def find(Closure Input) {
  95                 musicPlayers.find(Input)
  96         }
  97         def sort(Closure Input) {
  98                 musicPlayers.sort(Input)
  99         }
 100         def collect(Closure Input) {
 101                 musicPlayers.collect(Input)
 102         }
 103
 104         //methods
 105         def mute() {
 106                 if (mute != "muted") {
 107                         this.mute = "muted"
 108                         musicPlayers[0].mute()
 109                 }
 110         }
 111         def nextTrack() {
 112                 if (status != "playing") {
 113                         this.status = "playing"
 114                 }
 115                 this.trackNumber = this.trackNumber+1
 116                 musicPlayers[0].nextTrack()
 117         }
 118         def pause() {
 119                 if (status != "paused") {
 120                         this.status = "paused"
 121                         musicPlayers[0].pause()
 122                 }
 123         }
 124         def play() {
 125                 if (status != "playing") {
 126                         this.status = "playing"
 127                         musicPlayers[0].play()
 128                 }
 129         }
 130         def playTrack(String trackToPlay) {
 131                 if (status != "playing") {
 132                         this.status = "playing"
 133                 }
 134                 musicPlayers[0].playTrack(trackToPlay)
 135         }
 136         def previousTrack() {
 137                 if (status != "playing") {
 138                         this.status = "playing"
 139                 }
 140                 if (this.trackNumber != 1)
 141                         this.trackNumber = this.trackNumber-1
 142                 musicPlayers[0].previousTrack()
 143         }
 144         def restoreTrack(String trackToRestore) {
 145                 musicPlayers[0].restoreTrack(trackToRestore)
 146         }
 147         def resumeTrack(String trackToResume) {
 148                 if (status != "playing") {
 149                         this.status = "playing"
 150                 }
 151                 musicPlayers[0].resumeTrack(trackToResume)
 152         }
 153         def setLevel(int level) {
 154                 if (level != this.level) {
 155                         this.level = level
 156                         musicPlayers[0].setLevel(level)
 157                 }
 158         }
 159         def setTrack(String trackToSet) {
 160                 if (status != "playing") {
 161                         this.status = "playing"
 162                 }
 163                 musicPlayers[0].setTrack(trackToSet)
 164         }
 165         def stop() {
 166                 if (status != "stopped") {
 167                         this.status = "stopped"
 168                         musicPlayers[0].stop()
 169                 }
 170         }
 171         def playText(String text) {
 172                 if (status != "playing") {
 173                         this.status = "playing"
 174                 }
 175                 musicPlayers[0].playText(text)
 176         }
 177
 178         def currentValue(String deviceFeature) {
 179                 musicPlayers[0].currentValue(deviceFeature)
 180         }
 181
 182         def latestValue(String deviceFeature) {
 183                 musicPlayers[0].latestValue(deviceFeature)
 184         }
 185
 186         def getAt(int ix) {
 187                 musicPlayers[ix]
 188         }
 189 }