85 "close_act == {(s,s'). s' = s (|open := False|) & open s}" |
85 "close_act == {(s,s'). s' = s (|open := False|) & open s}" |
86 |
86 |
87 req_up :: "(state*state) set" |
87 req_up :: "(state*state) set" |
88 "req_up == |
88 "req_up == |
89 {(s,s'). s' = s (|stop :=False, |
89 {(s,s'). s' = s (|stop :=False, |
90 floor := floor s + #1, |
90 floor := floor s + Numeral1, |
91 up := True|) |
91 up := True|) |
92 & s : (ready Int goingup)}" |
92 & s : (ready Int goingup)}" |
93 |
93 |
94 req_down :: "(state*state) set" |
94 req_down :: "(state*state) set" |
95 "req_down == |
95 "req_down == |
96 {(s,s'). s' = s (|stop :=False, |
96 {(s,s'). s' = s (|stop :=False, |
97 floor := floor s - #1, |
97 floor := floor s - Numeral1, |
98 up := False|) |
98 up := False|) |
99 & s : (ready Int goingdown)}" |
99 & s : (ready Int goingdown)}" |
100 |
100 |
101 move_up :: "(state*state) set" |
101 move_up :: "(state*state) set" |
102 "move_up == |
102 "move_up == |
103 {(s,s'). s' = s (|floor := floor s + #1|) |
103 {(s,s'). s' = s (|floor := floor s + Numeral1|) |
104 & ~ stop s & up s & floor s ~: req s}" |
104 & ~ stop s & up s & floor s ~: req s}" |
105 |
105 |
106 move_down :: "(state*state) set" |
106 move_down :: "(state*state) set" |
107 "move_down == |
107 "move_down == |
108 {(s,s'). s' = s (|floor := floor s - #1|) |
108 {(s,s'). s' = s (|floor := floor s - Numeral1|) |
109 & ~ stop s & ~ up s & floor s ~: req s}" |
109 & ~ stop s & ~ up s & floor s ~: req s}" |
110 |
110 |
111 (*This action is omitted from prior treatments, which therefore are |
111 (*This action is omitted from prior treatments, which therefore are |
112 unrealistic: nobody asks the lift to do anything! But adding this |
112 unrealistic: nobody asks the lift to do anything! But adding this |
113 action invalidates many of the existing progress arguments: various |
113 action invalidates many of the existing progress arguments: various |