Add gilbreath suite ; booleans are not represented in a good way.

5 files changed, 105 insertions, 60 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 4c3fddb..feaf037 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -9,12 +9,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig
 
     type st
 
-    val do_prog     : prog -> id -> unit
+    val do_prog     : int -> prog -> id -> unit
 
 end = struct
 
     type st = {
         p           : prog;
+        widen_delay : int;
         root_scope  : scope;
         all_vars    : var_def list;
         env         : E.t;
@@ -69,7 +70,7 @@ end = struct
         (List.flatten (List.map vars_of_eq eqs))
 
     (* init state *)
-    let init_state p root =
+    let init_state widen_delay p root =
       let root_scope = get_root_scope p root in
 
       let f = Formula.eliminate_not (Transform.f_of_prog p root) in
@@ -86,11 +87,11 @@ end = struct
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
       Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
 
-      Format.printf "Vars: %a@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
+      Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
 
       let env = E.apply_f env init_f in
 
-      { p; root_scope; f; cl; all_vars; env }
+      { p; root_scope; widen_delay; f; cl; all_vars; env }
 
     (*
       pass_cycle : var_def list -> E.t -> E.t
@@ -121,13 +122,12 @@ end = struct
 
     (* cycle : st -> cl -> env -> env *)
     let cycle st cl i =
-      E.apply_cl (pass_cycle st.all_vars i) cl
+      (pass_cycle st.all_vars (E.apply_cl i cl)) 
 
     (*
       loop : st -> cl -> env -> env -> env
     *)
     let loop st cycle_cl pnew stay =
-      let pnew = E.apply_cl pnew cycle_cl in
 
       Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
         Formula_printer.print_conslist cycle_cl
@@ -142,10 +142,9 @@ end = struct
         E.join acc0 j
       in
 
-      let widen_delay = 10 in
       let rec iter n i =
         let i' =
-          if n < widen_delay
+          if n < st.widen_delay
             then E.join i (fsharp i)
             else E.widen i (fsharp i)
         in
@@ -159,21 +158,23 @@ end = struct
     (*
       do_prog : prog -> id -> unit
     *)
-    let do_prog p root =
-      let st = init_state p root in
+    let do_prog widen_delay p root =
+      let st = init_state widen_delay p root in
 
       let pnew = st.env in
 
       let stay = loop st st.cl pnew (E.vbottom pnew) in
 
-      Format.printf "@[<hov>Final stay %a@]@."
-        E.print_all stay;
+      let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in
+
+      Format.printf "@[<hov>Final %a@]@."
+        E.print_all final;
 
       Format.printf "Probes:@[<hov>";
       List.iter (fun (p, id, _) ->
         if p then Format.printf "@ %a ∊ %a,"
               Formula_printer.print_id id
-              E.print_itv (E.var_itv stay id))
+              E.print_itv (E.var_itv final id))
         st.all_vars;
       Format.printf "@]@."
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 262bccb..44495c4 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -12,17 +12,31 @@ type num_expr =
   (* identifier *)
   | NIdent of id
 
+
 type bool_expr =
   (* constants *)
   | BConst of bool
   (* operators from numeric values to boolean values *)
   | BRel of binary_rel_op * num_expr * num_expr
+  | BBoolEq of id * bool
   (* boolean operators *)
   | BAnd of bool_expr * bool_expr
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
 
+let f_and a b = match a, b with
+  | BConst false, _ | _, BConst false -> BConst false
+  | BConst true, b -> b
+  | a, BConst true -> a
+  | a, b -> BAnd(a, b)
+
+let f_or a b = match a, b with
+  | BConst true, _ | _, BConst true -> BConst true
+  | BConst false, b -> b
+  | a, BConst false -> a
+  | a, b -> BOr(a, b)
+
 
 (* Write all formula without using the NOT operator *)
 
@@ -33,6 +47,7 @@ let rec eliminate_not = function
   | x -> x
 and eliminate_not_negate = function
   | BConst x -> BConst(not x)
+  | BBoolEq(id, v) -> BBoolEq(id, not v)
   | BNot e -> eliminate_not e
   | BRel(r, a, b) ->
     let r' = match r with
@@ -83,6 +98,11 @@ let rec conslist_of_f = function
     in [cons], CLTrue
   | BConst x ->
     [], if x then CLTrue else CLFalse
+  | BBoolEq(id, v) ->
+    if v then
+      [NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue
+    else
+      [NIdent id, CONS_EQ], CLTrue
   | BOr(a, b) ->
     let ca, ra = conslist_of_f a in
     let cb, rb = conslist_of_f b in
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 53a9b6a..1b31ba1 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -60,6 +60,11 @@ let rec print_num_expr fmt e = match e with
 
 let rec print_bool_expr fmt e = match e with
   | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
+  | BBoolEq(id, v) ->
+    if v then
+      Format.fprintf fmt "%a" print_id id
+    else
+      Format.fprintf fmt "¬%a" print_id id
   | BRel(op, a, b) ->
     print_ch fmt print_num_expr ne_prec a be_prec e;
     Format.fprintf fmt "@ %s " (string_of_binary_rel op);
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 3cdcc31..855f970 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -215,14 +215,15 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
             List.iteri
               (fun j (v, ids) ->
                 if j > 0 then Format.fprintf fmt "@ ";
+                Format.fprintf fmt "@[<hov 4>";
                 List.iteri
                   (fun i id ->
-                    if i > 0 then Format.fprintf fmt ", ";
+                    if i > 0 then Format.fprintf fmt ",@ ";
                     Format.fprintf fmt "%a" Formula_printer.print_id id)
                   ids;
                 match V.as_const v with
-                | Some i -> Format.fprintf fmt " = %d" i
-                | _ -> Format.fprintf fmt " ∊ %s" (V.to_string v))
+                | Some i -> Format.fprintf fmt " = %d@]" i
+                | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v))
               sbl;
             Format.fprintf fmt " }@]"
 
