package Battery
import Timer.SimulatedTimer
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
public class Batteries {
private int deviceNumbers
private List batteries
private String label = "battery0"
private String displayName = "battery0"
private int battery = 50
- private String currentBattery = 50
+ private int currentBattery = 50
+ private int batteryLatestValue = 50
- Batteries(Closure sendEvent, int deviceNumbers) {
+ Batteries(Closure sendEvent, int deviceNumbers, boolean init) {
this.sendEvent = sendEvent
this.deviceNumbers = deviceNumbers
this.batteries = []
-
- def init = Verify.getIntFromList(30, 50, 70)
- this.battery = init
+
+ if (init) {
+ this.battery = 50
+ this.currentBattery = 50
+ this.batteryLatestValue = 50
+ } else {
+ this.battery = 35
+ this.currentBattery = 35
+ this.batteryLatestValue = 35
+ }
batteries.add(new Battery(id, label, displayName, this.battery))
}
//By Model Checker
def setValue(LinkedHashMap eventDataMap) {
- if (eventDataMap["value"] != batteries[0].battery) {
+ if (eventDataMap["value"].toInteger() != batteries[0].battery) {
+ this.battery = eventDataMap["value"].toInteger()
+ this.currentBattery = eventDataMap["value"].toInteger()
+ this.batteryLatestValue = eventDataMap["value"].toInteger()
batteries[0].setValue(eventDataMap["value"])
- this.battery = batteries[0].battery
- this.currentBattery = batteries[0].battery
sendEvent(eventDataMap)
}
}
def each(Closure Input) {
batteries.each(Input)
}
+ def sort(Closure Input) {
+ batteries.sort(Input)
+ }
def find(Closure Input) {
batteries.find(Input)
}
batteries[0].currentValue(deviceFeature)//It is called if we have only one device
}
+ def latestValue(String deviceFeature) {
+ batteries[0].latestValue(deviceFeature)//It is called if we have only one device
+ }
+
def getAt(int ix) {
batteries[ix]
}