diff --git a/src/Coverage.ml b/src/Coverage.ml index af5adbc494b7da1ef9e353d2fde17712300ad7c3..05fb89565afea4b70d23bbe72149de93f56d49ce 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