Adding more exploration for execution paths.
[smartthings-infrastructure.git] / Runner.py
index d3d7c16f0ff5cc506d4d71da1462ab95d7115929..e82d1c2f1534f7a60e4da261a0ac9404d7968fa8 100644 (file)
--- a/Runner.py
+++ b/Runner.py
@@ -68,9 +68,24 @@ Out.write("import Alarm.Alarm\n")
 Out.write("import Alarm.Alarms\n")
 Out.write("import SpeechSynthesis.SpeechSynthesis\n")
 Out.write("import SpeechSynthesis.SpeechSynthesises\n")
+Out.write("import AccelerationSensor.AccelerationSensor\n")
+Out.write("import AccelerationSensor.AccelerationSensors\n")
+Out.write("import Battery.Battery\n")
+Out.write("import Battery.Batteries\n")
+Out.write("import BeaconSensor.BeaconSensor\n")
+Out.write("import BeaconSensor.BeaconSensors\n")
+Out.write("import CarbonMonoxideDetector.CarbonMonoxideDetector\n")
+Out.write("import CarbonMonoxideDetector.CarbonMonoxideDetectors\n")
+Out.write("import ColorControl.ColorControl\n")
+Out.write("import ColorControl.ColorControls\n")
+Out.write("import EnergyMeter.EnergyMeter\n")
+Out.write("import EnergyMeter.EnergyMeters\n")
 Out.write("import Event.Event\n")
 Out.write("import Timer.SimulatedTimer\n")
 Out.write("\n")
+Out.write("//JPF's Verify API\n")
+Out.write("import gov.nasa.jpf.vm.Verify\n")
+Out.write("\n")
 Out.write("//Global eventHandler\n")
 for line in eventHandler:
        Out.write(line)
@@ -214,11 +229,24 @@ for line in App2:
                Out.write("\t"+line)
 Out.write("}\n")
 Out.write("\n")
-Out.write("@Field def app1 = new App1(this)\n")
-Out.write("@Field def app2 = new App2(this)\n")
-Out.write("app1.installed()\n")
-Out.write("app2.installed()\n")
-Out.write("\n")
+Out.write("@Field def app1\n")
+Out.write("@Field def app2\n")
+Out.write("def initOrder = Verify.getBoolean()\n")
+Out.write("if (initOrder) {\n")
+Out.write("\tapp1 = new App1(this)\n")
+Out.write("\tapp2 = new App2(this)\n")
+Out.write("} else {\n")
+Out.write("\tapp2 = new App2(this)\n")
+Out.write("\tapp1 = new App1(this)\n")
+Out.write("}\n\n")
+Out.write("def installOrder = Verify.getBoolean()\n")
+Out.write("if (installOrder) {\n")
+Out.write("\tapp1.installed()\n")
+Out.write("\tapp2.installed()\n")
+Out.write("} else {\n")
+Out.write("\tapp1.installed()\n")
+Out.write("\tapp2.installed()\n")
+Out.write("}\n\n")
 for line in eventSimulator:
        Out.write(line)
 Out.close()