
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@5357:     "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
paulson@5277: 		          ~ open s & req s = {}},
paulson@5584: 	       Acts0 = {request_act, open_act, close_act,
paulson@5584: 		        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




