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 initTrack = Verify.getIntFromList(1, 2, 3)
  34                 this.trackNumber = initTrack
  35                 def initMute = Verify.getBoolean()
  36                 if (initMute) {
  37                         this.mute = "unmuted"
  38                 } else {
  39                         this.mute = "mute"
  40                 }
  41                 def initStatus = Verify.getBoolean()
  42                 if (initStatus) {
  43                         this.status = "pause"
  44                 } else {
  45                         this.status = "play"
  46                 }
  47                 def initTrackData = Verify.getBoolean()
  48                 if (initTrackData) {
  49                         this.trackData = "someTrack"
  50                 } else {
  51                         this.trackData = "someOtherTrack"
  52                 }
  53                 def initTrackDesc = Verify.getBoolean()
  54                 if (initTrackDesc) {
  55                         this.trackDescription = "someDescriptions"
  56                 } else {
  57                         this.trackDescription = "someOtherDescriptions"
  58                 }
  59
  60                 def initLevel = Verify.getIntFromList(10, 20, 30)
  61                 this.level = initLevel
  62                 def initMute = Verify.getBoolean()
  63                 if (initMute) {
  64                         this.mute = "unmuted"
  65                 } else {
  66                         this.mute = "mute"
  67                 }
  68                 def initStatus = Verify.getBoolean()
  69                 if (initStatus) {
  70                         this.status = "paused"
  71                 } else {
  72                         this.status = "playing"
  73                 }
  74
  75                 musicPlayers.add(new MusicPlayer(id, label, displayName, this.level, this.mute, this.status, this.trackNumber, this.trackData, this.trackDescription))
  76         }
  77
  78         //By model checker
  79         def setValue(LinkedHashMap eventDataMap) {
  80                 if (eventDataMap["name"] == "status") {
  81                         if (eventDataMap["value"] != musicPlayers[0].status) {
  82                                 musicPlayers[0].setValue(eventDataMap["value"], "status")
  83                                 this.status = musicPlayers[0].status
  84                                 sendEvent(eventDataMap)
  85                         }
  86                 } else if (eventDataMap["name"] == "level") {
  87                         if (eventDataMap["value"] != musicPlayers[0].level) {
  88                                 musicPlayers[0].setValue(eventDataMap["value"], "level")
  89                                 this.level = musicPlayers[0].level
  90                                 sendEvent(eventDataMap)
  91                         }
  92                 } else if (eventDataMap["name"] == "trackDescription") {
  93                         if (eventDataMap["value"] != musicPlayers[0].trackDescription) {
  94                                 musicPlayers[0].setValue(eventDataMap["value"], "trackDescription")
  95                                 this.trackDescription = musicPlayers[0].trackDescription
  96                                 sendEvent(eventDataMap)
  97                         }
  98                 } else if (eventDataMap["name"] == "trackData") {
  99                         if (eventDataMap["value"] != musicPlayers[0].trackData) {
 100                                 musicPlayers[0].setValue(eventDataMap["value"], "trackData")
 101                                 this.trackData = musicPlayers[0].trackData
 102                                 sendEvent(eventDataMap)
 103                         }
 104                 } else if (eventDataMap["name"] == "mute") {
 105                         if (eventDataMap["value"] != musicPlayers[0].mute) {
 106                                 musicPlayers[0].setValue(eventDataMap["value"], "mute")
 107                                 this.mute = musicPlayers[0].mute
 108                                 sendEvent(eventDataMap)
 109                         }
 110                 }
 111         }
 112
 113         //Methods for closures
 114         def count(Closure Input) {
 115                 musicPlayers.count(Input)
 116         }
 117         def size() {
 118                 musicPlayers.size()
 119         }
 120         def each(Closure Input) {
 121                 musicPlayers.each(Input)
 122         }
 123         def find(Closure Input) {
 124                 musicPlayers.find(Input)
 125         }
 126         def collect(Closure Input) {
 127                 musicPlayers.collect(Input)
 128         }
 129
 130         //methods
 131         def mute() {
 132                 if (mute != "muted") {
 133                         musicPlayers[0].mute()
 134                         this.mute = "muted"
 135                 }
 136         }
 137         def nextTrack() {
 138                 musicPlayers[0].nextTrack()
 139                 if (status != "playing") {
 140                         this.status = "playing"
 141                 }
 142                 this.trackNumber = musicPlayers[0].trackNumber
 143         }
 144         def pause() {
 145                 if (status != "paused") {
 146                         musicPlayers[0].pause()
 147                         this.status = "paused"
 148                 }
 149         }
 150         def play() {
 151                 if (status != "playing") {
 152                         musicPlayers[0].play()
 153                         this.status = "playing"
 154                 }
 155         }
 156         def playTrack(String trackToPlay) {
 157                 musicPlayers[0].playTrack(trackToPlay)
 158                 if (status != "playing") {
 159                         this.status = "playing"
 160                 }
 161                 this.trackNumber = musicPlayers[0].trackNumber
 162         }
 163         def previousTrack() {
 164                 musicPlayers[0].previousTrack()
 165                 if (status != "playing") {
 166                         this.status = "playing"
 167                 }
 168                 this.trackNumber = musicPlayers[0].trackNumber
 169         }
 170         def restoreTrack(String trackToRestore) {
 171                 musicPlayers[0].restoreTrack(trackToRestore)
 172         }
 173         def resumeTrack(String trackToResume) {
 174                 musicPlayers[0].resumeTrack(trackToResume)
 175                 if (status != "playing") {
 176                         this.status = "playing"
 177                 }
 178         }
 179         def setLevel(int level) {
 180                 if (level != this.level) {
 181                         musicPlayers[0].setLevel(level)
 182                         this.level = level
 183                 }
 184         }
 185         def setTrack(String trackToSet) {
 186                 musicPlayers[0].setTrack(trackToSet)
 187                 if (status != "playing") {
 188                         this.status = "playing"
 189                 }
 190                 this.trackNumber = musicPlayers[0].trackNumber
 191         }
 192         def stop() {
 193                 if (status != "stopped") {
 194                         musicPlayers[0].stop()
 195                         this.status = "stopped"
 196                 }
 197         }
 198
 199         def currentValue(String deviceFeature) {
 200                 musicPlayers[0].currentValue(deviceFeature)
 201         }
 202
 203         def getAt(int ix) {
 204                 musicPlayers[ix]
 205         }
 206 }