From d57e3491720e912b4e2fd6c73f9d356901a42df5 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 17 Jun 2014 14:34:40 +0200 Subject: Write transformation of program into logical formula. --- abstract/formula.ml | 78 +++++++++++++++++ abstract/formula_printer.ml | 133 +++++++++++++++++++++++------ abstract/transform.ml | 203 ++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 389 insertions(+), 25 deletions(-) create mode 100644 abstract/transform.ml (limited to 'abstract') 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 "@[(%a)@]" pf a + else Format.fprintf fmt "@[%a@]" pf a +let print_ah fmt pf fa a fe e = + if fa a <= fe e + then Format.fprintf fmt "@[(%a)@]" pf a + else Format.fprintf fmt "@[%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 "@[(%a)@]" print_bool_expr a + else Format.fprintf fmt "@[%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 "@[(%a)@]" print_bool_expr b + else Format.fprintf fmt "@[%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 "@[%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 "@[%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 "@[%a@]" print_cons a; true + | p::q -> + Format.fprintf fmt "@[%a@]" print_cons p; + Format.fprintf fmt "@ ∧ "; + aux q + in + match e with + | CLTrue -> + Format.fprintf fmt "@[("; + ignore (aux cons); + Format.fprintf fmt ")@]" + | CLFalse -> + Format.fprintf fmt "false" + | _ -> + Format.fprintf fmt "@[("; + 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 "@[(%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 + -- cgit v1.2.3