1 //Create a class for acceleration sensor
2 package AccelerationSensor
3 import Timer.SimulatedTimer
6 import gov.nasa.jpf.vm.Verify
8 public class AccelerationSensor {
11 private String displayName
12 private String acceleration
13 private String currentAcceleration
14 private String accelerationLatestValue
16 AccelerationSensor(String id, String label, String displayName, String acceleration, String accelerationLatestValue) {
19 this.displayName = displayName
20 this.acceleration = acceleration
21 this.currentAcceleration = acceleration
22 this.accelerationLatestValue = accelerationLatestValue
25 def setValue(String value) {
26 println("the acceleration sensor with id:$id is triggered to $value!")
27 this.accelerationLatestValue = value
28 this.acceleration = value
29 this.currentAcceleration = value
33 def evtActive = [[name: "acceleration", value: "active", deviceId: "accelerationSensorID0", descriptionText: "",
34 displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
35 def evtInactive = [[name: "acceleration", value: "inactive", deviceId: "accelerationSensorID0", descriptionText: "",
36 displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
37 def init = Verify.getInt(0,4)
39 if (init == 0) {//return empty set
41 } else if (init == 1) {//send one active event
46 } else if (init == 2) {//send two active events
54 } else if (init == 3) {//send one inactive event
59 } else if (init == 4) {//send two inactive events
71 def evtActive = [[name: "acceleration", value: "active", deviceId: "accelerationSensorID0", descriptionText: "",
72 displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
73 def evtInactive = [[name: "acceleration", value: "inactive", deviceId: "accelerationSensorID0", descriptionText: "",
74 displayed: true, linkText: "", isStateChange: false, unit: "", data: '{"info": "info"}']]
75 def init = Verify.getInt(0,4)
77 if (init == 0) {//return empty set
79 } else if (init == 1) {//send one active event
84 } else if (init == 2) {//send two active events
92 } else if (init == 3) {//send one inactive event
97 } else if (init == 4) {//send two inactive events
109 def currentValue(String deviceFeature) {
110 if (deviceFeature == "acceleration") {
115 def latestValue(String deviceFeature) {
116 if (deviceFeature == "acceleration") {
117 return accelerationLatestValue