Commit 9d0c853a authored by erwan's avatar erwan

Update: monadisation of Lutin, part 4.

Rationale: make rdbg time traveling work.
parent 7a6ac267
......@@ -27,7 +27,7 @@ Executable lutin
Path: lutin/src
MainIs: main.ml
BuildDepends: str,unix,num,rdbg-plugin (>= 1.177),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp
NativeOpt: -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
NativeOpt: -warn-error "+26" -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Build: true
Install:true
CompiledObject: native
......
......@@ -73,7 +73,7 @@ let main_read_arg () =
args.tmp_dir <- lurette_tmp_dir;
Unix.putenv "TMPDIR" (String.escaped lurette_tmp_dir) ;
in
let source_dir = (Filename.concat (ExtTools.lurette_path()) "source") in
let _source_dir = (Filename.concat (ExtTools.lurette_path()) "source") in
match args.sut_compiler with
| Scade -> assert false
| VerimagV4
......
......@@ -89,7 +89,7 @@ let (make_rp_list : reactive_program list ->
(Data.subst list -> ctx -> (Data.subst list -> ctx -> Event.t) ->
Event.t) list * Data.subst list list * Data.subst list list) =
fun rpl ->
let add_init init (a,b,c,d,e) = (a,b,c,d,e,init,init) in
let _add_init init (a,b,c,d,e) = (a,b,c,d,e,init,init) in
let aux rp =
let plugin =
match rp with
......
(* Time-stamp: <modified the 29/03/2019 (at 14:53) by Erwan Jahier> *)
(* Time-stamp: <modified the 11/04/2019 (at 14:56) by Erwan Jahier> *)
(* Mimick the behavior of 'rdbg -lurette', but without the dependency
on ocaml *)
open Event
......@@ -77,11 +77,11 @@ let _ =
args.verbose <- if !verbose then 1 else 0 ;
args.output <- !output_file ;
args.overwrite_output = !overwrite_output;
args.stop_on_oracle_error = not !dont_stop_on_oracle_error;
args.log = !log;
args.cov_file = !cov_file;
args.reset_cov_file = !reset_cov_file;
args.overwrite_output <- !overwrite_output;
args.stop_on_oracle_error <- not !dont_stop_on_oracle_error;
args.log <- !log;
args.cov_file <- !cov_file;
args.reset_cov_file <- !reset_cov_file;
args.debug_rdbg <- !drdbg;
args.rdbg <- false;
......
......@@ -42,13 +42,13 @@ let print_header
)
open Util
let make
(srcname: string)
(mnode : string)
(auto : AutoGen.t)
(os : Pervasives.out_channel) =
(
(* le source au cas ou ... *)
let source_code = AutoGen.source auto in
......@@ -61,8 +61,7 @@ let make
let etab2prof s xi acc = (
(s, xi.xi_prof)::acc
) in
let xlist = Hashtbl.fold etab2prof
(Expand.extern_tab source_code) [] in
let xlist = Util.StringMap.fold etab2prof (Expand.extern_tab source_code) [] in
if (xlist = []) then ()
else (
fprintf os "\nfunctions {\n";
......@@ -79,7 +78,7 @@ let make
(* pour les dumps des vars support *)
(* Hashtbl.iter (print_support Local) (Expand.support_tab source_code); *)
let print_support nme = (
let info = Util.hfind (Expand.support_tab source_code) nme in
let info = Util.StringMap.find nme (Expand.support_tab source_code) in
fprintf os " %s : %s"
(CoIdent.to_string nme)
(CkTypeEff.to_string info.si_type);
......@@ -104,8 +103,7 @@ let make
(* pour les dumps de la liste d'alias *)
let print_alias nme = (
let info = Util.hfind
(Expand.alias_tab source_code) nme in
let info = StringMap.find nme (Expand.alias_tab source_code) in
fprintf os " %s : %s"
(CoIdent.to_string nme)
(CkTypeEff.to_string info.ai_type);
......
(**
ON THE FLY generation of automata
For full automata gen. see AutoGen
*)
open LutErrors;;
open Printf;;
open CoIdent ;;
open CoAlgExp ;;
open CoTraceExp ;;
open LutPredef ;;
open Expand ;;
let dbg = Verbose.get_flag "AutoExplore"
(** N.B. On utilise des AlgExp.t de type "CkTypeEff.weight" pour
reprsenter les poids dans les transitions *)
(* tree-like transitions:
- leaves:
"Vanish" for normal termination
"Raise exception" for abnormal termination
"Goto" for an actual transition
- n-ary node with weights
*)
(** WEIGHTS *)
type weightexp =
| W_huge
| W_exp of CoAlgExp.t
let opt_weight_of_opt_algexp = function
| None -> None
| Some e -> Some (
if (e = CoAlgExp.of_huge_weight) then W_huge
else W_exp e
)
let huge_weight = W_huge
(** EXCEPTIONS *)
type raise_desc = string
(** GOTO *)
type stable_state = CoTraceExp.t
(* type cond = CoAlgExp.t list *)
type cond = Guard.t
type goto = cond * stable_state
(** TRANSITION TREE *)
type ttree =
Vanish
| Raise of raise_desc
| Goto of goto
| Split of (ttree * weightexp option * cond) list
let ttree_stats = function
| None -> "empty ttree"
| Some t -> (
let rec f t = (
match t with
| Split l -> (
let g (nn0, nf0) (t,_,_) = (
let (nn, nf) = f t in
(nn0+nn,nf0+nf)
) in
List.fold_left g (1,0) l
)
| _ -> (0, 1)
) in
let (nn, nf) = f t in
Printf.sprintf "nodes:%d, leaves:%d" nn nf
)
(* DATA CONTEXT managment (for simulation) *)
type config = { data: Guard.store option; control: string }
let make_config dataopt ctrl =
let st = match dataopt with
| None -> None
| Some (i,p) -> Some { Guard.curs = i; Guard.pres = p}
in { data = st; control = ctrl }
(** STATE MANAGMENT *)
type state_info =
SS_stable of CoTraceExp.t
| SS_transient
| SS_final of string
(* POINT TO POINT TRANSITION:
intermediate representation
for full automaton generation *)
type trans = {
src: string;
wgt: weightexp option;
form: cond;
dest: string;
}
(* THE MAIN TYPE
- (control) states are CoTraceExp.t
- (control) states are hashed, and labelled by a unique string
- a config is a variable config + a (control) state
*)
type t = {
source_code : Expand.t;
mutable nb_stables : int;
mutable nb_transients : int;
mutable init_control : string;
mutable final_control : string;
states : (string, state_info) Hashtbl.t ;
mutable transitions : trans list;
(* Gestion des puits *)
mutable nb_sinks : int;
_state2trace : (string, CoTraceExp.t) Hashtbl.t ;
_trace2state : (CoTraceExp.t, string) Hashtbl.t;
_config2ttree : (config, ttree) Hashtbl.t;
(* liste des control inexplors *)
mutable todo : string list;
(* mode global/dynamique *)
}
(* Misc infos *)
let source (it:t) = it.source_code
let states (it:t) = it.states
let init_control (it:t) = it.init_control
let transitions (it:t) = it.transitions
(* ADD/REPLACE pre values in data strore *)
let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.escope) = (
match pctx with
| [] -> data
| _ -> (
let ctx = match data with
| Some d -> d
| None -> Guard.empty_store
in
let addp accin (id, eo) = (
match eo with
| None -> accin
| Some e -> (
let v = try (
Guard.value_of_algexp unalias ctx e
) with Guard.Not_constant e -> raise (Internal_error ("AutoExplore.add_pres",
("initial value of \""^id^"\" must be a constant expression")))
in
Value.OfIdent.add accin (id, v)
)
) in
let new_pres = List.fold_left addp ctx.Guard.pres pctx in
Some {Guard.curs=ctx.Guard.curs; Guard.pres=new_pres}
)
)
let get_cpt i = CoIdent.of_cpt i
let dynamic_weight_exp (f : string) (c : int) (args : CoAlgExp.t list) = (
let pcpt = CoAlgExp.of_pre (get_cpt c) CkTypeEff.integer in
CoAlgExp.of_call (CoIdent.from_string f) CkTypeEff.integer (pcpt::args)
)
let incr_loop_cpt (c : int) = (
let nme = get_cpt c in
let precpt = CoAlgExp.of_pre nme CkTypeEff.integer in
let cpt = CoAlgExp.of_support nme CkTypeEff.integer true in
CoAlgExp.of_call (CoIdent.from_string LutPredef.kw_eq) CkTypeEff.boolean [
cpt ;
CoAlgExp.of_call (CoIdent.from_string LutPredef.kw_plus) CkTypeEff.integer [
precpt;
CoAlgExp.of_iconst "1"
]
]
)
let reset_loop_cpt (c : int) = (
let nme = get_cpt c in
let cpt = CoAlgExp.of_support nme CkTypeEff.integer true in
CoAlgExp.of_call (CoIdent.from_string LutPredef.kw_eq) CkTypeEff.boolean [
cpt ;
CoAlgExp.of_iconst "0"
]
)
(** dump des transition branchues pour debug *)
let dump_weight = ( function
| Some W_huge -> printf "huge"
| Some (W_exp w) -> CoAlgExp.dump w
| None -> printf "1"
)
(* obsolete
let (algexp_of_weight: weightexp -> CoAlgExp.t) = (
function w -> w
)
*)
let dump_ttree topt = (
let rec rdump t pfx = (
match t with
Vanish -> (
printf "%sVANISH\n" pfx;
) |
Raise e -> (
printf "%sRAISE %s\n" pfx e;
) |
Goto (c, n) -> (
printf "%sGOTO:[\n" pfx;
printf "%s cond:(" pfx;
(* Utils.iter_sep (CoAlgExp.dump) (function _ -> printf " & ") c ; *)
Guard.dumpf stdout c;
printf " )\n%s next: <" pfx;
CoTraceExp.dump n;
printf ">\n%s]\n" pfx
) |
Split twl -> (
printf "%sSPLIT:\n" pfx;
let recpfx = sprintf "%s " pfx in
let dchoice (t,wo,cl) = (
printf "%s[\n" pfx;
(match wo with
Some w -> (
printf "%sWEIGHT: " recpfx;
dump_weight wo ;
printf "\n"
) | None -> ()
);
printf "%sCOND: (" recpfx;
Guard.dumpf stdout cl;
printf ")\n";
rdump t recpfx ;
printf "%s]\n" pfx
) in
List.iter dchoice twl
)
) in
(
match topt with
None -> printf "%s" LutPredef.kw_deadlock
| Some t -> rdump t ""
);
printf "\n"
)
(****************************************************************************
TRACE -> TRANSITIONS BRANCHUES
-----------------------------------------------------------------------------
C'est essentiellement une fonction :
CkTypeExp.t -> ttree
Le traitement des "feuilles" est ralis par des fonctions
passes en paramtre (callback) :
- terminaisons normales (vanish)
- terminaisons anormales (raise)
- une pour traiter les continuations (goto)
N.B. ces deux fonctions peuvent ne pas rendre de rsultat en cas
de ``DeadLock'' statique.
****************************************************************************)
(** utilitaire : mise en squence tenant compte du TE_eps *)
let put_in_seq te1 te2 = (
if(te1 = TE_eps) then te2
else if(te2 = TE_eps) then te1
else (TE_fby (te1,te2))
)
(** utilitaire : mise en parallle *)
let put_in_para te1 te2 = (
match (te1,te2) with
| (TE_eps, x) -> x
| (x, TE_eps) -> x
| (x, TE_para yl) -> TE_para (x::yl)
| (x,y) -> TE_para [x; y]
)
(* For old algo with several callbacks *)
(** type de la fonction de traitement des vanish *)
type goto_callback = goto -> ttree option
(** type de la fonction de traitement des raise *)
type raise_callback = raise_desc -> ttree option
(** type de la fonction de traitement des goto *)
type vanish_callback = unit -> ttree option
(* For NEW algo with a UNIQUE callback *)
type callback = ttree option -> ttree option
(** CoTraceExp.t -> ttree *)
(* MAIN (RECURSIVE) TRAVERSAL OF A LUTIN STATE
New algo -> 2009 semantics, with:
- inherited acc-umulator for constraints
- all the rest (mainly control) performed by cont-inuation
N.B. cases that impact acc-umulator are:
- TE_constraint
- TE_para and also TE_assert (special case)
with partial evaluation of contraints
*)
let gentrans
(xenv : Expand.t)
(data : Guard.store option) (* data env = inputs + pres *)
(x : CoTraceExp.t) (* control = lutin trace *)
= (
(*-------------------------------------------*)
(* Correspondance id de trace -> trace exp
N.B. on traque les rcursions ? *)
(*-------------------------------------------*)
let id2trace s = (
(Util.hfind (Expand.trace_tab xenv) s).ti_def_exp
) in
let unalias s = (
(Util.hfind (Expand.alias_tab xenv) s).ai_def_exp
) in
(*-------------------------------------------*)
(* LA FONCTION RCURSIVE *)
(*-------------------------------------------*)
let rec rec_gentrans
(data : Guard.store option) (* data env = inputs + pres *)
(x : CoTraceExp.t)
(acc : cond)
(cont : callback)
= (
Verbose.exe ~level:13
(fun () ->
Printf.printf
"rec_gentrans \"%s\"\n" (CoTraceExp.dumps x));
match x with
(***** EPSILON => vanish ... *****)
| TE_eps -> (
cont (Some Vanish)
)
(***** TRACE NOMME => ON CHERCHE SA DEF ******)
| TE_ref s -> (
rec_gentrans data (id2trace s) acc cont
)
(***** CONTRAINTE => on appelle le callback *)
| TE_constraint (ae,si) -> (
(* HERE DO EVAL ! *)
try (
let new_acc = Guard.add ~unalias:unalias ~context:data ae acc si in
(* ICI *)
(* cont (Some (Goto (Guard.of_exp ~unalias:unalias ~context:data ae, TE_eps))) *)
cont (Some (Goto (new_acc, TE_eps)))
) with Guard.Unsat -> (
Verbose.put ~flag:dbg " !!!!! CUT A BRANCH\n";
(* HERE: cont or not cont ???? *)
cont None
)
)
(***** SEQUENCE *****)
(* on gnre la trace de te1 avec :
- goto(cl,n) => goto(cl,n fby te2)
- vanish => te2
*)
| TE_fby (te1, te2) -> (
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 te2)))
| Vanish -> rec_gentrans data te2 acc cont
| _ -> cont (Some c)
)
in
rec_gentrans data te1 acc rec_cont
)
(**** CHOIX *****)
(* chaque choix est trait dans
l'environnement global,
on dcore la branche avec le poids
correspondant et une action vide *)
(* ICI *)
| TE_choice wtel -> (
let res = ref [] in
let tc (te, we) =
match (rec_gentrans data te acc cont) with
| None -> ()
| Some tt -> res := (tt, opt_weight_of_opt_algexp we, Guard.empty)::!res
in
List.iter tc wtel;
match !res with
| [] -> None
| ttlist -> Some (Split ttlist)
)
(*** PRIORITE ****)
| TE_prio tel -> (
let rec doit = (
function
[] -> assert false
| [te] -> (
rec_gentrans data te acc cont
)
| te::tail -> (
let first = rec_gentrans data te acc cont in
let others = doit tail in
match (first, others) with
(None,None) -> None
| (Some f, None) -> Some f
| (None, Some o) -> Some o
| (Some f, Some o) -> Some
(Split [(f, Some huge_weight, Guard.empty) ;
(o, None, Guard.empty)])
)
) in doit tel
)
(*** 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 gnre en priorit les cas ``boucle'' *)
let goon = rec_gentrans data te acc rec_cont in
(* on considre 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 ****)
| TE_loopi (cpt,min,max,te,si) -> (
(* similaire la boucle sauf pour les poids et les effets
de bord :
goon -> interval_goon(pre cpt, min, max)
+ loop_incr_exp cpt
stop -> interal_stop(pre cpt, min, max)
+ loop_reset_exp cpt
*)
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
let goon = rec_gentrans data te acc rec_cont in
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) -> (
let gw = dynamic_weight_exp LutPredef.kw_interval_goon cpt [min; max] in
let ga = incr_loop_cpt cpt in
let sw = dynamic_weight_exp LutPredef.kw_interval_stop cpt [min; max] in
let sa = reset_loop_cpt cpt in
Some
(Split [(g, Some (W_exp gw), Guard.of_exp ga si) ;
(s, Some (W_exp sw), Guard.of_exp sa si)])
)
)
(*** BOUCLE moyenne ****)
| TE_loopa (cpt,av, ecopt,te,si) -> (
(* similaire la boucle sauf pour les poids :
goon -> loopa_goon(pre cpt, min, max)
stop -> loopa_stop(pre cpt, min, max)
*)
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
let goon = rec_gentrans data te acc rec_cont in
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) -> (
let ec = match ecopt with
Some x -> x
| None -> CoAlgExp.of_iconst "0"
in
let gw = dynamic_weight_exp LutPredef.kw_average_goon cpt [av; ec] in
let ga = incr_loop_cpt cpt in
let sw = dynamic_weight_exp LutPredef.kw_average_stop cpt [av; ec] in
let sa = reset_loop_cpt cpt in
Some
(Split [(g, Some (W_exp gw), Guard.of_exp ga si) ;
(s, Some (W_exp sw), Guard.of_exp sa si)])
)
)
(** Assert
*)
| TE_assert (a, te, si) -> (
let rec_cont =
function
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, TE_assert (a,n,si))))
| _ -> cont (Some c)
)
in
(* HERE: CONTINUE EVEN IF IT IS UNSAT *)