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)