Adding path explorations for initializations.
[smartthings-infrastructure.git] / Lock / Locks.groovy
index f792c6ccfda41d3f5d36d8ec77ae1436ffc85a7d..f2b9d75fdf688071f50198b3727e1104d3f4409a 100644 (file)
@@ -2,6 +2,9 @@
 package Lock
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class Locks{
        int deviceNumbers       
        List locks      
@@ -22,6 +25,14 @@ public class Locks{
                this.deviceNumbers = deviceNumbers
                this.locks = []
 
+               def init = Verify.getBoolean()
+               if (init) {
+                       this.lockState = "locked"
+                       this.lockLatestValue = "locked"
+               } else {
+                       this.lockState = "unlocked"
+                       this.lockLatestValue = "unlocked"
+               }
                locks.add(new Lock(sendEvent,id, label, displayName, this.lockState, this.lockLatestValue))
        }