1 files changed, 20 insertions, 0 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 480705f..e0f32c2 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -490,6 +490,26 @@ and f_of_prog rp assume_guarantees =
       f_and clock_eq scope_f
     in
       prog_init, prog_normal
+
+let f_of_prog_incl_init rp assume_guarantees =
+    let td = {
+      rp = rp;
+      consts = I.consts rp;
+    } in
+
+    let init_cond = BEnumCons(E_EQ, "L/must_reset", bool_true) in
+    let no_next_init_cond = BEnumCons(E_EQ, "/must_reset", bool_false) in
+
+    let clock_scope, clock_eq = gen_clock td rp.root_scope true [init_cond] in
+
+    let scope_f = 
+      f_of_scope
+        true
+        td td.rp.root_scope
+        clock_scope
+        assume_guarantees in
+    f_and clock_eq (f_and no_next_init_cond scope_f)
+