X-Git-Url: http://plrg.eecs.uci.edu/git/?p=smartthings-infrastructure.git;a=blobdiff_plain;f=SmokeDetector%2FSmokeDetectors.groovy;h=e9d5da2f67b6c87057cc915d970fb9dbb83a1dc1;hp=95bcb3c265a95b4072fbc02095f2abcc32f51c12;hb=31da25f02c14814f402e84b35a174f3c0958cd38;hpb=7bc2c68bdfb07a54d6e8399e7514d715c78a2398

diff --git a/SmokeDetector/SmokeDetectors.groovy b/SmokeDetector/SmokeDetectors.groovy
index 95bcb3c..e9d5da2 100644
--- a/SmokeDetector/SmokeDetectors.groovy
+++ b/SmokeDetector/SmokeDetectors.groovy
@@ -2,6 +2,9 @@
 package SmokeDetector
 import Timer.SimulatedTimer
 
+//JPF's Verify API
+import gov.nasa.jpf.vm.Verify
+
 public class SmokeDetectors {
 	private int deviceNumbers
 	private List smokeDetectors
@@ -21,6 +24,17 @@ public class SmokeDetectors {
 		this.deviceNumbers = deviceNumbers
 		this.smokeDetectors = []
 
+		def init = Verify.getInt(0,2)
+		if (init == 0) {
+			this.currentSmokeValue = "clear"
+			this.smokeLatestValue = "clear"
+		} else if (init == 1) {
+			this.currentSmokeValue = "detected"
+			this.smokeLatestValue = "detected"
+		} else {
+			this.currentSmokeValue = "tested"
+			this.smokeLatestValue = "tested"		
+		}
 		smokeDetectors.add(new SmokeDetector(id, label, displayName, this.currentSmokeValue, this.smokeLatestValue))
 	}