diff --git a/abstract/transform.ml b/abstract/transform.ml
index b141cc6..87da1bd 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -18,11 +18,6 @@ type transform_data = {
     (* future : the automata state *)
 }
 
-let f_and a b =
-  if a = BConst true then b
-    else if b = BConst true then a
-      else BAnd(a, b)
-
 
 (* f_of_nexpr :
     transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
@@ -55,48 +50,76 @@ let rec f_of_nexpr td (node, prefix) where expr =
   (* temporal *)
   | AST_pre(_, id) -> where [NIdent id]
   | AST_arrow(a, b) ->
-      BOr(
-        BAnd(BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0),
-          sub where a),
-        BAnd(BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1),
-          sub where b))
+    f_or
+      (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+        (sub where a))
+      (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+        (sub where b))
   (* other *)
   | AST_if(c, a, b) ->
-    BOr(
-      BAnd(f_of_bexpr td (node, prefix) c, sub where a),
-      BAnd(BNot(f_of_bexpr td (node, prefix) c), sub where b))
+    f_or
+      (f_and (f_of_expr td (node, prefix) c) (sub where a))
+      (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
   | AST_instance ((f, _), args, nid) ->
     let (n, _) = find_node_decl td.p f in
     where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
     
   (* boolean values treated as integers *)
   | _ ->
-    BOr(
-      BAnd ((f_of_bexpr td (node, prefix) expr), where [NIntConst 1]),
-      BAnd (BNot(f_of_bexpr td (node, prefix) expr), where [NIntConst 0])
-    )
+    f_or
+      (f_and ((f_of_expr td (node, prefix) expr)) (where [NIntConst 1]))
+      (f_and (BNot(f_of_expr td (node, prefix) expr)) (where [NIntConst 0]))
+
 
-(* f_of_expr :
+(* 
+  f_of_expr :
     transform_data -> (string, string) -> expr -> bool_expr
+  f_of_bexpr :
+    transform_data -> (string, string) -> (bool_expr -> 'a) -> expr -> 'a
 *)
-and f_of_bexpr td (node, prefix) expr =
+and f_of_bexpr td (node, prefix) where expr =
   let sub = f_of_bexpr td (node, prefix) in
   match fst expr with
-  | AST_bool_const b -> BConst b
-  | AST_binary_bool(AST_AND, a, b) -> BAnd(sub a, sub b)
-  | AST_binary_bool(AST_OR, a, b) -> BOr(sub a, sub b)
-  | AST_not(a) -> BNot(sub a)
+  | 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_rel(rel, a, b) ->
-    f_of_nexpr td (node, prefix)
-      (function
-        | [x] -> f_of_nexpr td (node, prefix)
-          (function
-            | [y] -> BRel(rel, x, y)
-            | _ -> invalid_arity "boolean relation") b
-        | _ -> invalid_arity "boolean relation")
-      a
-  | _ -> loc_error (snd expr) error "Invalid type : expected boolean value"
-  
+    where
+      (f_of_nexpr td (node, prefix)
+        (function
+          | [x] -> f_of_nexpr td (node, prefix)
+            (function
+              | [y] -> BRel(rel, x, y)
+              | _ -> invalid_arity "boolean relation") b
+          | _ -> invalid_arity "boolean relation")
+        a)
+  | AST_identifier (id, _) ->
+    let id = node^"/"^id in
+    f_or
+      (f_and (BBoolEq(id, true)) (where (BConst true)))
+      (f_and (BBoolEq(id, false)) (where (BConst false)))
+  (* temporal *)
+  | AST_pre(_, id) ->
+    f_or
+      (f_and (BBoolEq(id, true)) (where (BConst true)))
+      (f_and (BBoolEq(id, false)) (where (BConst false)))
+  | AST_arrow(a, b) ->
+      f_or
+        (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+          (sub where a))
+        (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+          (sub where b))
+  (* other *)
+  | AST_if(c, a, b) ->
+    f_or
+      (f_and (f_of_expr td (node, prefix) c) (sub where a))
+      (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
+
+  | _ -> loc_error (snd expr) error "Expected boolean value."
+
+and f_of_expr td (node, prefix) expr =
+    f_of_bexpr td (node, prefix) (fun x -> x) expr
   
 
 and f_of_scope active td (node, prefix, eqs) =
@@ -148,7 +171,7 @@ and f_of_scope active td (node, prefix, eqs) =
     | AST_assume (_, e) ->
       let assume_eq = 
         if active then
-          f_of_bexpr td (node, prefix) e
+          f_of_expr td (node, prefix) e
         else
           BConst true
       in
@@ -166,12 +189,11 @@ and f_of_scope active td (node, prefix, eqs) =
         | AST_activate_body b ->
             f_of_scope true td (node, b.act_id^".", b.body)
         | AST_activate_if(c, a, b) ->
-          BOr(
-            f_and (f_of_bexpr td (node, prefix) c)
-              (f_and (do_tree_act a) (do_tree_inact b)),
-            f_and (BNot(f_of_bexpr td (node, prefix) c))
-              (f_and (do_tree_act b) (do_tree_inact a))
-          )
+          f_or
+            (f_and (f_of_expr td (node, prefix) c)
+              (f_and (do_tree_act a) (do_tree_inact b)))
+            (f_and (BNot(f_of_expr td (node, prefix) c))
+              (f_and (do_tree_act b) (do_tree_inact a)))
       and do_tree_inact = function
         | AST_activate_body b ->
           f_of_scope false td (node, b.act_id^".", b.body)
@@ -202,10 +224,6 @@ and f_of_prog p root =
     } in
 
     f_of_scope true td td.root_scope
-  
-
-
-