From c33d8aa55a11d155f224cc04172c31cfd8034ef2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Tue, 7 Jul 2015 13:31:17 +0200
Subject: [PATCH] Removed the call to [Dijkstra] and the comparison of results
with A*.
---
src/Coverage.ml | 68 +++++++++++++++++--------------------------------
1 file changed, 24 insertions(+), 44 deletions(-)
diff --git a/src/Coverage.ml b/src/Coverage.ml
index af5adbc49..05fb89565 100644
--- a/src/Coverage.ml
+++ b/src/Coverage.ml
@@ -34,62 +34,42 @@ open Grammar
yields a lower bound on the actual distance to every state from any entry
state. *)
-module ForwardAutomaton = struct
+let approximate : Lr1.node -> int =
- type vertex =
- Lr1.node
+ let module A = Astar.Make(struct
- let equal s1 s2 =
- Lr1.Node.compare s1 s2 = 0
+ type node =
+ Lr1.node
- let hash s =
- Hashtbl.hash (Lr1.number s)
+ let equal s1 s2 =
+ Lr1.Node.compare s1 s2 = 0
- type label =
- unit
+ let hash s =
+ Hashtbl.hash (Lr1.number s)
- let sources f =
- (* The sources are the entry states. *)
- ProductionMap.iter (fun _ s -> f s) Lr1.entry
+ type label =
+ unit
- let successors s edge =
- SymbolMap.iter (fun sym s' ->
- (* The weight of the edge from [s] to [s'] is given by the function
- [Grammar.Analysis.minimal_symbol]. *)
- edge () (CompletedNatWitness.to_int (Analysis.minimal_symbol sym)) s'
- ) (Lr1.transitions s)
+ let sources f =
+ (* The sources are the entry states. *)
+ ProductionMap.iter (fun _ s -> f s) Lr1.entry
-end
+ let successors s edge =
+ SymbolMap.iter (fun sym s' ->
+ (* The weight of the edge from [s] to [s'] is given by the function
+ [Grammar.Analysis.minimal_symbol]. *)
+ edge () (CompletedNatWitness.to_int (Analysis.minimal_symbol sym)) s'
+ ) (Lr1.transitions s)
-let approximate : Lr1.node -> int =
- let module D = Dijkstra.Make(ForwardAutomaton) in
- D.search (fun (_, _, _) -> ())
+ let estimate _ =
+ (* A* with a zero [estimate] behaves like Dijkstra's algorithm. *)
+ 0
-let approx : Lr1.node -> int =
- let module A = Astar.Make(struct
- include ForwardAutomaton
- let estimate _ = 0
- type node = vertex
end) in
+
let distance, _ = A.search (fun (_, _) -> ()) in
distance
-(* Debugging. TEMPORARY *)
-let approximate s =
- let d1 = approximate s
- and d2 = approx s in
- assert (d1 = d2);
- d1
-
-(* Test. TEMPORARY *)
-
-let () =
- Lr1.iter (fun s ->
- Printf.fprintf stderr
- "State %d is at least %d steps away from an initial state.\n%!"
- (Lr1.number s) (approximate s)
- )
-
(* ------------------------------------------------------------------------ *)
(* Auxiliary functions. *)
@@ -434,7 +414,7 @@ let backward (s', z) : unit =
) (Lr1.predecessors s')
let estimate (s', _z) =
- approx s'
+ approximate s'
end) in
--
GitLab