Commit 7c56884f authored by bguillaum's avatar bguillaum

add the debug_loop mode

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/semagramme/libcaml-grew/trunk@9031 7838e531-6607-4d57-9587-6c381814729c
parent 8a741963
...@@ -85,9 +85,11 @@ module Rule = struct ...@@ -85,9 +85,11 @@ module Rule = struct
(* the rewriting depth is bounded to stop rewriting when the system is not terminating *) (* the rewriting depth is bounded to stop rewriting when the system is not terminating *)
let max_depth_det = ref 2000 let max_depth_det = ref 2000
let max_depth_non_det = ref 100 let max_depth_non_det = ref 100
let debug_loop = ref false
let set_max_depth_det value = max_depth_det := value let set_max_depth_det value = max_depth_det := value
let set_max_depth_non_det value = max_depth_non_det := value let set_max_depth_non_det value = max_depth_non_det := value
let set_debug_loop () = debug_loop := true
type const = type const =
| Cst_out of Pid.t * Label_cst.t | Cst_out of Pid.t * Label_cst.t
...@@ -876,18 +878,11 @@ module Rule = struct ...@@ -876,18 +878,11 @@ module Rule = struct
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** [apply_rule instance matching rule] returns a new instance after the application of the rule (** [apply_rule instance matching rule] returns a new instance after the application of the rule
[Command_execution_fail] is raised if some merge unification fails *) [Command_execution_fail] is raised if some merge unification fails *)
let apply_rule domain modul_name max_depth instance matching rule = let apply_rule domain modul_name instance matching rule =
(* Timeout check *) (* Timeout check *)
(try Timeout.check () with Timeout.Stop -> Error.run "Time out"); (try Timeout.check () with Timeout.Stop -> Error.run "Time out");
(* limit the rewriting depth to avoid looping rewriting *)
begin
if List.length instance.Instance.rules >= max_depth
then Error.run "[Module %s] max depth %d reached, last rules applied: …, %s, %s"
modul_name max_depth (List_.rev_to_string (fun x->x) ", " (List_.cut 4 instance.Instance.rules)) rule.name
end;
let (new_instance, created_nodes) = let (new_instance, created_nodes) =
List.fold_left List.fold_left
(fun (instance, created_nodes) command -> (fun (instance, created_nodes) command ->
...@@ -976,24 +971,41 @@ module Rule = struct ...@@ -976,24 +971,41 @@ module Rule = struct
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** [one_step domain modul_name instance rules] computes the list of one-step reduct with rules *) (** [one_step domain modul_name instance rules] computes the list of one-step reduct with rules *)
let one_step domain modul_name instance rules = let one_step domain modul_name instance rules =
List.fold_left
(fun acc rule ->
let matching_list = match_in_graph domain ?param:rule.param rule.pattern instance.Instance.graph in
List.fold_left (* limit the rewriting depth to avoid looping rewriting *)
(fun acc1 matching -> if List.length instance.Instance.rules >= !max_depth_non_det
try (apply_rule domain modul_name !max_depth_non_det instance matching rule) :: acc1 then
with Command_execution_fail -> acc1 if !debug_loop
) acc matching_list then []
) [] rules else Error.run "[Module %s] max depth %d reached, last rules applied: …, %s"
modul_name !max_depth_non_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else
List.fold_left
(fun acc rule ->
let matching_list = match_in_graph domain ?param:rule.param rule.pattern instance.Instance.graph in
List.fold_left
(fun acc1 matching ->
try (apply_rule domain modul_name instance matching rule) :: acc1
with Command_execution_fail -> acc1
) acc matching_list
) [] rules
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** [conf_one_step domain modul_name instance rules] computes one Some (one-step reduct) with rules, None if no rule apply *) (** [conf_one_step domain modul_name instance rules] computes one Some (one-step reduct) with rules, None if no rule apply *)
let rec conf_one_step domain modul_name (instance : Instance.t) = function let rec conf_one_step domain modul_name (instance : Instance.t) rules =
| [] -> None
| rule::rule_tail ->
let (pos,negs) = rule.pattern in
(* limit the rewriting depth to avoid looping rewriting *)
if List.length instance.Instance.rules >= !max_depth_det
then
if !debug_loop
then None
else Error.run "[Module %s] max depth %d reached, last rules applied: …, %s"
modul_name !max_depth_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else
match rules with
| [] -> None
| rule::rule_tail ->
let (pos,negs) = rule.pattern in
(* get the list of partial matching for positive part of the pattern *) (* get the list of partial matching for positive part of the pattern *)
let matching_list = let matching_list =
extend_matching extend_matching
...@@ -1001,7 +1013,6 @@ module Rule = struct ...@@ -1001,7 +1013,6 @@ module Rule = struct
(pos.graph,P_graph.empty) (pos.graph,P_graph.empty)
instance.Instance.graph instance.Instance.graph
(init rule.param pos) in (init rule.param pos) in
try try
let (first_matching_where_all_witout_are_fulfilled,_) = let (first_matching_where_all_witout_are_fulfilled,_) =
List.find List.find
...@@ -1012,10 +1023,9 @@ module Rule = struct ...@@ -1012,10 +1023,9 @@ module Rule = struct
fulfill domain (pos.graph,neg.graph) instance.Instance.graph new_partial_matching fulfill domain (pos.graph,neg.graph) instance.Instance.graph new_partial_matching
) negs ) negs
) matching_list in ) matching_list in
Some (apply_rule domain modul_name !max_depth_det instance first_matching_where_all_witout_are_fulfilled rule) Some (apply_rule domain modul_name instance first_matching_where_all_witout_are_fulfilled rule)
with Not_found -> (* try another rule *) conf_one_step domain modul_name instance rule_tail with Not_found -> (* try another rule *) conf_one_step domain modul_name instance rule_tail
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** filter nfs being equal *) (** filter nfs being equal *)
let rec filter_equal_nfs nfs = let rec filter_equal_nfs nfs =
......
...@@ -65,6 +65,10 @@ module Rule : sig ...@@ -65,6 +65,10 @@ module Rule : sig
(** [set_max_depth_non_det value] set the maximum rewriting depth in non-deterministic application of a module. *) (** [set_max_depth_non_det value] set the maximum rewriting depth in non-deterministic application of a module. *)
val set_max_depth_non_det: int -> unit val set_max_depth_non_det: int -> unit
(** [set_debug_loop ()] turns the debug mode on for loop: when the bound is reached, the graph is considered as a normal form.
This is a kind of hack to be able to explore loops in GUI. *)
val set_debug_loop: unit -> unit
(** [get_name t] returns the name of the rule [t]. *) (** [get_name t] returns the name of the rule [t]. *)
val get_name: t -> string val get_name: t -> string
......
...@@ -231,6 +231,8 @@ module Rewrite = struct ...@@ -231,6 +231,8 @@ module Rewrite = struct
let set_max_depth_det value = Grew_rule.Rule.set_max_depth_det value let set_max_depth_det value = Grew_rule.Rule.set_max_depth_det value
let set_max_depth_non_det value = Grew_rule.Rule.set_max_depth_non_det value let set_max_depth_non_det value = Grew_rule.Rule.set_max_depth_non_det value
let set_debug_loop () = Grew_rule.Rule.set_debug_loop ()
let display ~gr ~grs ~seq = let display ~gr ~grs ~seq =
handle ~name:"Rewrite.display" (fun () -> Grew_grs.Grs.build_rew_display grs seq gr) () handle ~name:"Rewrite.display" (fun () -> Grew_grs.Grs.build_rew_display grs seq gr) ()
......
...@@ -150,6 +150,7 @@ module Rewrite: sig ...@@ -150,6 +150,7 @@ module Rewrite: sig
val set_max_depth_det: int -> unit val set_max_depth_det: int -> unit
val set_max_depth_non_det: int -> unit val set_max_depth_non_det: int -> unit
val set_debug_loop: unit -> unit
(** [display gr grs seq] builds the [display] (datatype used by the GUI) given by (** [display gr grs seq] builds the [display] (datatype used by the GUI) given by
the rewriting of graph [gr] with the sequence [seq] of [grs]. the rewriting of graph [gr] with the sequence [seq] of [grs].
......
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