diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | abstract/formula.ml | 78 | ||||
| -rw-r--r-- | abstract/formula_printer.ml | 133 | ||||
| -rw-r--r-- | abstract/transform.ml | 203 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 6 | ||||
| -rw-r--r-- | interpret/ast_util.ml | 2 | ||||
| -rw-r--r-- | interpret/interface.ml | 6 | ||||
| -rw-r--r-- | interpret/interpret.ml | 2 | ||||
| -rw-r--r-- | libs/util.ml | 8 | ||||
| -rw-r--r-- | main.ml | 6 |
10 files changed, 418 insertions, 31 deletions
@@ -10,6 +10,7 @@ SRC= main.ml \ frontend/ast_printer.ml \ abstract/formula.ml \ abstract/formula_printer.ml \ + abstract/transform.ml \ interpret/bad_interpret.ml \ interpret/interface.ml \ interpret/interpret.ml \ @@ -18,8 +19,8 @@ SRC= main.ml \ all: $(BIN) $(BIN): $(SRC) - ocamlbuild -Is $(SRCDIRS) -cflags '-I +zarith -I +apron -I +gmp' \ - -lflags '-I +zarith -I +apron -I +gmp zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa' \ + ocamlbuild -Is $(SRCDIRS) -cflags '-I +zarith -I +apron -I +gmp -I +str' \ + -lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa' \ main.native mv main.native $(BIN) 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 + diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index b6dcdbc..641e4fd 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -52,8 +52,8 @@ let binary_rel_precedence = function | AST_EQ | AST_NE -> 41 | AST_LT | AST_LE | AST_GT | AST_GE -> 40 let binary_bool_precedence = function - | AST_AND -> 31 - | AST_OR -> 30 + | AST_OR -> 31 + | AST_AND -> 30 let arrow_precedence = 20 let if_precedence = 10 @@ -127,7 +127,7 @@ let rec print_expr fmt e = then Format.fprintf fmt " (%a)" print_expr e2 else Format.fprintf fmt " %a" print_expr e2 | AST_binary_bool (op,(e1,_),(e2,_)) -> - if expr_precedence e1 < expr_precedence e + if expr_precedence e1 <= expr_precedence e then Format.fprintf fmt "(%a) " print_expr e1 else Format.fprintf fmt "%a " print_expr e1; Format.pp_print_string fmt (string_of_binary_bool op); diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml index e7428bd..80411d8 100644 --- a/interpret/ast_util.ml +++ b/interpret/ast_util.ml @@ -70,4 +70,4 @@ let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v) let no_variable e = error ("No such variable: " ^ e) let type_error e = error ("Type error: " ^ e) let not_implemented e = error ("Not implemented: " ^ e) - +let invalid_arity e = error ("Invalid arity (" ^ e ^ ")") diff --git a/interpret/interface.ml b/interpret/interface.ml index 7b84396..621bfa2 100644 --- a/interpret/interface.ml +++ b/interpret/interface.ml @@ -1,4 +1,5 @@ open Ast +open Util module type INTERPRET = sig @@ -24,6 +25,11 @@ module type INTERPRET = sig type io = (id * value) list (* + Get the constants only + *) + val consts : prog -> id -> value VarMap.t + + (* Construct initial state for a program. The id is the root node of the program evaluation. *) diff --git a/interpret/interpret.ml b/interpret/interpret.ml index 063dad0..24903f1 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -451,5 +451,7 @@ module I : INTERPRET = struct do_weak_transitions env st.root_scope; extract_st env, out + let consts p root = + (init_state p root).save end diff --git a/libs/util.ml b/libs/util.ml index 494faac..97aa480 100644 --- a/libs/util.ml +++ b/libs/util.ml @@ -47,3 +47,11 @@ let uid = let c = ref 0 in fun () -> c := !c + 1; string_of_int !c +(* On lists *) + +(* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *) +let rec list_fold_op op = function + | [] -> invalid_arg "list_fold_opt on empty list" + | [a] -> a + | x::q -> op x (list_fold_op op q) + @@ -63,6 +63,12 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; + let prog_f = Formula.eliminate_not (Transform.f_of_prog prog "test") in + Formula_printer.print_expr Format.std_formatter prog_f; + Format.printf "@."; + let prog_f_cl = Formula.conslist_of_f prog_f in + Formula_printer.print_conslist Format.std_formatter prog_f_cl; + if !vtest then do_test_interpret prog true else if !test then do_test_interpret prog false; |