|
1 (* Title: HOL/UNITY/Lift.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 The Lift-Control Example |
|
7 *) |
|
8 |
|
9 Lift = SubstAx + |
|
10 |
|
11 record state = |
|
12 floor :: int (*current position of the lift*) |
|
13 open :: bool (*whether the door is open at floor*) |
|
14 stop :: bool (*whether the lift is stopped at floor*) |
|
15 req :: int set (*for each floor, whether the lift is requested*) |
|
16 up :: bool (*current direction of movement*) |
|
17 move :: bool (*whether moving takes precedence over opening*) |
|
18 |
|
19 consts |
|
20 Min, Max :: int (*least and greatest floors*) |
|
21 |
|
22 rules |
|
23 Min_le_Max "Min <= Max" |
|
24 |
|
25 constdefs |
|
26 |
|
27 (** Abbreviations: the "always" part **) |
|
28 |
|
29 above :: state set |
|
30 "above == {s. EX i. floor s < i & i <= Max & i : req s}" |
|
31 |
|
32 below :: state set |
|
33 "below == {s. EX i. Min <= i & i < floor s & i : req s}" |
|
34 |
|
35 queueing :: state set |
|
36 "queueing == above Un below" |
|
37 |
|
38 goingup :: state set |
|
39 "goingup == above Int ({s. up s} Un -below)" |
|
40 |
|
41 goingdown :: state set |
|
42 "goingdown == below Int ({s. ~ up s} Un -above)" |
|
43 |
|
44 ready :: state set |
|
45 "ready == {s. stop s & ~ open s & move s}" |
|
46 |
|
47 |
|
48 (** Further abbreviations **) |
|
49 |
|
50 moving :: state set |
|
51 "moving == {s. ~ stop s & ~ open s}" |
|
52 |
|
53 stopped :: state set |
|
54 "stopped == {s. stop s & ~ open s & ~ move s}" |
|
55 |
|
56 opened :: state set |
|
57 "opened == {s. stop s & open s & move s}" |
|
58 |
|
59 closed :: state set (*but this is the same as ready!!*) |
|
60 "closed == {s. stop s & ~ open s & move s}" |
|
61 |
|
62 atFloor :: int => state set |
|
63 "atFloor n == {s. floor s = n}" |
|
64 |
|
65 Req :: int => state set |
|
66 "Req n == {s. n : req s}" |
|
67 |
|
68 |
|
69 |
|
70 (** The program **) |
|
71 |
|
72 request_act :: "(state*state) set" |
|
73 "request_act == {(s,s'). s' = s (|stop:=True, move:=False|) |
|
74 & ~ stop s & floor s : req s}" |
|
75 |
|
76 open_act :: "(state*state) set" |
|
77 "open_act == |
|
78 {(s,s'). s' = s (|open :=True, |
|
79 req := req s - {floor s}, |
|
80 move := True|) |
|
81 & stop s & ~ open s & floor s : req s |
|
82 & ~(move s & s: queueing)}" |
|
83 |
|
84 close_act :: "(state*state) set" |
|
85 "close_act == {(s,s'). s' = s (|open := False|) & open s}" |
|
86 |
|
87 req_up :: "(state*state) set" |
|
88 "req_up == |
|
89 {(s,s'). s' = s (|stop :=False, |
|
90 floor := floor s + #1, |
|
91 up := True|) |
|
92 & s : (ready Int goingup)}" |
|
93 |
|
94 req_down :: "(state*state) set" |
|
95 "req_down == |
|
96 {(s,s'). s' = s (|stop :=False, |
|
97 floor := floor s - #1, |
|
98 up := False|) |
|
99 & s : (ready Int goingdown)}" |
|
100 |
|
101 move_up :: "(state*state) set" |
|
102 "move_up == |
|
103 {(s,s'). s' = s (|floor := floor s + #1|) |
|
104 & ~ stop s & up s & floor s ~: req s}" |
|
105 |
|
106 move_down :: "(state*state) set" |
|
107 "move_down == |
|
108 {(s,s'). s' = s (|floor := floor s - #1|) |
|
109 & ~ stop s & ~ up s & floor s ~: req s}" |
|
110 |
|
111 (*This action is omitted from prior treatments, which therefore are |
|
112 unrealistic: nobody asks the lift to do anything! But adding this |
|
113 action invalidates many of the existing progress arguments: various |
|
114 "ensures" properties fail.*) |
|
115 button_press :: "(state*state) set" |
|
116 "button_press == |
|
117 {(s,s'). EX n. s' = s (|req := insert n (req s)|) |
|
118 & Min <= n & n <= Max}" |
|
119 |
|
120 |
|
121 Lift :: state program |
|
122 (*for the moment, we OMIT button_press*) |
|
123 "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s & |
|
124 ~ open s & req s = {}}, |
|
125 {request_act, open_act, close_act, |
|
126 req_up, req_down, move_up, move_down}, |
|
127 UNIV)" |
|
128 |
|
129 |
|
130 (** Invariants **) |
|
131 |
|
132 bounded :: state set |
|
133 "bounded == {s. Min <= floor s & floor s <= Max}" |
|
134 |
|
135 open_stop :: state set |
|
136 "open_stop == {s. open s --> stop s}" |
|
137 |
|
138 open_move :: state set |
|
139 "open_move == {s. open s --> move s}" |
|
140 |
|
141 stop_floor :: state set |
|
142 "stop_floor == {s. stop s & ~ move s --> floor s : req s}" |
|
143 |
|
144 moving_up :: state set |
|
145 "moving_up == {s. ~ stop s & up s --> |
|
146 (EX f. floor s <= f & f <= Max & f : req s)}" |
|
147 |
|
148 moving_down :: state set |
|
149 "moving_down == {s. ~ stop s & ~ up s --> |
|
150 (EX f. Min <= f & f <= floor s & f : req s)}" |
|
151 |
|
152 metric :: [int,state] => int |
|
153 "metric == |
|
154 %n s. if floor s < n then (if up s then n - floor s |
|
155 else (floor s - Min) + (n-Min)) |
|
156 else |
|
157 if n < floor s then (if up s then (Max - floor s) + (Max-n) |
|
158 else floor s - n) |
|
159 else #0" |
|
160 |
|
161 locale floor = |
|
162 fixes |
|
163 n :: int |
|
164 assumes |
|
165 Min_le_n "Min <= n" |
|
166 n_le_Max "n <= Max" |
|
167 defines |
|
168 |
|
169 end |