Adding path explorations for initializations.

[smartthings-infrastructure.git] / ContactSensor / ContactSensors.groovy

diff --git a/ContactSensor/ContactSensors.groovy b/ContactSensor/ContactSensors.groovy
index 1de8c76dccd1ec2a90c08319dbf11236ba12333c..489200dbf0a43907d3556cef56f50c528d7a5834 100644 (file)
--- a/ContactSensor/ContactSensors.groovy
+++ b/ContactSensor/ContactSensors.groovy
@@ -2,6 +2,9 @@
 package ContactSensor
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class ContactSensors {
        private int deviceNumbers
        private List contacts
@@ -22,6 +25,23 @@ public class ContactSensors {
                this.deviceNumbers = deviceNumbers
                this.contacts = []
 
+               def initSensor = Verify.getBoolean()
+               if (initSensor) {
+                       this.contactState = "closed"
+                       this.currentContact = "closed"
+                       this.latestValue = "closed"
+               } else {
+                       this.contactState = "open"
+                       this.currentContact = "open"
+                       this.latestValue = "open"
+               }
+
+               def initAlarm = Verify.getBoolean()
+               if (initAlarm) {
+                       this.alarmState = "armed"
+               } else {
+                       this.alarmState = "not armed"
+               }
                contacts.add(new ContactSensor(id, label, displayName, this.contactState, this.currentContact, this.alarmState, this.latestValue))
        }