Adding path explorations for initializations.

[smartthings-infrastructure.git] / MotionSensor / MotionSensors.groovy

diff --git a/MotionSensor/MotionSensors.groovy b/MotionSensor/MotionSensors.groovy
index 863903c5017090867a58f7ca2b3e5bf676986e59..85167131551b73f787be48e6525bb806a5e2db8c 100644 (file)
--- a/MotionSensor/MotionSensors.groovy
+++ b/MotionSensor/MotionSensors.groovy
@@ -2,6 +2,9 @@
 package MotionSensor
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class MotionSensors {
        private int deviceNumbers
        private List motionSensors
@@ -21,6 +24,14 @@ public class MotionSensors {
                this.deviceNumbers = deviceNumbers
                this.motionSensors = []
 
+               def init = Verify.getBoolean()
+               if (init) {
+                       this.motion = "inactive"
+                       this.motionLatestValue = "inactive"
+               } else {
+                       this.motion = "active"
+                       this.motionLatestValue = "active"
+               }
                motionSensors.add(new MotionSensor(id, label, displayName, this.motion, this.motionLatestValue))
        }