Commit 561ba995 authored by Pascal Raymond's avatar Pascal Raymond
Browse files

AutoExplore with partial eval no longer used,

in order to avoid strange "assert" behavior.
Simu is based on standard AutoGen, thus
the behavior is the same with simu and compiled luc.
Warning: the experience of AutoExplore raised
important problems between Lutin and Lucky semantics:
should be fixed in a later version !
parent be3171fe
......@@ -4,20 +4,20 @@
# step 0
10 0 20.000000 #outs 6 0 16.278233
# step 1
10 0 20.000000 #outs 11 1 16.610070
10 0 20.000000 #outs 6 1 21.603283
# step 2
10 0 20.000000 #outs 9 1 17.399245
# step 3
10 0 20.000000 #outs 9 1 24.170976
10 0 20.000000 #outs 13 1 19.172617
# step 4
10 0 20.000000 #outs 8 0 24.249699
10 0 20.000000 #outs 11 0 19.251183
# step 5
10 0 20.000000 #outs 8 1 15.253516
# step 6
10 0 20.000000 #outs 14 0 16.432561
10 0 20.000000 #outs 7 0 21.425417
# step 7
10 0 20.000000 #outs 9 1 17.336461
# step 8
10 0 20.000000 #outs 7 0 19.618259
# step 9
10 0 20.000000 #outs 7 0 21.008662
10 0 20.000000 #outs 14 0 16.016641
# Interpreting the lutin file foo.lut with node main
-1 true 7.188031
3 true 5.883434
2 true 9.917567
1 true 13.888125
0 true 18.693193
4 true 19.679989
6 true 17.278568
5 true 18.418950
4 true 14.450737
7 true 13.272541
11 true 15.191055
-2 true 10.880835
0 true 9.916883
1 true 8.889484
3 true 8.694923
7 true 9.681718
3 true 12.275496
6 true 8.423593
5 true 4.455379
2 true 8.274838
6 true 10.193351
......@@ -3,200 +3,200 @@
#step 1
0 T 0.00 #outs 0 T 1.27
#step 2
0 F 1.27 #outs 1 T -2.12
0 F 1.27 #outs -4 T 2.87
#step 3
1 F -2.12 #outs 0 T -4.72
-4 F 2.87 #outs -5 T 0.27
#step 4
0 F -4.72 #outs -1 T -0.55
-5 F 0.27 #outs -2 T -0.55
#step 5
-1 F -0.55 #outs -3 F 3.70
-2 F -0.55 #outs -1 F -1.30
#step 6
-3 T 3.70 #outs -5 T -1.05
-1 T -1.30 #outs -3 T -6.05
#step 7
-5 F -1.05 #outs -1 F -4.61
-3 F -6.05 #outs -6 F -4.62
#step 8
-1 T -4.61 #outs -2 T -2.28
-6 T -4.62 #outs -2 T -7.29
#step 9
-2 F -2.28 #outs -5 F -2.66
-2 F -7.29 #outs -5 F -7.67
#step 10
-5 T -2.66 #outs -8 T -1.66
-5 T -7.67 #outs -1 T -11.65
#step 11
-8 F -1.66 #outs -8 F 2.78
-1 F -11.65 #outs -1 F -7.22
#step 12
-8 T 2.78 #outs -5 T -0.86
-1 T -7.22 #outs -2 T -5.87
#step 13
-5 F -0.86 #outs -1 F -2.89
-2 F -5.87 #outs -6 F -2.90
#step 14
-1 T -2.89 #outs -3 T -7.08
-6 T -2.90 #outs -8 T -7.09
#step 15
-3 F -7.08 #outs 0 T -8.42
-8 F -7.09 #outs -12 T -3.44
#step 16
0 F -8.42 #outs 1 F -4.85
-12 F -3.44 #outs -11 F 0.14
#step 17
1 T -4.85 #outs 1 T -0.98
-11 T 0.14 #outs -11 T 4.01
#step 18
1 F -0.98 #outs 5 T -3.74
-11 F 4.01 #outs -15 T 6.24
#step 19
5 F -3.74 #outs 9 F -4.43
-15 F 6.24 #outs -19 F 10.55
#step 20
9 T -4.43 #outs 13 T -3.79
-19 T 10.55 #outs -15 T 11.19
#step 21
13 F -3.79 #outs 12 F -5.03
-15 F 11.19 #outs -16 F 9.95
#step 22
12 T -5.03 #outs 10 T -7.79
-16 T 9.95 #outs -18 T 7.19
#step 23
10 F -7.79 #outs 9 T -10.65
-18 F 7.19 #outs -19 T 4.33
#step 24
9 F -10.65 #outs 12 T -13.68
-19 F 4.33 #outs -20 T 6.30
#step 25
12 F -13.68 #outs 9 T -12.10
-20 F 6.30 #outs -16 T 2.88
#step 26
9 F -12.10 #outs 10 F -9.94
-16 F 2.88 #outs -15 F 5.04
#step 27
10 T -9.94 #outs 10 T -7.67
-15 T 5.04 #outs -15 T 7.31
#step 28
10 F -7.67 #outs 9 F -11.84
-15 F 7.31 #outs -16 F 3.14
#step 29
9 T -11.84 #outs 5 T -14.50
-16 T 3.14 #outs -20 T 0.48
#step 30
5 F -14.50 #outs 4 F -10.07
-20 F 0.48 #outs -19 F -0.09
#step 31
4 T -10.07 #outs 6 T -10.40
-19 T -0.09 #outs -21 T 4.59
#step 32
6 F -10.40 #outs 7 T -9.11
-21 F 4.59 #outs -20 T 5.88
#step 33
7 F -9.11 #outs 7 F -6.87
-20 F 5.88 #outs -20 F 8.11
#step 34
7 T -6.87 #outs 8 T -3.98
-20 T 8.11 #outs -19 T 11.00
#step 35
8 F -3.98 #outs 4 T -2.70
-19 F 11.00 #outs -18 T 7.29
#step 36
4 F -2.70 #outs 0 F -6.68
-18 F 7.29 #outs -22 F 3.31
#step 37
0 T -6.68 #outs 0 T -6.72
-22 T 3.31 #outs -23 T 8.27
#step 38
0 F -6.72 #outs -4 F -7.67
-23 F 8.27 #outs -27 F 7.32
#step 39
-4 T -7.67 #outs -4 T -9.99
-27 T 7.32 #outs -31 T 9.99
#step 40
-4 F -9.99 #outs -1 T -5.19
-31 F 9.99 #outs -28 T 14.79
#step 41
-1 F -5.19 #outs -1 T -6.49
-28 F 14.79 #outs -29 T 18.49
#step 42
-1 F -6.49 #outs -4 F -11.10
-29 F 18.49 #outs -32 F 13.89
#step 43
-4 T -11.10 #outs -3 T -11.58
-32 T 13.89 #outs -33 T 18.40
#step 44
-3 F -11.58 #outs -3 F -10.70
-33 F 18.40 #outs -33 F 19.28
#step 45
-3 T -10.70 #outs -3 T -7.70
-33 T 19.28 #outs -33 T 22.28
#step 46
-3 F -7.70 #outs 0 T -4.88
-33 F 22.28 #outs -30 T 25.10
#step 47
0 F -4.88 #outs 2 F -3.26
-30 F 25.10 #outs -28 F 26.73
#step 48
2 T -3.26 #outs 2 T -8.22
-28 T 26.73 #outs -29 T 26.75
#step 49
2 F -8.22 #outs 1 T -12.89
-29 F 26.75 #outs -30 T 22.08
#step 50
1 F -12.89 #outs 2 F -10.64
-30 F 22.08 #outs -29 F 24.34
#step 51
2 T -10.64 #outs 1 T -7.71
-29 T 24.34 #outs -26 T 22.27
#step 52
1 F -7.71 #outs 1 F -11.70
-26 F 22.27 #outs -30 F 23.27
#step 53
1 T -11.70 #outs 2 T -14.75
-30 T 23.27 #outs -34 T 25.21
#step 54
2 F -14.75 #outs 6 F -12.82
-34 F 25.21 #outs -30 F 27.14
#step 55
6 T -12.82 #outs 7 T -15.57
-30 T 27.14 #outs -33 T 29.39
#step 56
7 F -15.57 #outs 3 T -15.38
-33 F 29.39 #outs -30 T 24.58
#step 57
3 F -15.38 #outs 4 F -13.74
-30 F 24.58 #outs -29 F 26.22
#step 58
4 T -13.74 #outs 4 T -13.24
-29 T 26.22 #outs -29 T 26.73
#step 59
4 F -13.24 #outs 2 T -17.97
-29 F 26.73 #outs -31 T 22.00
#step 60
2 F -17.97 #outs 5 T -22.23
-31 F 22.00 #outs -35 T 22.73
#step 61
5 F -22.23 #outs 8 F -17.72
-35 F 22.73 #outs -32 F 27.24
#step 62
8 T -17.72 #outs 11 T -13.86
-32 T 27.24 #outs -29 T 31.10
#step 63
11 F -13.86 #outs 10 F -16.10
-29 F 31.10 #outs -30 F 28.86
#step 64
10 T -16.10 #outs 9 T -20.98
-30 T 28.86 #outs -31 T 23.98
#step 65
9 F -20.98 #outs 9 T -22.55
-31 F 23.98 #outs -32 T 27.40
#step 66
9 F -22.55 #outs 9 F -27.08
-32 F 27.40 #outs -36 F 27.87
#step 67
9 T -27.08 #outs 9 T -23.30
-36 T 27.87 #outs -36 T 31.65
#step 68
9 F -23.30 #outs 13 F -25.13
-36 F 31.65 #outs -40 F 34.81
#step 69
13 T -25.13 #outs 10 T -27.95
-40 T 34.81 #outs -43 T 31.99
#step 70
10 F -27.95 #outs 8 F -25.86
-43 F 31.99 #outs -40 F 29.09
#step 71
8 T -25.86 #outs 12 T -29.50
-40 T 29.09 #outs -42 T 30.44
#step 72
12 F -29.50 #outs 8 F -34.35
-42 F 30.44 #outs -46 F 25.59
#step 73
8 T -34.35 #outs 9 T -36.19
-46 T 25.59 #outs -50 T 28.74
#step 74
9 F -36.19 #outs 10 F -34.81
-50 F 28.74 #outs -49 F 30.13
#step 75
10 T -34.81 #outs 8 T -39.05
-49 T 30.13 #outs -51 T 25.89
#step 76
8 F -39.05 #outs 10 F -38.23
-51 F 25.89 #outs -49 F 26.71
#step 77
10 T -38.23 #outs 7 T -35.09
-49 T 26.71 #outs -49 T 24.85
#step 78
7 F -35.09 #outs 4 F -38.52
-49 F 24.85 #outs -52 F 21.42
#step 79
4 T -38.52 #outs 5 T -42.89
-52 T 21.42 #outs -56 T 22.05
#step 80
5 F -42.89 #outs 9 F -43.37
-56 F 22.05 #outs -59 F 26.56
#step 81
9 T -43.37 #outs 12 T -42.99
-59 T 26.56 #outs -56 T 26.94
#step 82
12 F -42.99 #outs 14 T -38.75
-56 F 26.94 #outs -54 T 31.18
#step 83
14 F -38.75 #outs 14 T -34.38
-54 F 31.18 #outs -54 T 35.55
#step 84
14 F -34.38 #outs 13 F -35.70
-54 F 35.55 #outs -55 F 34.23
#step 85
13 T -35.70 #outs 10 T -36.79
-55 T 34.23 #outs -58 T 33.14
#step 86
10 F -36.79 #outs 6 F -35.22
-58 F 33.14 #outs -58 F 29.72
#step 87
6 T -35.22 #outs 10 T -39.45
-58 T 29.72 #outs -60 T 30.48
#step 88
10 F -39.45 #outs 6 T -38.42
-60 F 30.48 #outs -58 T 26.51
#step 89
6 F -38.42 #outs 2 T -34.55
-58 F 26.51 #outs -57 T 25.39
#step 90
2 F -34.55 #outs 2 F -33.04
-57 F 25.39 #outs -57 F 26.90
#step 91
2 T -33.04 #outs 0 T -32.09
-57 T 26.90 #outs -55 T 22.86
#step 92
0 F -32.09 #outs -4 F -33.35
-55 F 22.86 #outs -59 F 21.60
#step 93
-4 T -33.35 #outs -4 T -33.56
-59 T 21.60 #outs -61 T 26.38
#step 94
-4 F -33.56 #outs 0 F -31.67
-61 F 26.38 #outs -57 F 28.28
#step 95
0 T -31.67 #outs -3 T -33.33
-57 T 28.28 #outs -60 T 26.62
#step 96
-3 F -33.33 #outs -3 T -35.25
-60 F 26.62 #outs -62 T 29.70
#step 97
-3 F -35.25 #outs 0 T -38.14
-62 F 29.70 #outs -63 T 31.80
#step 98
0 F -38.14 #outs 3 T -38.05
-63 F 31.80 #outs -60 T 31.89
#step 99
3 F -38.05 #outs 3 T -42.54
-60 F 31.89 #outs -64 T 32.38
#step 100
3 F -42.54 #outs -1 T -44.71
-64 F 32.38 #outs -68 T 30.22
......@@ -137,7 +137,7 @@ let init_control (it:t) = it.init_control
let transitions (it:t) = it.transitions
(* ADD/REPLACE pre values in data strore *)
let add_pres (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
match pctx with
| [] -> data
| _ -> (
......@@ -147,7 +147,7 @@ let add_pres (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
in
let addp accin (id, e) = (
let v = try (
Guard.value_of_algexp ctx e
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
......@@ -318,6 +318,9 @@ let gentrans
let id2trace s = (
(Hashtbl.find (Expand.trace_tab xenv) s).ti_def_exp
) in
let unalias s = (
(Hashtbl.find (Expand.alias_tab xenv) s).ai_def_exp
) in
(*-------------------------------------------*)
(* LA FONCTION RCURSIVE *)
......@@ -342,10 +345,10 @@ let gentrans
| TE_constraint ae -> (
(* HERE DO EVAL ! *)
try (
let new_acc = Guard.add ~context:data ae acc in
let new_acc = Guard.add ~unalias:unalias ~context:data ae acc in
(* ICI *)
(* cont (Some (Goto (Guard.of_exp ~context:data ae, TE_eps))) *)
(* cont (Some (Goto (Guard.of_exp ~unalias:unalias ~context:data ae, TE_eps))) *)
cont (Some (Goto (new_acc, TE_eps)))
) with Guard.Unsat -> (
......@@ -516,9 +519,9 @@ let gentrans
| _ -> cont (Some c)
)
) in
(* HERE: DO EVAL! *)
(* HERE: CONTINUE EVEN IF IT IS UNSAT *)
try (
let rec_acc = Guard.add ~context:data a acc in
let rec_acc = Guard.add ~unalias:unalias ~context:data a acc in
rec_gentrans data te rec_acc rec_cont
) with Guard.Unsat -> (
(* HERE: cont or not cont ???? *)
......@@ -530,7 +533,7 @@ let gentrans
recursive call with a new store
*)
| TE_init_pre (pctx, te) -> (
let new_data = add_pres data pctx in
let new_data = add_pres unalias data pctx in
rec_gentrans new_data te acc cont
)
(** RAISE
......@@ -651,7 +654,7 @@ let gentrans
)
)
) in try (
(* let tail_acc = Guard.merge ~context:data cl acc in *)
(* let tail_acc = Guard.merge ~unalias:unalias ~context:data cl acc in *)
rec_gentrans data (TE_para(el)) cl tail_cont
) with Guard.Unsat -> (
(* HERE: cont or not cont ???? *)
......
......@@ -33,7 +33,7 @@ open Predef ;;
open Expand ;;
let dbg = Verbose.get_flag "AutoExplore"
let dbg = Verbose.get_flag "AutoGen"
(** N.B. On utilise des AlgExp.t de type "CkTypeEff.weight" pour
représenter les poids dans les transitions *)
......@@ -78,6 +78,30 @@ type ttree =
| Goto of goto
| Split of (ttree * weightexp option * cond) list
let rec string_of_ttree topt = (
match topt with
None -> sprintf "%s" Predef.kw_deadlock
| Some t -> (
match t with
| Vanish -> "Vanish"
| Raise x -> sprintf "Raise %s" x
| Goto (c, ss) -> (
let cl = List.map CoAlgExp.lus_dumps (Guard.to_exp_list c) in
sprintf "Goto (%s, %s)" (String.concat " and " cl) (CoTraceExp.dumps ss)
)
| Split l -> (
let soc (t, wo, c) = (
let ws = match wo with
| Some W_huge -> "<INF>"
| None -> "< 1 >"
| Some _ -> "< ? >"
in
sprintf "%s : %s" ws (string_of_ttree (Some t))
) in
String.concat ";\n " (List.map soc l)
)
)
)
(* DATA CONTEXT managment (for simulation)
......@@ -85,6 +109,8 @@ NB used here ONLY for pre re-initialisation (cf. exist)
*)
type config = { data: Guard.store option; control: string }
let make_config state = { data = None; control = state }
(** STATE MANAGMENT *)
type state_info =
SS_stable of CoTraceExp.t
......@@ -134,7 +160,7 @@ let init_control (it:t) = it.init_control
let transitions (it:t) = it.transitions
(* ADD/REPLACE pre values in data strore *)
let add_pres (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
match pctx with
| [] -> data
| _ -> (
......@@ -144,7 +170,7 @@ let add_pres (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
in
let addp accin (id, e) = (
let v = try (
Guard.value_of_algexp ctx e
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
......@@ -243,8 +269,6 @@ let dump_ttree topt = (
printf "\n"
)
(****************************************************************************
TRACE -> TRANSITIONS BRANCHUES
-----------------------------------------------------------------------------
......@@ -303,6 +327,11 @@ type callback = ttree option -> ttree option
with partial evaluation of contraints
*)
let dump_cont str tt x = (
dump_ttree tt;
)
let gentrans
(xenv : Expand.t)
(data : Guard.store option) (* data env = inputs + pres *)
......@@ -315,6 +344,9 @@ let gentrans
let id2trace s = (
(Hashtbl.find (Expand.trace_tab xenv) s).ti_def_exp
) in
let unalias s = (
(Hashtbl.find (Expand.alias_tab xenv) s).ai_def_exp
) in
(*-------------------------------------------*)
(* LA FONCTION RÉCURSIVE *)
......@@ -325,7 +357,7 @@ let gentrans
(acc : cond)
(cont : callback)
= (
Verbose.put ~level:13 "rec_gentrans \"%s\"\n" (CoTraceExp.dumps x);
Verbose.put ~flag:dbg "++rec_gentrans \"%s\"\n" (CoTraceExp.dumps x);
match x with
(***** EPSILON => vanish ... *****)
| TE_eps -> (
......@@ -347,7 +379,9 @@ let gentrans
- vanish => te2
*)
| TE_fby (te1, te2) -> (
let rec_cont = ( function
let fby_cont a = (
Verbose.put ~flag:dbg "-- fby_cont (%s)\n in context %s\n" (string_of_ttree a) (CoTraceExp.dumps x);
match a with
| None -> None
| Some c -> (
match c with
......@@ -357,7 +391,7 @@ let gentrans
| _ -> cont (Some c)
)
) in
rec_gentrans data te1 acc rec_cont
rec_gentrans data te1 acc fby_cont
)
(**** CHOIX *****)
(* chaque choix est traité dans
......@@ -401,7 +435,9 @@ let gentrans
)
(*** BOUCLE "INFINIE" ***)
| TE_loop te -> (
let rec_cont = ( function
let loop_goon_cont a = (
Verbose.put ~flag:dbg "-- loop_goon_cont (%s)\n in context %s\n" (string_of_ttree a) (CoTraceExp.dumps x);
match a with
| None -> None
| Some c -> (
match c with
......@@ -412,9 +448,11 @@ let gentrans
)
) in
(* on génère en priorité les cas ``boucle'' *)
let goon = rec_gentrans data te acc rec_cont in
let goon = rec_gentrans data te acc loop_goon_cont in
Verbose.put ~flag:dbg "==== loop goon branch of %s\n gives: %s\n" (CoTraceExp.dumps x) (string_of_ttree goon);
(* on considère aussi le cas vanish *)
let stop = cont (Some Vanish) in
Verbose.put ~flag:dbg "==== loop stop branch of %s\n gives: %s\n" (CoTraceExp.dumps x) (string_of_ttree stop);
match (goon,stop) with
(None,None) -> None
| (Some g, None) -> Some g
......@@ -431,7 +469,9 @@ let gentrans
stop -> interal_stop(pre cpt, min, max)
+ loop_reset_exp cpt
*)
let rec_cont = ( function
let loopi_goon_cont a = (
Verbose.put ~flag:dbg "-- loopi_goon_cont (%s)\n in context %s\n" (string_of_ttree a) (CoTraceExp.dumps x);
match a with
| None -> None
| Some c -> (
match c with
......@@ -441,7 +481,7 @@ let gentrans
| _ -> cont (Some c)
)
) in
let goon = rec_gentrans data te acc rec_cont in
let goon = rec_gentrans data te acc loopi_goon_cont in
let stop = cont (Some Vanish) in
match (goon,stop) with
(None,None) -> None
......@@ -462,7 +502,9 @@ let gentrans
goon -> loopa_goon(pre cpt, min, max)
stop -> loopa_stop(pre cpt, min, max)
*)
let rec_cont = ( function
let loopa_goon_cont a = (
Verbose.put ~flag:dbg "-- loopi_goon_cont (%s)\n in context %s\n" (string_of_ttree a) (CoTraceExp.dumps x);
match a with
| None -> None
| Some c -> (
match c with
......@@ -472,7 +514,7 @@ let gentrans
| _ -> cont (Some c)
)
) in
let goon = rec_gentrans data te acc rec_cont in
let goon = rec_gentrans data te acc loopa_goon_cont in
let stop = cont (Some Vanish) in
match (goon,stop) with
(None,None) -> None
......@@ -494,7 +536,9 @@ let gentrans
(** Assert
*)
| TE_assert (a, te) -> (
let rec_cont = ( function
let assert_cont act = (
Verbose.put ~flag:dbg "-- assert_cont (%s)\n in context %s\n" (string_of_ttree act) (CoTraceExp.dumps x);
match act with
| None -> None
| Some c -> (
match c with
......@@ -504,13 +548,13 @@ let gentrans
)
) in
let rec_acc = Guard.add ~context:data a acc in
rec_gentrans data te rec_acc rec_cont
rec_gentrans data te rec_acc assert_cont
)
(** init_pre
recursive call with a new store
*)