8334
|
1 |
(* Title: HOL/UNITY/Reachability
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tanja Vos, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2000 University of Cambridge
|
|
5 |
|
|
6 |
Reachability in Graphs
|
|
7 |
|
|
8 |
From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
|
|
9 |
*)
|
|
10 |
|
|
11 |
Reachability = Detects +
|
|
12 |
|
|
13 |
types edge = "(vertex*vertex)"
|
|
14 |
|
|
15 |
record state =
|
|
16 |
reach :: vertex => bool
|
|
17 |
nmsg :: edge => nat
|
|
18 |
|
|
19 |
consts REACHABLE :: edge set
|
|
20 |
root :: vertex
|
|
21 |
E :: edge set
|
|
22 |
V :: vertex set
|
|
23 |
|
|
24 |
inductive "REACHABLE"
|
|
25 |
intrs
|
|
26 |
base "v : V ==> ((v,v) : REACHABLE)"
|
|
27 |
step "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
|
|
28 |
|
|
29 |
constdefs
|
|
30 |
reachable :: vertex => state set
|
|
31 |
"reachable p == {s. reach s p}"
|
|
32 |
|
|
33 |
nmsg_eq :: nat => edge => state set
|
|
34 |
"nmsg_eq k == %e. {s. nmsg s e = k}"
|
|
35 |
|
|
36 |
nmsg_gt :: nat => edge => state set
|
|
37 |
"nmsg_gt k == %e. {s. k < nmsg s e}"
|
|
38 |
|
|
39 |
nmsg_gte :: nat => edge => state set
|
|
40 |
"nmsg_gte k == %e. {s. k <= nmsg s e}"
|
|
41 |
|
|
42 |
nmsg_lte :: nat => edge => state set
|
|
43 |
"nmsg_lte k == %e. {s. nmsg s e <= k}"
|
|
44 |
|
|
45 |
|
|
46 |
|
|
47 |
final :: state set
|
|
48 |
"final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
|
|
49 |
|
|
50 |
rules
|
|
51 |
Graph1 "root : V"
|
|
52 |
|
|
53 |
Graph2 "(v,w) : E ==> (v : V) & (w : V)"
|
|
54 |
|
|
55 |
MA1 "F : Always (reachable root)"
|
|
56 |
|
|
57 |
MA2 "[|v:V|] ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
|
|
58 |
|
|
59 |
MA3 "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
|
|
60 |
|
|
61 |
MA4 "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
|
|
62 |
|
|
63 |
MA5 "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w))"
|
|
64 |
|
|
65 |
MA6 "[|v:V|] ==> F : Stable (reachable v)"
|
|
66 |
|
|
67 |
MA6b "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
|
|
68 |
|
|
69 |
MA7 "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
|
|
70 |
|
|
71 |
end
|
|
72 |
|