package AccelerationSensor
import Timer.SimulatedTimer
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
public class AccelerationSensors {
private int deviceNumbers
private List accelerationSensors
- AccelerationSensors(Closure sendEvent, int deviceNumbers) {
+ AccelerationSensors(Closure sendEvent, int deviceNumbers, boolean init) {
this.sendEvent = sendEvent
this.deviceNumbers = deviceNumbers
this.accelerationSensors = []
- def init = Verify.getBoolean()
if (init) {
this.acceleration = "inactive"
this.accelerationLatestValue = "inactive"
}
}
+ //methods
+ def eventsSince(Date dateObj) {
+ return accelerationSensors[0].eventsSince()
+ }
+
+ def statesSince(String info, Date dateObj) {
+ return accelerationSensors[0].statesSince()
+ }
+
//Methods for closures
def count(Closure Input) {
accelerationSensors.count(Input)
accelerationSensors[0].latestValue(deviceFeature)//It is called if we have only one device
}
- def statesSince(String info, Date dateObj) {
- return accelerationSensors[0].statesSince(info, dateObj)
- }
-
def getAt(int ix) {
accelerationSensors[ix]
}