1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(* Given a DIRECTED graph G represented by a list of
(x , [neighbours of x])
then (have_cycle G) returns true if G has a nontrivial cycle.
Remark : G is not necessarly connected. *******)
type mark = NotMarked | OnThePath | AlreadyVisited;;
let df_cycle v marks g =
let rec df_cycle_rec x =
(List.assoc x marks) := OnThePath;
let nx = List.assoc x g
in let nb_marks =
List.fold_left (fun s x -> if !(List.assoc x marks)=OnThePath
then s+1 else s) 0 nx
in if nb_marks>0
then true
else let isc = List.fold_left (fun r y -> if r then true
else if !(List.assoc y marks)=AlreadyVisited
then false
else (df_cycle_rec y)) false nx
in if isc then true
else ((List.assoc x marks) := AlreadyVisited; false)
and df_init ls = match ls with
(s::lls) -> if (!(List.assoc s marks)=NotMarked)
& ((List.length (List.assoc s g))>0)
then (if df_cycle_rec s
then true
else df_init lls)
else df_init lls
| [] -> false
in df_init v;;
let have_cycle g =
let v = List.map (fun (x,_) -> x) g
in let marks = List.map (fun x -> (x,ref NotMarked)) v
in if List.length g<2
then false
else let x0 = fst (List.hd g)
in df_cycle v marks g;;
(* Examples...
have_cycle [(1,[2;3]); (2,[3]); (3,[])];; (false)
have_cycle [(1,[2;3]); (2,[1;3]); (3,[1;2])];; (true)
have_cycle [(1 , [6]);
(2 , [3;4;5]);
(3 , [2;5]);
(4 , [2]);
(5 , [2;3]);
(6 , [1])];; (true)
have_cycle [(2,[3]); (4,[]); (1,[4]); (3,[])];; (false)
have_cycle [(3,[1;2]); (4,[]); (2,[4]); (1,[4])];; (false)
*)
|
