Write transformation of program into logical formula.

3 files changed, 389 insertions, 25 deletions

diff --git a/abstract/formula.ml b/abstract/formula.ml
index 389000c..2c83b32 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -22,3 +22,81 @@ type bool_expr =
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
+
+
+(* Write all formula without using the NOT operator *)
+
+let rec eliminate_not = function
+  | BNot e -> eliminate_not_negate e
+  | BAnd(a, b) -> BAnd(eliminate_not a, eliminate_not b)
+  | BOr(a, b) -> BOr(eliminate_not a, eliminate_not b)
+  | x -> x
+and eliminate_not_negate = function
+  | BConst x -> BConst(not x)
+  | BNot e -> eliminate_not e
+  | BRel(r, a, b) ->
+    let r' = match r with
+    | AST_EQ -> AST_NE
+    | AST_NE -> AST_EQ
+    | AST_LT -> AST_GE
+    | AST_LE -> AST_GT
+    | AST_GT -> AST_LE
+    | AST_GE -> AST_LT
+    in
+    BRel(r', a, b)
+  | BAnd(a, b) ->
+    BOr(eliminate_not_negate a, eliminate_not_negate b)
+  | BOr(a, b) ->
+    BAnd(eliminate_not_negate a, eliminate_not_negate b)
+
+(*
+  In big ANDs, try to separate levels of /\ and levels of \/
+  We also use this step to simplify trues and falses that may be present.
+*)
+
+type cons_op =
+  | CONS_EQ | CONS_NE
+  | CONS_GT | CONS_GE
+type cons = num_expr * cons_op  (* always imply right member = 0 *)
+
+type conslist = cons list * conslist_bool_expr
+and conslist_bool_expr =
+  | CLTrue
+  | CLFalse
+  | CLAnd of conslist_bool_expr * conslist_bool_expr
+  | CLOr of conslist * conslist
+
+let rec conslist_of_f = function
+  | BNot e -> conslist_of_f (eliminate_not_negate e)
+  | BRel (op, a, b) ->
+    let cons = match op with
+      | AST_EQ -> NBinary(AST_MINUS, a, b), CONS_EQ
+      | AST_NE -> NBinary(AST_MINUS, a, b), CONS_NE
+      | AST_GT -> NBinary(AST_MINUS, a, b), CONS_GT
+      | AST_GE -> NBinary(AST_MINUS, a, b), CONS_GE
+      | AST_LT -> NBinary(AST_MINUS, b, a), CONS_GT
+      | AST_LE -> NBinary(AST_MINUS, b, a), CONS_GE
+    in [cons], CLTrue
+  | BConst x ->
+    [], if x then CLTrue else CLFalse
+  | BOr(a, b) ->
+    let ca, ra = conslist_of_f a in
+    let cb, rb = conslist_of_f b in
+    begin match ca, ra, cb, rb with
+      | _, CLFalse, _, _ -> cb, rb
+      | _, _, _, CLFalse -> ca, ra
+      | [], CLTrue, _, _ -> [], CLTrue
+      | _, _, [], CLTrue -> [], CLTrue
+      | _ -> [], CLOr((ca, ra), (cb, rb))
+    end
+  | BAnd(a, b) ->
+    let ca, ra = conslist_of_f a in
+    let cb, rb = conslist_of_f b in
+    let cons = ca @ cb in
+    begin match ra, rb with
+      | CLFalse, _ | _, CLFalse -> [], CLFalse
+      | CLTrue, _ -> cons, rb
+      | ra, CLTrue -> cons, ra
+      | _, _ -> cons, CLAnd(ra, rb)
+    end
+
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 7e626f0..994c82a 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -1,6 +1,15 @@
+open Ast
 open Formula
 open Ast_printer
 
+let string_of_binary_rel = function
+  | AST_EQ -> "="
+  | AST_NE -> "≠"
+  | AST_LT -> "<"
+  | AST_LE -> "≤"
+  | AST_GT -> ">"
+  | AST_GE -> "≥"
+
 let ne_prec = function
   | NUnary(op, _) -> unary_precedence
   | NBinary(op, _, _) -> binary_op_precedence op
@@ -13,44 +22,118 @@ let be_prec = function
   | BNot _ -> unary_precedence
   | _ -> 100
 
+let is_or = function
+  | BOr _ -> true
+  | _ -> false
+let is_and = function
+  | BAnd _ -> true
+  | _ -> false
+
 
-let print_lh fmt pf fa a fe e =
+let print_ch fmt pf fa a fe e =
   if fa a < fe e
-    then Format.fprintf fmt "@[<2>(%a)@]" pf a
-    else Format.fprintf fmt "%a" pf a
-let print_rh fmt pf fb b fe e =
-  if fb b < fe e
-    then Format.fprintf fmt "@[<2>(%a)@]" pf b
-    else Format.fprintf fmt "%a" pf b
+    then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
+    else Format.fprintf fmt "@[<hv 2>%a@]" pf a
+let print_ah fmt pf fa a fe e =
+  if fa a <= fe e
+    then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
+    else Format.fprintf fmt "@[<hv 2>%a@]" pf a
 
 let rec print_num_expr fmt e = match e with
   | NIntConst i -> Format.fprintf fmt "%d" i
   | NRealConst f -> Format.fprintf fmt "%f" f
-  | NIdent id -> Format.fprintf fmt "%s" id
+  | NIdent id ->
+    let re = Str.regexp "/" in
+    Format.fprintf fmt "%s" (Str.global_replace re "·" id)
   | NBinary(op, a, b) ->
-    print_lh fmt print_num_expr ne_prec a ne_prec e;
-    Format.fprintf fmt "@ %s@ " (string_of_binary_op op);
-    print_rh fmt print_num_expr ne_prec b ne_prec e
+    print_ch fmt print_num_expr ne_prec a ne_prec e;
+    Format.fprintf fmt "@ %s " (string_of_binary_op op);
+    print_ah fmt print_num_expr ne_prec b ne_prec e
   | NUnary(op, a) ->
-    Format.pp_print_string fmt (string_of_unary_op op);
-    print_rh fmt print_num_expr ne_prec a ne_prec e
+    Format.fprintf fmt "%s " (string_of_unary_op op);
+    print_ah fmt print_num_expr ne_prec a ne_prec e
+
+(* Print boolean form of formula *)
 
 let rec print_bool_expr fmt e = match e with
   | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
   | BRel(op, a, b) ->
-    print_lh fmt print_num_expr ne_prec a be_prec e;
-    Format.fprintf fmt "@ %s@ " (string_of_binary_rel op);
-    print_rh fmt print_num_expr ne_prec b be_prec e
+    print_ch fmt print_num_expr ne_prec a be_prec e;
+    Format.fprintf fmt "@ %s " (string_of_binary_rel op);
+    print_ch fmt print_num_expr ne_prec b be_prec e
   | BAnd (a, b) ->
-    print_lh fmt print_bool_expr be_prec a be_prec e;
-    Format.fprintf fmt "@ /\\@ ";
-    print_rh fmt print_bool_expr be_prec b be_prec e
+
+    if is_and a then
+      Format.fprintf fmt "%a" print_bool_expr a
+    else
+      if be_prec a < be_prec e || is_or a
+        then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr a
+        else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr a;
+    Format.fprintf fmt "@ ∧ ";
+    if is_and b then
+        Format.fprintf fmt "%a" print_bool_expr b
+    else
+      if be_prec b < be_prec e || is_or b
+        then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr b
+        else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr b
+
   | BOr (a, b) ->
-    print_lh fmt print_bool_expr be_prec a be_prec e;
-    Format.fprintf fmt "@ \\/@ ";
-    print_rh fmt print_bool_expr be_prec b be_prec e
+    print_ch fmt print_bool_expr be_prec a be_prec e;
+    Format.fprintf fmt "@ ∨ ";
+    print_ch fmt print_bool_expr be_prec b be_prec e
   | BNot (a) ->
-    Format.pp_print_string fmt "!";
-    print_rh fmt print_bool_expr be_prec a be_prec e
+    Format.pp_print_string fmt "¬";
+    print_ch fmt print_bool_expr be_prec a be_prec e
+
+let print_expr fmt e =
+  Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr e
+
+
+(* Print constraint list form of formula *)
+
+let print_cons fmt (eq, sg) =
+  let sg_str = match sg with
+  | CONS_EQ -> "="
+  | CONS_NE -> "≠"
+  | CONS_GT -> ">"
+  | CONS_GE -> "≥"
+  in
+  Format.fprintf fmt "@[<hv 2>%a %s 0@]"
+    print_num_expr eq sg_str
+
+let rec print_conslist fmt (cons, e) =
+  let rec aux = function
+    | [] -> false
+    | [a] ->
+      Format.fprintf fmt "@[<hv 2>%a@]" print_cons a; true
+    | p::q ->
+      Format.fprintf fmt "@[<hv 2>%a@]" print_cons p;
+      Format.fprintf fmt "@ ∧ ";
+      aux q
+  in
+  match e with
+  | CLTrue ->
+    Format.fprintf fmt "@[<hv 2>(";
+    ignore (aux cons);
+    Format.fprintf fmt ")@]"
+  | CLFalse -> 
+    Format.fprintf fmt "false"
+  | _ ->
+    Format.fprintf fmt "@[<hv 2>(";
+    if aux cons then Format.fprintf fmt "@ ∧ ";
+    print_conslist_expr fmt e;
+    Format.fprintf fmt ")@]"
+
+and print_conslist_expr fmt = function
+  | CLTrue -> Format.fprintf fmt "true"
+  | CLFalse -> Format.fprintf fmt "false"
+  | CLOr(a, b) ->
+    Format.fprintf fmt "@[<hv 2>(%a@ ∨ %a)@]"
+        print_conslist a
+        print_conslist b
+  | CLAnd(a, b) ->
+    Format.fprintf fmt "%a@ ∧ %a"
+        print_conslist_expr a
+        print_conslist_expr b
+
 
-let print_expr = print_bool_expr
diff --git a/abstract/transform.ml b/abstract/transform.ml
new file mode 100644
index 0000000..56d54ce
--- /dev/null
+++ b/abstract/transform.ml
@@ -0,0 +1,203 @@
+open Ast
+open Util
+open Ast_util
+open Formula
+
+open Interpret  (* used for constant evaluation ! *)
+
+
+(* Transform SCADE program to logical formula. *)
+
+(* node * prefix * equations *)
+type scope = id * id * eqn ext list
+
+type transform_data = {
+    p           : Ast.prog;
+    consts      : I.value VarMap.t;
+    root_scope  : scope;
+    (* 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
+*)
+let rec f_of_nexpr td (node, prefix) where expr =
+  let sub = f_of_nexpr td (node, prefix) in
+  match fst expr with
+  (* ident *)
+  | AST_identifier(id, _) -> where [NIdent (node^"/"^id)]
+  | AST_idconst(id, _) ->
+    begin let x = VarMap.find ("cst/"^id) td.consts in
+      try where [NIntConst (I.as_int x)]
+      with _ -> try where [NRealConst (I.as_real x)]
+      with _ -> error "Invalid data for supposedly numerical constant."
+    end
+  (* numerical *)
+  | AST_int_const(i, _) -> where [NIntConst(int_of_string i)]
+  | AST_real_const(r, _) -> where [NRealConst(float_of_string r)]
+  | AST_unary(op, e) ->
+    sub (function
+      | [x] -> where [NUnary(op, x)]
+      | _ -> invalid_arity "Unary operator") e
+  | AST_binary(op, a, b) ->
+    sub (function
+      | [x] ->
+        sub (function
+          | [y] -> where [NBinary(op, x, y)]
+          | _ -> invalid_arity "binary_operator") b
+      | _ -> invalid_arity "binary operator") a
+  (* 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))
+  (* 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))
+  | 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_of_expr :
+    transform_data -> (string, string) -> expr -> bool_expr
+*)
+and f_of_bexpr td (node, prefix) 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_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"
+  
+  
+
+and f_of_scope active td (node, prefix, eqs) =
+  let expr_eq e eq =
+    let instance_eq (id, eqs, args) =
+      let eq = f_of_scope active td (node^"/"^id, "", eqs) in
+      if active then
+        List.fold_left (fun eq ((_,(argname,_),_), expr) ->
+            let eq_arg = f_of_nexpr td (node, prefix) (function
+                  | [v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
+                  | _ -> invalid_arity "in argument")
+                expr
+            in f_and eq eq_arg)
+        eq args
+      else
+        eq
+    in
+    let eq = List.fold_left (fun x i -> f_and (instance_eq i) x)
+      eq (extract_instances td.p e)
+    in
+    let pre_expr (id, expr) =
+      if active then
+        f_of_nexpr td (node, prefix) (function
+            | [v] -> BRel(AST_EQ, NIdent("N"^id), v)
+            | _ -> invalid_arity "pre on complex data not supported")
+          expr
+      else
+        BRel(AST_EQ, NIdent("N"^id), NIdent id)
+    in
+    List.fold_left (fun x i -> f_and (pre_expr i) x)
+      eq (extract_pre e)
+  in
+  let do_eq eq = match fst eq with
+    | AST_assign(ids, e) ->
+      let assign_eq = 
+        if active then
+          f_of_nexpr td (node, prefix)
+            (fun vs ->
+              let rels = 
+                List.map2 (fun (id, _) v -> BRel(AST_EQ, NIdent (node^"/"^id), v))
+                ids vs
+              in
+                list_fold_op f_and rels)
+            e
+        else
+          BConst true
+      in
+        expr_eq e assign_eq
+    | AST_assume (_, e) ->
+      if active then
+        f_of_bexpr td (node, prefix) e
+      else
+        BConst true
+    | AST_guarantee _ -> BConst true
+    | AST_activate (b, _) ->
+      let rec cond_eq = function
+        | AST_activate_body b -> BConst true
+        | AST_activate_if(c, a, b) ->
+          f_and (expr_eq c (BConst true))
+            (f_and (cond_eq a) (cond_eq b))
+      in
+      let rec do_tree_act = function
+        | 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))
+          )
+      and do_tree_inact = function
+        | AST_activate_body b ->
+          f_of_scope false td (node, b.act_id^"_", b.body)
+        | AST_activate_if(_, a, b) ->
+          f_and (do_tree_inact a) (do_tree_inact b)
+      in
+        f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
+    | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
+  in
+  let time_incr_eq =
+    if active then
+      BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
+          NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
+    else
+      BRel(AST_EQ,
+          NIdent("N"^node^"/"^prefix^"time"),
+          NIdent(node^"/"^prefix^"time"))
+  in
+  List.fold_left f_and
+    time_incr_eq
+    (List.map do_eq eqs)
+
+and f_of_prog p root =
+    let (n, _) = find_node_decl p root in
+    let root_scope = ("", "", n.body) in
+    let td = {
+      root_scope = root_scope;
+      p = p;
+      consts = I.consts p root;
+    } in
+
+    f_of_scope true td td.root_scope
+