|
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 :: nat (*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 :: nat 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 :: nat (*least and greatest floors*) |
|
21 |
|
22 rules |
|
23 min_le_max "min <= max" |
|
24 |
|
25 |
|
26 constdefs |
|
27 |
|
28 (** Abbreviations: the "always" part **) |
|
29 |
|
30 above :: "state set" |
|
31 "above == {s. EX i. floor s < i & i <= max & i : req s}" |
|
32 |
|
33 below :: "state set" |
|
34 "below == {s. EX i. min <= i & i < floor s & i : req s}" |
|
35 |
|
36 queueing :: "state set" |
|
37 "queueing == above Un below" |
|
38 |
|
39 goingup :: "state set" |
|
40 "goingup == above Int ({s. up s} Un Compl below)" |
|
41 |
|
42 goingdown :: "state set" |
|
43 "goingdown == below Int ({s. ~ up s} Un Compl above)" |
|
44 |
|
45 ready :: "state set" |
|
46 "ready == {s. stop s & ~ open s & move s}" |
|
47 |
|
48 |
|
49 (** The program **) |
|
50 |
|
51 request_act :: "(state*state) set" |
|
52 "request_act == {(s,s'). s' = s (|stop:=True, move:=False|) |
|
53 & ~ stop s & floor s : req s}" |
|
54 |
|
55 open_act :: "(state*state) set" |
|
56 "open_act == |
|
57 {(s,s'). s' = s (|open :=True, |
|
58 req := req s - {floor s}, |
|
59 move := True|) |
|
60 & stop s & ~ open s & floor s : req s |
|
61 & ~(move s & s: queueing)}" |
|
62 |
|
63 close_act :: "(state*state) set" |
|
64 "close_act == {(s,s'). s' = s (|open := False|) & open s}" |
|
65 |
|
66 req_up_act :: "(state*state) set" |
|
67 "req_up_act == |
|
68 {(s,s'). s' = s (|stop :=False, |
|
69 floor := Suc (floor s), |
|
70 up := True|) |
|
71 & s : (ready Int goingup)}" |
|
72 |
|
73 req_down_act :: "(state*state) set" |
|
74 "req_down_act == |
|
75 {(s,s'). s' = s (|stop :=False, |
|
76 floor := floor s - 1, |
|
77 up := False|) |
|
78 & s : (ready Int goingdown)}" |
|
79 |
|
80 move_up :: "(state*state) set" |
|
81 "move_up == |
|
82 {(s,s'). s' = s (|floor := Suc (floor s)|) |
|
83 & ~ stop s & up s & floor s ~: req s}" |
|
84 |
|
85 move_down :: "(state*state) set" |
|
86 "move_down == |
|
87 {(s,s'). s' = s (|floor := floor s - 1|) |
|
88 & ~ stop s & ~ up s & floor s ~: req s}" |
|
89 |
|
90 Lprg :: state program |
|
91 "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s & |
|
92 ~ open s & req s = {}}, |
|
93 Acts = {id, request_act, open_act, close_act, |
|
94 req_up_act, req_down_act, move_up, move_down}|)" |
|
95 |
|
96 |
|
97 (** Invariants **) |
|
98 |
|
99 bounded :: state set |
|
100 "bounded == {s. min <= floor s & floor s <= max}" |
|
101 |
|
102 (** ??? |
|
103 (~ stop s & up s --> floor s < max) & |
|
104 (~ stop s & ~ up s --> min < floor s)}" |
|
105 **) |
|
106 |
|
107 open_stop :: state set |
|
108 "open_stop == {s. open s --> stop s}" |
|
109 |
|
110 open_move :: state set |
|
111 "open_move == {s. open s --> move s}" |
|
112 |
|
113 stop_floor :: state set |
|
114 "stop_floor == {s. open s & ~ move s --> floor s : req s}" |
|
115 |
|
116 moving_up :: state set |
|
117 "moving_up == {s. ~ stop s & up s --> |
|
118 (EX f. floor s <= f & f <= max & f : req s)}" |
|
119 |
|
120 moving_down :: state set |
|
121 "moving_down == {s. ~ stop s & ~ up s --> |
|
122 (EX f. min <= f & f <= floor s & f : req s)}" |
|
123 |
|
124 valid :: "state set" |
|
125 "valid == bounded Int open_stop Int open_move" |
|
126 |
|
127 end |