Commit f570cc25 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.55 Wed, 03 Apr 2002 14:41:43 +0200 by jahier

Parent-Version:      0.54
Version-Log:

Allow equalities between formula by translating [A = B] into
[Or(And(A,B), And(Not(A), Not(B)))].

Fix a bug where lurette had a bad behaviour whenever a toss
was performed on a domain which size was bigger than max_int
or max_float.

Fix a bug where lurette was not handling env with both boolean and
numerical as output vars.  Also add a few comments in solver.ml along
the way.
Adds a local bool as an output of heater in order to test the fix
above.

Project-Description: Lurette
parent f0aff2da
......@@ -6,11 +6,11 @@
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 9471 1017750312 51_env_state. 1.16)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(source/util.ml 11251 1017335442 35_util.ml 1.16)
(source/util.ml 11635 1017837703 35_util.ml 1.17)
(source/wtree.ml 8518 1016011748 b/1_wtree.ml 1.9)
(source/solver.ml 23024 1017750312 39_solver.ml 1.20)
(source/solver.ml 24560 1017837703 39_solver.ml 1.21)
(source/command_line.ml 4234 1017396284 b/20_command_li 1.5)
(source/lurette.ml 11288 1017750312 12_lurette.ml 1.32)
(source/lurette.ml 11389 1017837703 12_lurette.ml 1.33)
(source/solver.mli 1135 1016803757 38_solver.mli 1.10)
(source/env.mli 2593 1017396284 15_env.mli 1.11)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
......@@ -21,7 +21,7 @@
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 925 1017156165 b/17_passerelle 1.4)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 10794 1017335442 b/27_rnumsolver 1.5)
(source/rnumsolver.ml 10783 1017837703 b/27_rnumsolver 1.6)
(source/parse_env.mli 907 1016127950 40_parse_env. 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
......@@ -29,12 +29,12 @@
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7749 1016803757 49_eval.ml 1.12)
(source/gen_stubs.ml 35425 1017335442 24_generate_l 1.21)
(source/parse_env.ml 15579 1017247563 41_parse_env. 1.13)
(source/parse_env.ml 16114 1017837703 41_parse_env. 1.14)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2663 1016803757 b/24_sim2chro.m 1.6)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 3354 1016803757 44_formula.ml 1.9)
(source/formula.mli 3402 1017837703 44_formula.ml 1.10)
(TAGS 9825 1007379917 21_TAGS 1.6)
(test/Makefile_ima_exe 1625 1017750312 b/35_Makefile_i 1.3)
(source/command_line.mli 1384 1017396284 b/21_command_li 1.5)
......@@ -58,11 +58,11 @@
(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
(source/gne.ml 8204 1016803757 b/37_gne.ml 1.1)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1839 1017750312 18_Makefile 1.26)
(Makefile 1835 1017837703 18_Makefile 1.27)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 789 1016803757 46_print.mli 1.8)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
(test/heater_int.rif.exp 785 1015408234 b/28_heater_int 1.1)
(test/heater_int.rif.exp 858 1017837703 b/28_heater_int 1.2)
(source/formula.ml 6652 1016803757 45_formula.ml 1.11)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 6298 1016803757 47_print.ml 1.13)
......
......@@ -2,8 +2,8 @@ LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# OCAMLFLAGS = -noassert -unsafe
# OCAMLNCFLAGS = -inline 10
OCAMLFLAGS = -noassert -unsafe
OCAMLNCFLAGS = -inline 10
-include ./lurette.in
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 54)
(Parent-Version lurette 0 53)
(Project-Version lurette 0 55)
(Parent-Version lurette 0 54)
(Version-Log "
Cosmetic change:
Encapsulates the various fields of Env_state.
Allow equalities between formula by translating [A = B] into
[Or(And(A,B), And(Not(A), Not(B)))].
Fix a bug where lurette had a bad behaviour whenever a toss
was performed on a domain which size was bigger than max_int
or max_float.
Fix a bug where lurette was not handling env with both boolean and
numerical as output vars. Also add a few comments in solver.ml along
the way.
Adds a local bool as an output of heater in order to test the fix
above.
")
(New-Version-Log "")
(Checkin-Time "Tue, 02 Apr 2002 14:25:12 +0200")
(Checkin-Time "Wed, 03 Apr 2002 14:41:43 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -30,7 +37,7 @@ Encapsulates the various fields of Env_state.
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.32 644))
(source/lurette.ml (lurette/12_lurette.ml 1.33 644))
(source/command_line.ml (lurette/b/20_command_li 1.5 644))
(source/command_line.mli (lurette/b/21_command_li 1.5 644))
......@@ -42,21 +49,21 @@ Encapsulates the various fields of Env_state.
(source/env.mli (lurette/15_env.mli 1.11 644))
(source/env.ml (lurette/16_env.ml 1.23 644))
(source/util.ml (lurette/35_util.ml 1.16 644))
(source/util.ml (lurette/35_util.ml 1.17 644))
(source/solver.mli (lurette/38_solver.mli 1.10 644))
(source/solver.ml (lurette/39_solver.ml 1.20 644))
(source/solver.ml (lurette/39_solver.ml 1.21 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.5 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
(source/parse_env.mli (lurette/40_parse_env. 1.6 644))
(source/parse_env.ml (lurette/41_parse_env. 1.13 644))
(source/parse_env.ml (lurette/41_parse_env. 1.14 644))
(source/show_env.mli (lurette/42_show_env.m 1.5 644))
(source/show_env.ml (lurette/43_show_env.m 1.4 644))
(source/formula.mli (lurette/44_formula.ml 1.9 644))
(source/formula.mli (lurette/44_formula.ml 1.10 644))
(source/formula.ml (lurette/45_formula.ml 1.11 644))
(source/print.mli (lurette/46_print.mli 1.8 644))
......@@ -78,7 +85,7 @@ Encapsulates the various fields of Env_state.
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.25 644))
(Makefile (lurette/18_Makefile 1.26 644))
(Makefile (lurette/18_Makefile 1.27 644))
(interface/Makefile (lurette/25_Makefile 1.6 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.3 644))
(make_lurette (lurette/27_make_luret 1.8 744))
......@@ -115,7 +122,7 @@ Encapsulates the various fields of Env_state.
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.2 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.4 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.2 644))
......
......@@ -14,13 +14,13 @@
type expr =
| Sum of expr * expr
| Diff of expr * expr
| Prod of expr * expr
| Quot of expr * expr
| Mod of expr * expr
| Sum of expr * expr (** + *)
| Diff of expr * expr (** - *)
| Prod of expr * expr (** * *)
| Quot of expr * expr (** / *)
| Mod of expr * expr (** modulo *)
| Ival of int
| Ival of int
| Fval of float
| Ivar of string
| Fvar of string
......
......@@ -224,6 +224,9 @@ and
local_var_name_and_type_list
rif options.display_local_var;
(* Initializing Dd's libs. *)
(* Manager.disable_autodyn (Env_state.bdd_manager ()); *)
(* Initializing the solution number table *)
Env_state.set_sol_number
(Bdd.dtrue (Env_state.bdd_manager ())) (Util.one_sol, Util.zero_sol);
......
......@@ -160,8 +160,10 @@ and (parse_var: aut_token -> vnt) =
->
( match typ with
"bool" -> (var, BoolT)
| "float" -> (var, FloatT(-.max_float, max_float))
| "int" -> (var, IntT(min_int, max_int))
| "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
| "int" -> (var, IntT(min_int / 2, max_int / 2))
(* We divide by 2 so that domains are always smaller
than max_int resp max_float *)
| str -> failwith ("*** Bad type in .env: " ^ str )
)
with e ->
......@@ -196,8 +198,8 @@ and (parse_type: string -> string -> aut_token -> vnt) =
[< 'Genlex.Kwd ")" >] ->
( match typ with
"bool" -> (var, BoolT)
| "float" -> (var, FloatT(-.max_float, max_float))
| "int" -> (var, IntT(min_int, max_int))
| "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
| "int" -> (var, IntT(min_int / 2, max_int / 2))
| str -> failwith ("*** Bad type in .env: " ^ str )
)
| [< 'Genlex.Kwd ","; vnt = parse_type_more var typ >] -> vnt
......@@ -250,8 +252,8 @@ and (parse_prevar: aut_token -> vnt) =
let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
( match typ with
"bool" -> (pre_var, BoolT)
| "float" -> (pre_var, FloatT(-.max_float, max_float))
| "int" -> (pre_var, IntT(min_int, max_int))
| "float" -> (pre_var, FloatT(-.max_float /. 2., max_float /. 2.))
| "int" -> (pre_var, IntT(min_int / 2, max_int / 2))
| str -> failwith ("*** Bad type in .env: " ^ str )
)
with e ->
......@@ -341,23 +343,34 @@ and (parse_expr_or_bool_ident: string -> vnt list -> aut_token -> formula) =
fun id vars tok ->
let tok_list = Stream.npeek 10 tok in
let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
let var =
let some_var =
match vt with
BoolT -> Ivar("XXX")
| IntT(_,_) -> Ivar(id)
| FloatT(_,_) -> Fvar(id)
BoolT -> None
| IntT(_,_) -> Some(Ivar(id))
| FloatT(_,_) -> Some(Fvar(id))
in
try
match tok with parser
[< 'Genlex.Kwd "="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> Eq(var, e2)
| [< 'Genlex.Kwd ">"; pl = parse_pragma_list ; e2 = parse_expr vars >] -> Sup(var, e2)
| [< 'Genlex.Kwd ">="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> SupEq(var, e2)
| [< 'Genlex.Kwd "<"; pl = parse_pragma_list ; e2 = parse_expr vars >] -> Inf(var, e2)
| [< 'Genlex.Kwd "<="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> InfEq(var, e2)
| [< f = parse_more_formula (Bvar(id)) vars >] -> f
with e ->
print_err_msg tok_list "parse_expr_or_bool_ident" ;
raise e
( match some_var with
None ->
( try
match tok with parser
[< f = parse_more_formula (Bvar(id)) vars >] -> f
with e ->
print_err_msg tok_list "parse_expr_or_bool_ident" ;
raise e
)
| Some(var) ->
( try
match tok with parser
[< 'Genlex.Kwd "="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> Eq(var, e2)
| [< 'Genlex.Kwd ">"; pl = parse_pragma_list ; e2 = parse_expr vars >] -> Sup(var, e2)
| [< 'Genlex.Kwd ">="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> SupEq(var, e2)
| [< 'Genlex.Kwd "<"; pl = parse_pragma_list ; e2 = parse_expr vars >] -> Inf(var, e2)
| [< 'Genlex.Kwd "<="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> InfEq(var, e2)
with e ->
print_err_msg tok_list "parse_expr_or_bool_ident" ;
raise e
)
)
and (parse_more_formula: formula -> vnt list -> aut_token -> formula) =
fun f1 vars tok ->
......@@ -368,6 +381,8 @@ and (parse_more_formula: formula -> vnt list -> aut_token -> formula) =
f2 = parse_formula vars >] -> Or(f1, f2)
| [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ;
f2 = parse_formula vars >] -> And(f1, f2)
| [< 'Genlex.Kwd "="; pl = parse_pragma_list ;
f2 = parse_formula vars >] -> Or(And(f1, f2), And(Not(f1), Not(f2)))
| [< >] -> f1
with e ->
print_err_msg tok_list "parse_more_formula" ;
......
......@@ -361,9 +361,9 @@ let (draw_inside : store -> Formula.subst list) =
( match range with
ValI(i) ->
((vn, N(I(i)))::acc)
| RangeI(min, max) ->
let n = max - min + 1 in
let ran = Random.int n in
| RangeI(min, max) ->
let ran = Random.int (max - min + 1)
in
((vn, N(I(min + ran)))::acc)
| ValF(f) ->
......
......@@ -475,25 +475,22 @@ type var = int
appear in the bdds we manipulate.
*)
let rec (count_missing_vars: Bdd.t -> var -> int -> Bdd.t * int) =
fun comb var cpt ->
(* Returns [cpt] + the number of variables occurring in [comb]
before reaching [var] ([var] excluded). Also returns the comb
which topvar is [var]. *)
let _ = assert (not (Bdd.is_cst comb)) in
let combvar = Bdd.topvar comb in
if var = combvar
then (comb, cpt)
else count_missing_vars (Bdd.dthen comb) var (cpt+1)
let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
fun bdd comb ->
(** Returns the relative (to which bbd points to it) number of
solutions of [bdd] and the one of its negation. Also udpates
the solution number table for [bdd] and its negation, and
recursively for all its sub-bdds.
the solution number table for [bdd] and its negation, and
recursively for all its sub-bdds.
[comb] is a positive cube that ougth to contain the indexes of
boolean vars that are still to be generated, and the numerical
indexes that appears in [bdd].
*)
let _ = assert (not (Bdd.is_cst bdd)
&& (Bdd.topvar comb) = (Bdd.topvar bdd))
in
let bdd_not = (Bdd.dnot bdd) in
let (sol_nb, sol_nb_not) =
try
......@@ -501,8 +498,7 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
and (not_nt, not_ne) = Env_state.sol_number bdd_not in
(* solutions numbers in the table are absolute *)
((add_sol_nb nt ne), (add_sol_nb not_nt not_ne))
with Not_found ->
let _ = assert (not (Bdd.is_cst bdd)) in
with Not_found ->
let (nt, not_nt) = compute_absolute_sol_nb (Bdd.dthen bdd) comb in
let (ne, not_ne) = compute_absolute_sol_nb (Bdd.delse bdd) comb in
Env_state.set_sol_number bdd (nt, ne) ;
......@@ -513,13 +509,22 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
and
(compute_absolute_sol_nb: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
fun sub_bdd comb ->
(* returns the absolute number of solutions of [sub_bdd] (and its
(* Returns the absolute number of solutions of [sub_bdd] (and its
negation) w.r.t. [comb], where [comb] is the comb of the
father of [sub_bdd]. *)
father of [sub_bdd].
The [comb] is used to know which output boolean variables are
unconstraint along a path in the bdd. Indeed, the comb is made
of all the boolean output var indexes plus the num contraints
indexes that appears in the bdd; hence, if the topvar of the
bdd is different from the topvar of the comb, it means that
the topvar of the comb is unsconstraint and we need to
multiply the number of solution of the branch by 2.
*)
if Bdd.is_cst sub_bdd
then
then
let sol_nb =
if Bdd.is_true comb (* iff no bool are to be gen *)
if Bdd.is_true comb
then one_sol
else (two_power_of (List.length (Bdd.list_of_support (Bdd.dthen comb))))
in
......@@ -528,10 +533,20 @@ and
else (zero_sol, sol_nb)
else
let topvar = Bdd.topvar sub_bdd in
let rec
(count_missing_vars: Bdd.t -> var -> int -> Bdd.t * int) =
fun comb var cpt ->
(* Returns [cpt] + the number of variables occurring in [comb]
before reaching [var] ([var] excluded). Also returns the comb
whch topvar is [var]. *)
let _ = assert (not (Bdd.is_cst comb)) in
let combvar = Bdd.topvar comb in
if var = combvar
then (comb, cpt)
else count_missing_vars (Bdd.dthen comb) var (cpt+1)
in
let (sub_comb, missing_vars_nb) =
if Bdd.is_true comb (* iff no bool are to be gen *)
then (comb, 0)
else count_missing_vars (Bdd.dthen comb) topvar 0
count_missing_vars (Bdd.dthen comb) topvar 0
in
let (n0, not_n0) = build_sol_nb_table sub_bdd sub_comb in
let factor = (two_power_of missing_vars_nb) in
......@@ -542,24 +557,26 @@ and
(****************************************************************************)
let (toss_up_one_var: var -> subst) =
let (toss_up_one_var: var -> subst option) =
fun var ->
(* [var] is a index that ougth to correspond to a boolean
variable. This fonction performs a toss and returns a
substitution for the corresponding boolean variable. *)
(* if [var] is a index that corresponds to a boolean variable,
this fonction performs a toss and returns a substitution for
the corresponding boolean variable. It returns [None]
otherwise.
Indeed, if it happens that a numerical constraint does not
appear along a path, we simply ignore it and hence it will not
be added to the store.
*)
let af = Env_state.index_to_atomic_formula var in
let vn = (
match af with
Bv(vn0) -> vn0
| _ ->
(* Only bool index ougth to appear in the comb. *)
assert false
) in
let ran = Random.float 1. in
if (ran < 0.5)
then (vn, Formula.B(true))
else (vn, Formula.B(false))
Bv(vn) ->
let ran = Random.float 1. in
if (ran < 0.5)
then Some(vn, Formula.B(true))
else Some(vn, Formula.B(false))
| _ -> None
let (is_a_numeric_constraint : atomic_formula -> bool) =
fun af ->
......@@ -593,11 +610,14 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t ->
let af = (Env_state.index_to_atomic_formula bddvar) in
let top_var_is_numeric = is_a_numeric_constraint af in
if
not(Bdd.is_true comb) && (* iff no bool are to be gen *)
bddvar <> (Bdd.topvar comb) &&
not top_var_is_numeric
then
let new_sl = (toss_up_one_var (Bdd.topvar comb))::sl in
let new_sl =
match toss_up_one_var (Bdd.topvar comb) with
Some(s) -> s::sl
| None -> sl
in
draw_in_bdd (new_sl, store) bdd (Bdd.dthen comb)
else
(* bddvar = combvar xor top_var_is_numeric *)
......@@ -659,7 +679,7 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t ->
(* Toss the remaining bool vars. *)
( (List.append
sl1
(map toss_up_one_var (Bdd.list_of_support new_comb))),
(Util.list_map_option toss_up_one_var (Bdd.list_of_support new_comb))),
store1
)
else
......@@ -685,7 +705,7 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t ->
then
( (List.append
sl2
(List.map toss_up_one_var
(Util.list_map_option toss_up_one_var
(Bdd.list_of_support new_comb))),
store2
)
......@@ -727,6 +747,7 @@ let (solve_formula: env_in -> int -> formula list -> vn list -> vnt list ->
fun input p fl bool_vars_to_gen num_vars_to_gen ->
let f = formula_list_to_conj fl in
let bdd =
(* The bdd of f has necessarily been computed (by is_satisfiable) *)
try Env_state.bdd f
with Not_found -> Env_state.bdd_global f
in
......@@ -736,19 +757,34 @@ let (solve_formula: env_in -> int -> formula list -> vn list -> vnt list ->
True
bool_vars_to_gen
in
let (comb, _) = formula_to_bdd input bool_vars_to_gen_f in
let (comb0, _) = formula_to_bdd input bool_vars_to_gen_f in
let comb =
(* All boolean vars should appear in the comb so that when we
find that such a var is missing along a bdd path, we can
perform a (fair) toss for it. On the contrary, if a
numerical contraint disappear from a bdd (eg, consider [(f
&& false) || true]), it is not important; fairly tossing a
(boolean) value for a num constaint [nc] and performing a
fair toss in the resulting domain is equivalent to directly
perform the toss in the (unconstraint wrt [nc]) initial
domain.
*)
Bdd.dand (Bdd.support bdd) comb0
in
let _ =
if not (Env_state.sol_number_exists bdd)
then
let rec skip_var comb v =
if Bdd.is_true comb (* iff no bool are to be gen *)
then comb
let rec skip_unconstraint_bool_var_at_top comb v =
(* [build_sol_nb_table] supposes that the bdd and its comb
have the same top var.
*)
if Bdd.is_true comb then comb
else
let topvar = (Bdd.topvar comb) in
if v = topvar then comb else skip_var (Bdd.dthen comb) v
if v = topvar then comb
else skip_unconstraint_bool_var_at_top (Bdd.dthen comb) v
in
let comb2 = skip_var comb (Bdd.topvar bdd) in
let comb2 = skip_unconstraint_bool_var_at_top comb (Bdd.topvar bdd) in
let _ = build_sol_nb_table bdd comb2 in
()
in
......
......@@ -129,6 +129,20 @@ let rec list_fold_left3 f accu l1 l2 l3 =
| (_, _, _) -> invalid_arg "Util.list_fold_left3"
(** A special kind of map that applies a function that outputs an
[option] value, and which only returns a list containing only
success values. *)
let rec (list_map_option: ('a -> 'b option) -> 'a list -> 'b list) =
fun f l ->
match l with
[] -> []
| e::t ->
( match f e with
None -> (list_map_option f t)
| Some(b) -> b::(list_map_option f t)
)
let rec (list_map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list
-> 'c list -> 'd list) =
fun f l1 l2 l3 ->
......
......@@ -5,64 +5,65 @@ U:int
#@outputs
Heat_on:bool
Dudt:int
Toto:bool
@#
#step 1
17 #outs 0
17 #outs 0 t
#step 2
17 #outs t 0
17 #outs t 1 t
#step 3
17 #outs t 0
18 #outs t 1 t
#step 4
17 #outs t 2
19 #outs t 0 t
#step 5
19 #outs t 2
19 #outs t 0 t
#step 6
21 #outs t 2
19 #outs t 0 t
#step 7
23 #outs f -2
19 #outs t 1 t
#step 8
21 #outs f -5
20 #outs t 1 t
#step 9
16 #outs f 0
21 #outs t 2 t
#step 10
16 #outs f -1
23 #outs f -3 f
#step 11
15 #outs f -2
20 #outs f -1 f
#step 12
13 #outs f -5
19 #outs f -2 f
#step 13
8 #outs t 1
17 #outs f -4 f
#step 14
9 #outs t 2
13 #outs f -1 f
#step 15
11 #outs t 1
12 #outs t 2 t
#step 16
12 #outs t 2
14 #outs t 0 t
#step 17
14 #outs t 2
14 #outs t 0 t
#step 18
16 #outs t 2
14 #outs t 0 t
#step 19
18 #outs t 0
14 #outs t 2 t
#step 20
18 #outs t 2
16 #outs t 1 t
#step 21
20 #outs t 1
17 #outs t 0 t
#step 22
21 #outs t 1
17 #outs t 0 t
#step 23
22 #outs f -3
17 #outs t 1 t
#step 24
19 #outs f -1
18 #outs t 1 t
#step 25
18 #outs f -3
19 #outs t 2 t
#step 26
15 #outs f -3
21 #outs t 0 t
#step 27
12 #outs f -4
21 #outs f 0 f
#step 28
8 #outs t 0
21 #outs f -4 f
#step 29
8 #outs t 0
17 #outs f -2 f
#step 30
8 #outs t 0
15 #outs f -1 f