Commit 0d6751fd authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Added [Heap], taken from ocamlgraph.

Added [Dijkstra], homemade.
Modified [Coverage] to use [Dijkstra].
Also found a heavy bug where [causes_an_error] used [s] instead of [s']?
parent e1807886
......@@ -301,83 +301,62 @@ let backward s ((s', z) : Q.t) (get : Q.t -> property) : property =
let es = ref 0
exception Success
let arriere s (s', z) =
exception Success of property
let arriere (s', z) : bool =
let module G = struct
type vertex = Q.t
type label = unit (* TEMPORARY *)
module M = Maps.PersistentMapsToImperativeMaps(QM)
let marks = M.create()
let dummy = Mark.fresh()
let set_mark v mark =
M.add v mark marks
let get_mark v =
try
M.find v marks
with Not_found ->
dummy
let entry f =
f (s', z)
let equal v1 v2 = Q.compare v1 v2 = 0
let hash (s, z) = Hashtbl.hash (Lr1.number s, z)
type label = int * Terminal.t Seq.seq
let weight (w, _) = w
let source = (s', z)
let successors edge (s', z) =
assert (Lr1.Node.compare s s' <> 0);
match Lr1.incoming_symbol s' with
| None ->
(* We have reached a start symbol, but not the one we hoped for. *)
(* A start symbol has no predecessors. *)
()
| Some (Symbol.T t) ->
List.iter (fun pred ->
edge () (pred, t)
edge (1, Seq.singleton t) (pred, t)
) (Lr1.predecessors s')
| Some (Symbol.N nt) ->
List.iter (fun pred ->
Production.foldnt nt () (fun prod () ->
TerminalSet.iter (fun a ->
let _w = answer { s = pred; a = a; prod = prod; i = 0; z = z } in
edge () (pred, a)
match answer { s = pred; a = a; prod = prod; i = 0; z = z } with
| P.Infinity ->
()
| P.Finite (w, ts) ->
edge (w, ts) (pred, a)
) (first prod 0 z)
)
) (Lr1.predecessors s')
end in
let module B = Breadth.Make(G) in
let module D = Dijkstra.Make(G) in
try
if Lr1.Node.compare s s' = 0 then
raise Success;
B.search (fun _discovery _v () (v', _) ->
D.search (fun (distance, (v', _), _path) ->
incr es;
if !es mod 10000 = 0 then
Printf.fprintf stderr "es = %d\n%!" !es;
if Lr1.Node.compare v' s = 0 then
raise Success
if Lr1.incoming_symbol v' = None then
raise (Success (P.Finite (distance, Seq.empty))) (* TEMPORARY keep path *)
);
Printf.fprintf stderr "Unreachable.\n%!";
false
with Success ->
with Success _ ->
Printf.fprintf stderr "Got it.\n%!";
true
let arriere s' : bool =
(* Compute which states can reach the goal state [s']. *)
let relevant = Lr1.reverse_dfs s' in
Printf.fprintf stderr
"Attempting to reach an error in state %d:\n%!"
(Lr1.number s');
(* Iterate over all possible start states. *)
Lr1.fold_entry (fun _ s _ _ accu ->
Terminal.fold (fun z accu ->
accu ||
(* If [s] cannot reach [s'], there is no need to look for a path. *)
relevant s && begin
Printf.fprintf stderr
"Attempting to go from state %d to an error in state %d:\n%!"
(Lr1.number s) (Lr1.number s');
Terminal.fold (fun z accu ->
accu ||
causes_an_error s z &&
arriere s (s', z)
) accu
end
causes_an_error s' z &&
arriere (s', z)
) false
(* Debugging wrapper. TEMPORARY *)
......
(* This module implements Dijkstra's algorithm over a graph with labeled
weighted edges. (We assume the weight is contained in the label.) *)
module Make (G : sig
(* This is the type of graph vertices. *)
type vertex
include Hashtbl.HashedType with type t := vertex
(* This is the type of graph labels. *)
type label
(* A graph label implies a nonnegative integer weight. *)
val weight: label -> int
(* The source vertex. *)
val source: vertex
(* This provides access to a vertex' successors. *)
val successors: (label -> vertex -> unit) -> vertex -> unit
end) = struct
open G
(* The priority queue contains triples of a total weight, a vertex,
and the discovery path for this vertex -- a list of labels. *)
module Element = struct
type t = int * vertex * label list
let compare (w1, _, _) (w2, _, _) =
Pervasives.compare w2 w1 (* switched because [Heap] uses the wrong convention *)
end
module PQ =
Heap.Imperative(Element)
(* A hash table maps vertices to distances. Another table maps vertices to unit
values, indicating whether this distance is final. *)
module H =
Hashtbl.Make(struct include G type t = vertex end)
let search f =
(* Create the data structures. *)
let queue = PQ.create 1024 in
let dist : int H.t = H.create 1023 in
let fixed : unit H.t = H.create 1023 in
(* A handy accessor. *)
let distance v =
try H.find dist v with Not_found -> max_int
in
(* Insert the initial vertex. *)
PQ.add queue (0, source, []);
H.add dist source 0;
(* As long as the queue is nonempty, ... *)
while not (PQ.is_empty queue) do
(* Extract one vertex. *)
let (w, v, p) = PQ.pop_maximum queue in
(* Check if this vertex is final already. If so, nothing to do. *)
if not (H.mem fixed v) then begin
(* Mark it final. *)
H.add fixed v ();
(* Let the client know about it. *)
f (w, v, p);
(* Examine its outgoing edges. *)
successors (fun label v' ->
let w' = weight label + w in
if w' < distance v' then begin
assert (not (H.mem fixed v'));
H.replace dist v' w';
PQ.add queue (w', v', label :: p)
end
) v
end
done
end
(**************************************************************************)
(* *)
(* Ocamlgraph: a generic graph library for OCaml *)
(* Copyright (C) 2004-2010 *)
(* Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* $Id:$ *)
module type Ordered = sig
type t
val compare : t -> t -> int
end
exception EmptyHeap
(*s Imperative implementation *)
module Imperative(X : Ordered) = struct
(* The heap is encoded in the array [data], where elements are stored
from [0] to [size - 1]. From an element stored at [i], the left
(resp. right) subtree, if any, is rooted at [2*i+1] (resp. [2*i+2]). *)
type t = { mutable size : int; mutable data : X.t array }
(* When [create n] is called, we cannot allocate the array, since there is
no known value of type [X.t]; we'll wait for the first addition to
do it, and we remember this situation with a negative size. *)
let create n =
if n <= 0 then invalid_arg "create";
{ size = -n; data = [||] }
let is_empty h = h.size <= 0
(* [resize] doubles the size of [data] *)
let resize h =
let n = h.size in
assert (n > 0);
let n' = 2 * n in
let d = h.data in
let d' = Array.make n' d.(0) in
Array.blit d 0 d' 0 n;
h.data <- d'
let add h x =
(* first addition: we allocate the array *)
if h.size < 0 then begin
h.data <- Array.make (- h.size) x; h.size <- 0
end;
let n = h.size in
(* resizing if needed *)
if n == Array.length h.data then resize h;
let d = h.data in
(* moving [x] up in the heap *)
let rec moveup i =
let fi = (i - 1) / 2 in
if i > 0 && X.compare d.(fi) x < 0 then begin
d.(i) <- d.(fi);
moveup fi
end else
d.(i) <- x
in
moveup n;
h.size <- n + 1
let maximum h =
if h.size <= 0 then raise EmptyHeap;
h.data.(0)
let remove h =
if h.size <= 0 then raise EmptyHeap;
let n = h.size - 1 in
h.size <- n;
let d = h.data in
let x = d.(n) in
(* moving [x] down in the heap *)
let rec movedown i =
let j = 2 * i + 1 in
if j < n then
let j =
let j' = j + 1 in
if j' < n && X.compare d.(j') d.(j) > 0 then j' else j
in
if X.compare d.(j) x > 0 then begin
d.(i) <- d.(j);
movedown j
end else
d.(i) <- x
else
d.(i) <- x
in
movedown 0
let pop_maximum h = let m = maximum h in remove h; m
let iter f h =
let d = h.data in
for i = 0 to h.size - 1 do f d.(i) done
let fold f h x0 =
let n = h.size in
let d = h.data in
let rec foldrec x i =
if i >= n then x else foldrec (f d.(i) x) (succ i)
in
foldrec x0 0
end
(**************************************************************************)
(* *)
(* Ocamlgraph: a generic graph library for OCaml *)
(* Copyright (C) 2004-2010 *)
(* Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
module type Ordered = sig
type t
val compare : t -> t -> int
end
exception EmptyHeap
(*S Imperative implementation. *)
module Imperative(X: Ordered) : sig
(* Type of imperative heaps.
(In the following [n] refers to the number of elements in the heap) *)
type t
(* [create c] creates a new heap, with initial capacity of [c] *)
val create : int -> t
(* [is_empty h] checks the emptiness of [h] *)
val is_empty : t -> bool
(* [add x h] adds a new element [x] in heap [h]; size of [h] is doubled
when maximum capacity is reached; complexity $O(log(n))$ *)
val add : t -> X.t -> unit
(* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
when [h] is empty; complexity $O(1)$ *)
val maximum : t -> X.t
(* [remove h] removes the maximum element of [h]; raises [EmptyHeap]
when [h] is empty; complexity $O(log(n))$ *)
val remove : t -> unit
(* [pop_maximum h] removes the maximum element of [h] and returns it;
raises [EmptyHeap] when [h] is empty; complexity $O(log(n))$ *)
val pop_maximum : t -> X.t
(* usual iterators and combinators; elements are presented in
arbitrary order *)
val iter : (X.t -> unit) -> t -> unit
val fold : (X.t -> 'a -> 'a) -> t -> 'a -> 'a
end
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