Commit 74e896bf authored by erwan's avatar erwan

Update: monadisation of Lutin, part 6

Rationale: make rdbg time traveling work.
parent 3cde6aa1
......@@ -318,8 +318,8 @@ TODO:
type solutions = (Var.env_out * Var.env_loc) list
type guard = {
g_form : Exp.formula;
mutable g_sol : solutions option;
mutable g_bdd : Bdd.t option;
g_sol : solutions option;
g_bdd : Bdd.t option;
g_src : CoIdent.src_stack list
}
......@@ -407,49 +407,48 @@ fun ins outs locs -> (
*)
(* reuse Solver.solve_formula, returns solutions *)
let find_some_sols
(it:t)
(tfdn: Thickness.formula_draw_nb)
(tn: Thickness.numeric)
(g : guard)
= match g.g_sol with
| Some s -> s
| None ->
let zesol,bdd = (
let solver_vl = ref 0 in
Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
let snt, is_bool_sat,bdd = Solver.is_satisfiable_bdd it.snt
let find_some_sols (it:t) (tfdn: Thickness.formula_draw_nb) (tn: Thickness.numeric)
(g : guard) : guard * solutions
= match g.g_sol with
| Some s -> g, s
| None ->
let zesol,bdd = (
let solver_vl = ref 0 in
Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
let snt, is_bool_sat,bdd = Solver.is_satisfiable_bdd it.snt
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl *)
(Verbose.level())
"LutExe.is_bool_sat" (* ctx_msg: string *)
g.g_form
"LutExe.is_bool_sat" (* msg: string (?) *)
in
if not is_bool_sat then (
[],bdd
) else (
let snt, sols = Solver.solve_formula snt
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl *)
(* !solver_vl (* vl: int *) *)
(Verbose.level())
"LutExe.is_bool_sat" (* ctx_msg: string *)
g.g_form
"LutExe.is_bool_sat" (* msg: string (?) *)
in
if not is_bool_sat then (
[],bdd
) else (
let snt, sols = Solver.solve_formula snt
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl (* vl: int *) *)
(Verbose.level())
"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.g_form (* f: formula *)
in
sols,bdd
)
) in (
g.g_sol <- Some zesol;
g.g_bdd <- Some bdd;
zesol
)
"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.g_form (* f: formula *)
in
sols,bdd
)
) in (
{ g with
g_sol = Some zesol;
g_bdd = Some bdd;
},
zesol
)
let find_one_sol it g =
......@@ -459,12 +458,12 @@ let find_one_sol it g =
| Lucky.StepVertices -> (0,0,Thickness.AtMost 1)
in
match find_some_sols it 1 thick g with
| s::_ -> s
| [] -> raise Not_found
| g, s::_ -> g, s
| _, [] -> raise Not_found
(* check_sat *)
let check_satisfiablity (it:t) (g: guard) = (
let check_satisfiablity (it:t) (g: guard) : guard * bool = (
try (
Verbose.exe ~flag:dbg
(fun () ->
......@@ -472,9 +471,9 @@ let check_satisfiablity (it:t) (g: guard) = (
"--check satisfiablility of \"%s\"\n"
(* (Exp.formula_to_string g.g_form); *)
(string_of_guard g));
let _ = find_one_sol it g in
true
) with Not_found -> false
let g,_ = find_one_sol it g in
g, true
) with Not_found -> g, false
)
let min_max_src (bl1,el1,bc1,ec1,bchar1,echar1) (bl2,el2,bc2,ec2,bchar2,echar2) =
......@@ -580,8 +579,9 @@ exception LocalDeadlock
(** Add a new constraint to an existing guard *)
let add_to_guard it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) = (
let res = add_to_guard_nc it data e acc si in
if (check_satisfiablity it res) then res
let res = add_to_guard_nc it data e acc si in
let res, ok = check_satisfiablity it res in
if ok then res
else raise LocalDeadlock
)
......@@ -1447,7 +1447,7 @@ and to_reactive_prg (it:t) (curstate:internal_state) (invals: Value.t list) = (
| Vanish -> raise Stop
| Goto (zeguard, ctrl') -> (
(* THIS IS THE NORMAL BEHAVIOR *)
let (outs, locs) = try
let zeguard, (outs, locs) = try
find_one_sol it zeguard
with Not_found -> assert false
in
......@@ -1544,7 +1544,7 @@ let rec (genpath_ldbg :
(if snd si = [] then acc.g_src else (snd si)::acc.g_src)
in
let try_cont ctx () =
let is_sat = check_satisfiablity it new_acc in
let new_acc, is_sat = check_satisfiablity it new_acc in
if (is_sat) then
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
......@@ -1575,7 +1575,7 @@ let rec (genpath_ldbg :
else (* the constraint is unsat *)
let lazy_ci = fun () ->
let cc = add_to_guard_nc it data ae empty_guard si in
ignore (check_satisfiablity it cc);
let cc,_ = (check_satisfiablity it cc) in
let bdd = match new_acc.g_bdd with None -> assert false
| Some bdd -> bdd in
let bdd_cc = match cc.g_bdd with None -> assert false
......@@ -2338,7 +2338,7 @@ and (to_reactive_prg_ldbg :
| Vanish -> fail_cont ctx2
| Goto (zeguard, ctrl') ->
(* THIS IS THE NORMAL BEHAVIOR *)
let (outs, locs) =
let zeguard, (outs, locs) =
try find_one_sol it zeguard with Not_found -> assert false
in
let pres' = make_pre ins outs locs in
......@@ -2496,7 +2496,7 @@ let (step: t -> control_state -> data_state -> control_state * data_state) =
| Goto (zeguard, ctrl) -> (
MainArg.event_incr prog.arg_opt; (* exit *)
(* THIS IS THE NORMAL BEHAVIOR *)
let (outs, locs) =
let zeguard, (outs, locs) =
try find_one_sol prog zeguard
with Not_found -> assert false
in
......@@ -2552,7 +2552,7 @@ let (step_ldbg: ctx -> string -> t -> control_state -> data_state ->
| Raise str -> failwith str
| Goto (zeguard, ctrl) -> (
(* THIS IS THE NORMAL BEHAVIOR *)
let (outs, locs) =
let zeguard, (outs, locs) =
try find_one_sol prog zeguard
with Not_found -> assert false
in
......
......@@ -77,9 +77,10 @@ val get_init_pres: t -> Value.OfIdent.t
val get_behavior_gen : t -> Var.env_in -> Var.env -> control_state -> (unit -> behavior_gen)
val find_some_sols : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard -> (Var.env_out * Var.env_loc) list
val find_some_sols : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard ->
guard * (Var.env_out * Var.env_loc) list
val find_one_sol : t -> guard -> (Var.env_out * Var.env_loc)
val find_one_sol : t -> guard -> guard * (Var.env_out * Var.env_loc)
val make_pre : Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
......
......@@ -282,7 +282,7 @@ let to_exe oc infile mnode opt = (
| LutExe.Goto (zeguard, ctrl') -> (
(* THIS IS THE NORMAL BEHAVIOR *)
MainArg.event_incr opt;
let (outs, locs) = try LutExe.find_one_sol exe zeguard
let zeguard, (outs, locs) = try LutExe.find_one_sol exe zeguard
with Not_found -> assert false
in
(* Try to display more useful source level info with -vl
......
Markdown is supported
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