equal
deleted
inserted
replaced
114 & Min <= n & n <= Max}" |
114 & Min <= n & n <= Max}" |
115 |
115 |
116 |
116 |
117 Lprg :: state program |
117 Lprg :: state program |
118 (*for the moment, we OMIT button_press*) |
118 (*for the moment, we OMIT button_press*) |
119 "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s & |
119 "Lprg == mk_program (UNIV, |
|
120 {s. floor s = Min & ~ up s & move s & stop s & |
120 ~ open s & req s = {}}, |
121 ~ open s & req s = {}}, |
121 {request_act, open_act, close_act, |
122 {request_act, open_act, close_act, |
122 req_up, req_down, move_up, move_down})" |
123 req_up, req_down, move_up, move_down})" |
123 |
124 |
124 |
125 |