Skip to content

GitLab

Commit cf6901e9 authored by Pascal Raymond's avatar Pascal Raymond
Browse files

lutexe: add weak/strong assert/loop 

deterministic subset seems to work
parent b235802a
Hide whitespace changes
Inline Side-by-side
source/Lutin/checkType.ml
View file @ cf6901e9
......@@ -122,7 +122,7 @@ printf "check_exp\n";
let tel = rec_list_call [e1;e2] in
match_type_profile tel CkTypeEff.prof_tt_t e.src
)
| LOOP_n e1 -> (
| LOOP_n (_,e1) -> (
let tel = rec_list_call [e1] in
match_type_profile tel CkTypeEff.prof_t_t e.src
)
......@@ -144,7 +144,7 @@ printf "check_exp\n";
let tel = rec_list_call [av;e1] in
match_type_profile tel CkTypeEff.prof_it_t e.src
)
| ASSERT_n (c, e1) -> (
| ASSERT_n (_, c, e1) -> (
let tel = rec_list_call [c;e1] in
match_type_profile tel CkTypeEff.prof_bt_t e.src
)
......
source/Lutin/coTraceExp.ml
View file @ cf6901e9
......@@ -52,6 +52,7 @@ type t =
| TE_choice of (t * CoAlgExp.t option) list
| TE_noeps of t
| TE_loop of t
| TE_omega of t
(* version pour génération d'automates complets *)
| TE_loopi of int * CoAlgExp.t * CoAlgExp.t * t
| TE_loopa of int * CoAlgExp.t * CoAlgExp.t option * t
......@@ -59,6 +60,7 @@ type t =
| TE_loopg of (int -> int * int) * int * t
| TE_assert of CoAlgExp.t * t
| TE_strong_assert of CoAlgExp.t * t
(* Takes a list (id,val) *)
| TE_exist of escope * t
| TE_raise of string
......@@ -70,6 +72,7 @@ type t =
let of_constraint (ea : CoAlgExp.t) = ( TE_constraint ea )
let of_ref (s : CoIdent.t) = ( TE_ref s )
let of_loop (e : t) = (TE_loop e)
let of_omega (e : t) = (TE_omega e)
let of_noeps (e : t) = (TE_noeps e)
let of_fby (e1 : t) (e2 : t) = (TE_fby (e1,e2))
let of_choice lst = TE_choice lst
......@@ -83,6 +86,7 @@ let of_loopa moy ect e = (TE_loopa (new_loop_cpt (), moy,ect,e))
let of_loopg getweights cpt e = (TE_loopg (getweights, cpt, e))
let of_assert c e = (TE_assert (c,e))
let of_strong_assert c e = (TE_strong_assert (c,e))
let of_exist ctx e = (TE_exist (ctx,e))
......@@ -133,6 +137,12 @@ let rec _dump (pr: string -> unit) te = (
| TE_choice _ -> _dump pr te
| _ -> pr "{"; _dump pr te; pr "}"
)
| TE_omega te -> (
pr "loop omega ";
match te with
| TE_choice _ -> _dump pr te
| _ -> pr "{"; _dump pr te; pr "}"
)
| TE_noeps te -> (
pr "noeps ";
match te with
......@@ -170,6 +180,12 @@ let rec _dump (pr: string -> unit) te = (
pr "assert ";
pr (CoAlgExp.lus_dumps a) ;
pr " in ";
_dump pr e ;
)
| TE_strong_assert (a, e) -> (
pr "strong assert ";
pr (CoAlgExp.lus_dumps a) ;
pr " in ";
_dump pr e ;
)
| TE_exist (ctx,e) -> (
......
source/Lutin/coTraceExp.mli
View file @ cf6901e9
......@@ -32,11 +32,13 @@ type t =
| TE_choice of (t * CoAlgExp.t option) list
| TE_noeps of t
| TE_loop of t
| TE_omega of t
| TE_loopi of int * CoAlgExp.t * CoAlgExp.t * t
| TE_loopa of int * CoAlgExp.t * CoAlgExp.t option * t
(* internal loop with inline weigth computer + compteur *)
| TE_loopg of (int -> int * int) * int * t
| TE_assert of CoAlgExp.t * t
| TE_strong_assert of CoAlgExp.t * t
| TE_exist of escope * t
| TE_raise of string
| TE_try of t * t option
......@@ -59,6 +61,7 @@ val of_constraint : CoAlgExp.t -> t
val of_ref : CoIdent.t -> t
val of_loop : t -> t
val of_omega : t -> t
val of_loope : CoAlgExp.t -> t -> t
......@@ -77,6 +80,7 @@ val of_para : t list -> t
val of_choice : (t * CoAlgExp.t option ) list -> t
val of_assert : CoAlgExp.t -> t -> t
val of_strong_assert : CoAlgExp.t -> t -> t
val of_exist : escope -> t -> t
......
source/Lutin/expand.ml
View file @ cf6901e9
......@@ -1244,9 +1244,11 @@ and
) in
CoTraceExp.of_choice (List.map doit chargs)
)
| LOOP_n ee -> (
| LOOP_n (f,ee) -> (
let arg = treat_trace env sstack ee in
CoTraceExp.of_loop arg
match f with
| Weak -> CoTraceExp.of_loop arg
| Strong -> CoTraceExp.of_omega arg
)
| LOOPI_n (emin,emax,ee) -> (
let minres = treat_exp env sstack emin in
......@@ -1281,10 +1283,12 @@ and
CoTraceExp.of_loopa moyres None eres
)
)
| ASSERT_n (c,ee) -> (
| ASSERT_n (f,c,ee) -> (
let cres = treat_exp env sstack c in
let eres = treat_trace env sstack ee in
CoTraceExp.of_assert cres eres
match f with
| Weak -> CoTraceExp.of_assert cres eres
| Strong -> CoTraceExp.of_strong_assert cres eres
)
| RAISE_n id -> (
(* le programme est correct, DONC tgtid existe !! *)
......
source/Lutin/lutExe.ml
View file @ cf6901e9
......@@ -314,19 +314,22 @@ fun it tfdn tn g -> (
g
"LutExe.is_bool_sat" (* msg: string (?) *)
in
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
!solver_vl (* vl: int *)
"LutExe.solve_guard" (* msg: string *)
[it.out_var_names] (* output_var_names: Var.name list list *)
tfdn (* p: Thickness.formula_draw_nb *)
tn (* num_thickness Thickness.numeric *)
it.bool_vars_to_gen (* bool_vars_to_gen_f: formula *)
it.num_vars_to_gen (* num_vars_to_gen: var list *)
g (* f: formula *)
in sols
if not is_bool_sat then (
[]
) else (
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
!solver_vl (* vl: int *)
"LutExe.solve_guard" (* msg: string *)
[it.out_var_names] (* output_var_names: Var.name list list *)
tfdn (* p: Thickness.formula_draw_nb *)
tn (* num_thickness Thickness.numeric *)
it.bool_vars_to_gen (* bool_vars_to_gen_f: formula *)
it.num_vars_to_gen (* num_vars_to_gen: var list *)
g (* f: formula *)
in sols
)
)
let find_one_sol it g = (
......@@ -546,6 +549,73 @@ let genpath
rec_genpath ((List.map dobr tel)@other_brs)
)
(** Try similar to a recurse priority *)
| TE_try (e,eco) -> (
let try_cont a = (
Verbose.put ~flag:dbg "-- try_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x);
match a with
| Goto (cl,n) -> cont (Goto (cl, TE_try (n,eco)))
| _ -> cont a
) in
let new_other_brs = match eco with
| None -> other_brs
| Some ec -> {br with br_ctrl=ec}::other_brs
in
rec_genpath ({br with br_ctrl=e; br_cont=try_cont}::new_other_brs)
)
(** INFINITE WEAK LOOP *)
(* must behaves exactly as: (te\eps fby loop te) |> eps *)
| TE_loop te -> (
let e' =
TE_prio [
put_in_seq (TE_noeps te) (TE_loop te)
;
TE_eps
]
in
rec_genpath ({br with br_ctrl=e'}::other_brs)
)
(** INFINITE STRONG LOOP *)
(* must behaves exactly as: (te fby loop te) *)
| TE_omega te -> (
let e' = put_in_seq te (TE_omega te)
in
rec_genpath ({br with br_ctrl=e'}::other_brs)
)
(** ASSERT *)
(* default assert is WEAK for backward compatibility
must behave EXACTLY as
trap STOP in (te fby raise STOP) &> omega a
*)
| TE_assert (a, te) -> (
let stopid = CoIdent.get_fresh "Stop_loop" in
let e' = TE_catch (
stopid,
put_in_para
(put_in_seq te (TE_raise stopid))
(TE_omega (TE_constraint a))
,
None
) in
rec_genpath ({br with br_ctrl=e'}::other_brs)
)
(** STRONG ASSERT *)
(* must behave EXACTLY as
trap STOP in omega a &> (te fby raise STOP)
*)
| TE_strong_assert (a, te) -> (
let stopid = CoIdent.get_fresh "Stop_loop" in
let e' = TE_catch (
stopid,
put_in_para
(TE_omega (TE_constraint a))
(put_in_seq te (TE_raise stopid))
,
None
) in
rec_genpath ({br with br_ctrl=e'}::other_brs)
)
(** Exist: problem modifies the data and support, and the cont *)
| TE_exist (ectx, te) -> (
let addp inpres (id, eo) = (
......@@ -600,7 +670,7 @@ let genpath
)
)
) in
rec_genpath ({br with br_cont=para_head_cont}::other_brs)
rec_genpath ({br with br_ctrl=e; br_cont=para_head_cont}::other_brs)
)
(** No eps: forbids e to vanish (but not to raise !) *)
......@@ -631,32 +701,10 @@ let genpath
)
) else cont (Raise x)
)
| _ -> cont a
) in
rec_genpath ({br with br_ctrl=e ; br_cont=catch_cont}::other_brs)
)
(** Assert: problem, should it be equivalent to
"te &> omega(a)"
or
"omega(a) &> te" ?
*)
(*
| TE_assert (a, te) -> (
let rec_cont = ( function
| Goto (cl,n) -> cont (Goto (cl, TE_assert (a,n)))
| _ -> cont c
) in
(* HERE: CONTINUE EVEN IF IT IS UNSAT *)
try (
let rec_acc = Guard.add ~unalias:unalias ~context:data a acc in
rec_genpath data te rec_acc rec_cont
) with Guard.Unsat -> (
(* HERE: cont or not cont ???? *)
Verbose.put ~flag:dbg " !!!!! CUT A BRANCH\n";
cont None
)
)
*)
(**** CHOIX *****)
(*
| TE_choice wtel -> (
......@@ -671,31 +719,6 @@ let genpath
[] -> None
| ttlist -> Some (Split ttlist)
)
*)
(*** BOUCLE "INFINIE" ***)
(*
| TE_loop te -> (
let rec_cont = ( function
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, put_in_seq n x)))
| Vanish -> None
| _ -> cont (Some c)
)
) in
(* on génère en priorité les cas ``boucle'' *)
let goon = rec_genpath data te acc rec_cont in
(* on considère aussi le cas vanish *)
let stop = cont (Some Vanish) in
match (goon,stop) with
(None,None) -> None
| (Some g, None) -> Some g
| (None, Some s) -> Some s
| (Some g, Some s) -> Some
(Split [(g, Some huge_weight, Guard.empty) ; (s, None, Guard.empty)])
)
*)
(*** BOUCLE intervale ****)
(*
......@@ -767,55 +790,6 @@ let genpath
(Split [(g, Some (W_exp gw), Guard.of_exp ga) ; (s, Some (W_exp sw), Guard.of_exp sa)])
)
)
*)
(** on appèle recursivement le traitement de e avec un nouveau raise callback :
- si le callback est levé avec i, appèle recursivement :
* si eco = Some ec : ec avec les callbacks de l'appel
* sinon le vanish de l'appel
- sinon appèle le callback raise de l'appel
ET avec un nouveau goto callback :
* goto(cl,n) => goto(cl, catch(i,n,eco))
*)
(** TRY *)
(* optimisation : try(eps,_) = eps *)
(*
| TE_try (TE_eps,_) -> cont (Some Vanish)
| TE_try (e,eco) -> (
(** on créé un choix binaire entre :
- priorité (poids infini) e avec un nouveau goto callback :
* goto(cl,n) -> goto(cl, try(n,eco))
- sinon :
* si "eco = Some ec" alors appel rec. sur ec
* si "eco = None" alors appel du vanish
*)
(* la branche prio *)
let rec_cont = ( function
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, TE_try(n,eco))))
| _ -> cont (Some c)
)
) in
let prio = rec_genpath data e acc rec_cont in
(* la branche par defaut *)
let defaut = ( match eco with
| Some ec -> (
rec_genpath data ec acc cont
)
| None -> cont (Some Vanish)
) in
match (prio,defaut) with
(None,None) -> None
| (Some p, None) -> Some p
| (None, Some d) -> Some d
| (Some p, Some d) -> (
Some
(Split [(p, Some huge_weight, Guard.empty) ; (d, None, Guard.empty)])
)
)
*)
) in
(* Top-level branch *)
......
source/Lutin/lutLexer.mll
View file @ cf6901e9
......@@ -28,6 +28,8 @@ Hashtbl.add keywords "node" (function s -> TK_NODE s) ;;
Hashtbl.add keywords "extern" (function s -> TK_EXTERN s) ;;
Hashtbl.add keywords "system" (function s -> TK_SYSTEM s) ;;
Hashtbl.add keywords "returns" (function s -> TK_RETURNS s) ;;
Hashtbl.add keywords "weak" (function s -> TK_WEAK s) ;;
Hashtbl.add keywords "strong" (function s -> TK_STRONG s) ;;
Hashtbl.add keywords "assert" (function s -> TK_ASSERT s) ;;
Hashtbl.add keywords "raise" (function s -> TK_RAISE s) ;;
Hashtbl.add keywords "try" (function s -> TK_TRY s) ;;
......@@ -85,6 +87,8 @@ let token_code tk = (
| TK_NODE lxm -> ("TK_NODE", lxm)
| TK_SYSTEM lxm -> ("TK_SYSTEM", lxm)
| TK_RETURNS lxm -> ("TK_RETURNS", lxm)
| TK_WEAK lxm -> ("TK_WEAK", lxm)
| TK_STRONG lxm -> ("TK_STRONG", lxm)
| TK_ASSERT lxm -> ("TK_ASSERT", lxm)
| TK_RAISE lxm -> ("TK_RAISE", lxm)
| TK_TRY lxm -> ("TK_TRY", lxm)
......
source/Lutin/lutParser.mly
View file @ cf6901e9
......@@ -129,6 +129,8 @@ let make_val_exp ven lxm = {
%token <Lexeme.t> TK_RETURNS
%token <Lexeme.t> TK_EXIST
%token <Lexeme.t> TK_WEAK
%token <Lexeme.t> TK_STRONG
%token <Lexeme.t> TK_ASSERT
%token <Lexeme.t> TK_RAISE
%token <Lexeme.t> TK_TRY
......@@ -497,6 +499,15 @@ lutFunctionInType:
/* ebnf:group=statements */
lutAssertFlag:
TK_STRONG
{ Strong }
| TK_WEAK
{ Weak }
| /* nada */
{ Weak }
;
lutTraceExp:
/* ``feuilles''
*/
......@@ -511,6 +522,8 @@ lutTraceExp:
{ make_val_exp (FBY_n ($1,$3)) $2}
| lutLoopExp
{ $1 }
| lutLoopStatExp
{ $1 }
/*
les combinateurs entre accolades
*/
......@@ -522,8 +535,8 @@ lutTraceExp:
*/
| lutLetDecl TK_IN lutTraceExp
{ make_val_exp (LET_n (snd $1,$3)) ((fst $1).src) }
| TK_ASSERT lutExp TK_IN lutTraceExp
{ make_val_exp (ASSERT_n ($2,$4)) $1 }
| lutAssertFlag TK_ASSERT lutExp TK_IN lutTraceExp
{ make_val_exp (ASSERT_n ($1,$3,$5)) $2 }
| TK_EXIST lutTypedIdentList TK_IN lutTraceExp
{ make_val_exp (EXIST_n (List.rev $2,$4)) $1 }
| TK_EXCEPTION lutIdentList TK_IN lutTraceExp
......@@ -569,12 +582,17 @@ lutDoPart :
;
lutLoopExp:
TK_LOOP lutTraceExp
{ make_val_exp (LOOP_n $2) $1 }
/* | TK_LOOP lutExact lutTraceExp
{ make_val_exp (LOOPE_n ($2, $3)) $1 }
*/
| TK_LOOP lutAverage lutTraceExp
TK_LOOP lutTraceExp
{ make_val_exp (LOOP_n (Weak,$2)) $1 }
| TK_STRONG TK_LOOP lutTraceExp
{ make_val_exp (LOOP_n (Strong,$3)) $2 }
| TK_WEAK TK_LOOP lutTraceExp
{ make_val_exp (LOOP_n (Weak,$3)) $2 }
;
lutLoopStatExp:
TK_LOOP lutAverage lutTraceExp
{ make_val_exp (LOOPI_n (fst $2, snd $2, $3)) $1 }
| TK_LOOP lutGaussian lutTraceExp
{ make_val_exp (LOOPA_n (fst $2, snd $2, $3)) $1 }
......
source/Lutin/syntaxe.ml
View file @ cf6901e9
......@@ -86,6 +86,7 @@ and node_info = {
}
(* exp *)
and val_exp = val_exp_node srcflaged
and assert_flag = Strong | Weak
and val_exp_node =
(* zeroaire *)
TRUE_n
......@@ -98,11 +99,11 @@ and val_exp_node =
| FBY_n of val_exp * val_exp
| CHOICE_n of (val_exp * val_exp srcflaged option) list
| PRIO_n of val_exp list
| LOOP_n of val_exp
| LOOP_n of assert_flag *val_exp
(* | LOOPE_n of val_exp * val_exp *)
| LOOPI_n of val_exp * val_exp * val_exp
| LOOPA_n of val_exp * val_exp option * val_exp
| ASSERT_n of val_exp * val_exp
| ASSERT_n of assert_flag * val_exp * val_exp
| EXIST_n of (ident * type_exp * val_exp option * (val_exp * val_exp) option) list * val_exp
| RAISE_n of ident
| EXCEPT_n of ident list * val_exp
......
source/Lutin/syntaxeDump.ml
View file @ cf6901e9
......@@ -263,8 +263,11 @@ let _ =
iter_sep dump_brace_exp (fun _ -> (Format.fprintf !os "@]@\n&&@[<h 3>@\n")) el;
Format.fprintf !os "@]@\n}"
)
| LOOP_n e -> (
Format.fprintf !os "loop ";
| LOOP_n (f,e) -> (
let _ = match f with
| Strong -> Format.fprintf !os "strong loop ";
| Weak -> Format.fprintf !os "loop ";
in
dump_brace_exp e
)
(*
......@@ -294,8 +297,11 @@ let _ =
);
dump_brace_exp e
)
| ASSERT_n (a, e) -> (
Format.fprintf !os "assert ";
| ASSERT_n (f, a, e) -> (
let _ = match f with
| Strong -> Format.fprintf !os "strong assert ";
| Weak -> Format.fprintf !os "assert ";
in
dump_exp a ;
Format.fprintf !os " in ";
dump_brace_exp e ;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment