paulson@5277: (* Title: HOL/UNITY/Lift.thy paulson@5277: ID: $Id$ paulson@5277: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@5277: Copyright 1998 University of Cambridge paulson@5277: paulson@5277: The Lift-Control Example paulson@5277: *) paulson@5277: paulson@5277: Lift = SubstAx + paulson@5277: paulson@5277: record state = paulson@5563: floor :: int (*current position of the lift*) paulson@5277: open :: bool (*whether the door is open at floor*) paulson@5277: stop :: bool (*whether the lift is stopped at floor*) paulson@5563: req :: int set (*for each floor, whether the lift is requested*) paulson@5277: up :: bool (*current direction of movement*) paulson@5277: move :: bool (*whether moving takes precedence over opening*) paulson@5277: paulson@5277: consts paulson@5563: Min, Max :: int (*least and greatest floors*) paulson@5277: paulson@5277: rules paulson@5357: Min_le_Max "Min <= Max" paulson@5277: paulson@5277: constdefs paulson@5277: paulson@5277: (** Abbreviations: the "always" part **) paulson@5277: paulson@5320: above :: state set paulson@5357: "above == {s. EX i. floor s < i & i <= Max & i : req s}" paulson@5277: paulson@5320: below :: state set paulson@5357: "below == {s. EX i. Min <= i & i < floor s & i : req s}" paulson@5277: paulson@5320: queueing :: state set paulson@5277: "queueing == above Un below" paulson@5277: paulson@5320: goingup :: state set paulson@5340: "goingup == above Int ({s. up s} Un Compl below)" paulson@5277: paulson@5320: goingdown :: state set paulson@5277: "goingdown == below Int ({s. ~ up s} Un Compl above)" paulson@5277: paulson@5320: ready :: state set paulson@5277: "ready == {s. stop s & ~ open s & move s}" paulson@5277: paulson@5320: paulson@5320: (** Further abbreviations **) paulson@5277: paulson@5320: moving :: state set paulson@5320: "moving == {s. ~ stop s & ~ open s}" paulson@5320: paulson@5320: stopped :: state set paulson@5340: "stopped == {s. stop s & ~ open s & ~ move s}" paulson@5320: paulson@5320: opened :: state set paulson@5320: "opened == {s. stop s & open s & move s}" paulson@5320: paulson@5340: closed :: state set (*but this is the same as ready!!*) paulson@5320: "closed == {s. stop s & ~ open s & move s}" paulson@5320: paulson@5563: atFloor :: int => state set paulson@5320: "atFloor n == {s. floor s = n}" paulson@5320: paulson@5563: Req :: int => state set paulson@5340: "Req n == {s. n : req s}" paulson@5340: paulson@5320: paulson@5320: paulson@5277: (** The program **) paulson@5277: paulson@5277: request_act :: "(state*state) set" paulson@5277: "request_act == {(s,s'). s' = s (|stop:=True, move:=False|) paulson@5277: & ~ stop s & floor s : req s}" paulson@5277: paulson@5277: open_act :: "(state*state) set" paulson@5277: "open_act == paulson@5277: {(s,s'). s' = s (|open :=True, paulson@5277: req := req s - {floor s}, paulson@5277: move := True|) paulson@5277: & stop s & ~ open s & floor s : req s paulson@5277: & ~(move s & s: queueing)}" paulson@5277: paulson@5277: close_act :: "(state*state) set" paulson@5277: "close_act == {(s,s'). s' = s (|open := False|) & open s}" paulson@5277: paulson@5357: req_up :: "(state*state) set" paulson@5357: "req_up == paulson@5277: {(s,s'). s' = s (|stop :=False, paulson@5563: floor := floor s + #1, paulson@5277: up := True|) paulson@5277: & s : (ready Int goingup)}" paulson@5277: paulson@5357: req_down :: "(state*state) set" paulson@5357: "req_down == paulson@5277: {(s,s'). s' = s (|stop :=False, paulson@5563: floor := floor s - #1, paulson@5277: up := False|) paulson@5277: & s : (ready Int goingdown)}" paulson@5277: paulson@5277: move_up :: "(state*state) set" paulson@5277: "move_up == paulson@5563: {(s,s'). s' = s (|floor := floor s + #1|) paulson@5277: & ~ stop s & up s & floor s ~: req s}" paulson@5277: paulson@5277: move_down :: "(state*state) set" paulson@5277: "move_down == paulson@5563: {(s,s'). s' = s (|floor := floor s - #1|) paulson@5277: & ~ stop s & ~ up s & floor s ~: req s}" paulson@5277: paulson@5357: button_press :: "(state*state) set" paulson@5357: "button_press == paulson@5357: {(s,s'). EX n. s' = s (|req := insert n (req s)|) paulson@5357: & Min <= n & n <= Max}" paulson@5357: paulson@5357: paulson@5277: Lprg :: state program paulson@5357: (*for the moment, we OMIT button_press*) paulson@5596: "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s & paulson@5277: ~ open s & req s = {}}, paulson@5596: {request_act, open_act, close_act, paulson@5596: req_up, req_down, move_up, move_down})" paulson@5277: paulson@5277: paulson@5277: (** Invariants **) paulson@5277: paulson@5277: bounded :: state set paulson@5357: "bounded == {s. Min <= floor s & floor s <= Max}" paulson@5277: paulson@5277: open_stop :: state set paulson@5277: "open_stop == {s. open s --> stop s}" paulson@5277: paulson@5277: open_move :: state set paulson@5277: "open_move == {s. open s --> move s}" paulson@5277: paulson@5277: stop_floor :: state set paulson@5340: "stop_floor == {s. stop s & ~ move s --> floor s : req s}" paulson@5277: paulson@5277: moving_up :: state set paulson@5277: "moving_up == {s. ~ stop s & up s --> paulson@5357: (EX f. floor s <= f & f <= Max & f : req s)}" paulson@5277: paulson@5277: moving_down :: state set paulson@5277: "moving_down == {s. ~ stop s & ~ up s --> paulson@5357: (EX f. Min <= f & f <= floor s & f : req s)}" paulson@5277: paulson@5563: metric :: [int,state] => int paulson@5357: "metric == paulson@5563: %n s. if floor s < n then (if up s then n - floor s paulson@5563: else (floor s - Min) + (n-Min)) paulson@5563: else paulson@5563: if n < floor s then (if up s then (Max - floor s) + (Max-n) paulson@5563: else floor s - n) paulson@5563: else #0" paulson@5340: paulson@5340: locale floor = paulson@5340: fixes paulson@5563: n :: int paulson@5340: assumes paulson@5357: Min_le_n "Min <= n" paulson@5357: n_le_Max "n <= Max" paulson@5340: defines paulson@5277: paulson@5277: end