10782
|
1 |
(* Title: HOL/UNITY/Priority
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2001 University of Cambridge
|
|
5 |
|
|
6 |
The priority system
|
|
7 |
|
|
8 |
From Charpentier and Chandy,
|
|
9 |
Examples of Program Composition Illustrating the Use of Universal Properties
|
|
10 |
In J. Rolim (editor), Parallel and Distributed Processing,
|
|
11 |
Spriner LNCS 1586 (1999), pages 1215-1227.
|
|
12 |
*)
|
|
13 |
|
|
14 |
Priority = PriorityAux + Comp + SubstAx +
|
|
15 |
|
|
16 |
types state = "(vertex*vertex)set"
|
|
17 |
types command = "vertex=>(state*state)set"
|
|
18 |
|
|
19 |
consts
|
|
20 |
(* the initial state *)
|
|
21 |
init :: "(vertex*vertex)set"
|
|
22 |
|
|
23 |
constdefs
|
|
24 |
(* from the definitions given in section 4.4 *)
|
|
25 |
(* i has highest priority in r *)
|
|
26 |
highest :: "[vertex, (vertex*vertex)set]=>bool"
|
|
27 |
"highest i r == A i r = {}"
|
|
28 |
|
|
29 |
(* i has lowest priority in r *)
|
|
30 |
lowest :: "[vertex, (vertex*vertex)set]=>bool"
|
|
31 |
"lowest i r == R i r = {}"
|
|
32 |
|
|
33 |
act :: command
|
|
34 |
"act i == {(s, s'). s'=reverse i s & highest i s}"
|
|
35 |
|
|
36 |
(* All components start with the same initial state *)
|
|
37 |
Component :: "vertex=>state program"
|
|
38 |
"Component i == mk_program({init}, {act i}, UNIV)"
|
|
39 |
|
|
40 |
(* Abbreviations *)
|
|
41 |
Highest :: "vertex=>state set"
|
|
42 |
"Highest i == {s. highest i s}"
|
|
43 |
|
|
44 |
Lowest :: "vertex=>state set"
|
|
45 |
"Lowest i == {s. lowest i s}"
|
|
46 |
|
|
47 |
Acyclic :: "state set"
|
|
48 |
"Acyclic == {s. acyclic s}"
|
|
49 |
|
|
50 |
(* Every above set has a maximal vertex: two equivalent defs. *)
|
|
51 |
|
|
52 |
Maximal :: "state set"
|
|
53 |
"Maximal == INT i. {s. ~highest i s-->(EX j:above i s. highest j s)}"
|
|
54 |
|
|
55 |
Maximal' :: "state set"
|
|
56 |
"Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)"
|
|
57 |
|
|
58 |
|
|
59 |
Safety :: "state set"
|
|
60 |
"Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}"
|
|
61 |
|
|
62 |
|
|
63 |
(* Composition of a finite set of component;
|
|
64 |
the vertex 'UNIV' is finite by assumption *)
|
|
65 |
|
|
66 |
system :: "state program"
|
|
67 |
"system == JN i. Component i"
|
|
68 |
end |