Simplifications && preparation for restart.

1 files changed, 14 insertions, 8 deletions

diff --git a/abstract/transform.ml b/abstract/transform.ml
index 7ae54ad..dcb4049 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -120,7 +120,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
   | _ when type_expr td.rp node expr = [bool_type] ->
     f_or
       (f_and (f_of_expr td (node, prefix, clock_scope) expr)
-          (where [EE (EItem bool_true)]))
+        (where [EE (EItem bool_true)]))
       (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr))
         (where [EE (EItem bool_false)]))
   | _ -> le type_error "Expected numerical/enumerated value"
@@ -135,11 +135,12 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
 *)
 and f_of_bexpr td (node, prefix, clock_scope) where expr =
   let sub = f_of_bexpr td (node, prefix, clock_scope) in
+  let sub_id = sub (fun x -> x) in
   match fst expr with
   | AST_bool_const b -> where (BConst b)
-  | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b)
-  | AST_binary_bool(AST_OR, a, b) -> f_or (sub where a) (sub where b)
-  | AST_not(a) -> BNot(sub where a)
+  | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b))
+  | AST_binary_bool(AST_OR, a, b) -> where (f_or (sub_id a) (sub_id b))
+  | AST_not(a) -> where (BNot (sub_id a))
   | AST_binary_rel(rel, a, b) ->
     where
       (f_of_neexpr td (node, prefix, clock_scope)
@@ -175,9 +176,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
   | _ when type_expr td.rp node expr = [bool_type] ->
     let ff = function
       | [EE x] -> 
-        f_or
-          (f_and (f_e_eq x (EItem bool_true)) (where (BConst true)))
-          (f_and (f_e_eq x (EItem bool_false)) (where (BConst false)))
+        where (f_e_eq x (EItem bool_true))
       | _ -> assert false
     in
     f_of_neexpr td (node, prefix, clock_scope) ff expr
@@ -387,7 +386,14 @@ and f_of_prog rp assume_guarantees =
 
     let clock_scope, clock_eq = gen_clock td rp.root_scope true in
 
-    f_and clock_eq (f_of_scope true td td.rp.root_scope clock_scope assume_guarantees)
+    let scope_f = 
+      f_of_scope
+        true
+        td td.rp.root_scope
+        clock_scope
+        assume_guarantees in
+    f_and clock_eq scope_f
+      
 
 (*
     Translate init state into a formula