src/HOL/UNITY/Simple/Lift.thy
author wenzelm
Fri Oct 05 21:52:39 2001 +0200 (2001-10-05)
changeset 11701 3d51fbf81c17
parent 11195 65ede8dfe304
child 11868 56db9f3a6b3e
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
     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 :: int		(*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   :: int 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 :: int       (*least and greatest floors*)
    21 
    22 rules
    23   Min_le_Max  "Min <= Max"
    24   
    25 constdefs
    26   
    27   (** Abbreviations: the "always" part **)
    28   
    29   above :: state set
    30     "above == {s. EX i. floor s < i & i <= Max & i : req s}"
    31 
    32   below :: state set
    33     "below == {s. EX i. Min <= i & i < floor s & i : req s}"
    34 
    35   queueing :: state set
    36     "queueing == above Un below"
    37 
    38   goingup :: state set
    39     "goingup   == above Int  ({s. up s}  Un -below)"
    40 
    41   goingdown :: state set
    42     "goingdown == below Int ({s. ~ up s} Un -above)"
    43 
    44   ready :: state set
    45     "ready == {s. stop s & ~ open s & move s}"
    46 
    47  
    48   (** Further abbreviations **)
    49 
    50   moving :: state set
    51     "moving ==  {s. ~ stop s & ~ open s}"
    52 
    53   stopped :: state set
    54     "stopped == {s. stop s  & ~ open s & ~ move s}"
    55 
    56   opened :: state set
    57     "opened ==  {s. stop s  &  open s  &  move s}"
    58 
    59   closed :: state set  (*but this is the same as ready!!*)
    60     "closed ==  {s. stop s  & ~ open s &  move s}"
    61 
    62   atFloor :: int => state set
    63     "atFloor n ==  {s. floor s = n}"
    64 
    65   Req :: int => state set
    66     "Req n ==  {s. n : req s}"
    67 
    68 
    69   
    70   (** The program **)
    71   
    72   request_act :: "(state*state) set"
    73     "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
    74 		                  & ~ stop s & floor s : req s}"
    75 
    76   open_act :: "(state*state) set"
    77     "open_act ==
    78          {(s,s'). s' = s (|open :=True,
    79 			   req  := req s - {floor s},
    80 			   move := True|)
    81 		       & stop s & ~ open s & floor s : req s
    82 	               & ~(move s & s: queueing)}"
    83 
    84   close_act :: "(state*state) set"
    85     "close_act == {(s,s'). s' = s (|open := False|) & open s}"
    86 
    87   req_up :: "(state*state) set"
    88     "req_up ==
    89          {(s,s'). s' = s (|stop  :=False,
    90 			   floor := floor s + Numeral1,
    91 			   up    := True|)
    92 		       & s : (ready Int goingup)}"
    93 
    94   req_down :: "(state*state) set"
    95     "req_down ==
    96          {(s,s'). s' = s (|stop  :=False,
    97 			   floor := floor s - Numeral1,
    98 			   up    := False|)
    99 		       & s : (ready Int goingdown)}"
   100 
   101   move_up :: "(state*state) set"
   102     "move_up ==
   103          {(s,s'). s' = s (|floor := floor s + Numeral1|)
   104 		       & ~ stop s & up s & floor s ~: req s}"
   105 
   106   move_down :: "(state*state) set"
   107     "move_down ==
   108          {(s,s'). s' = s (|floor := floor s - Numeral1|)
   109 		       & ~ stop s & ~ up s & floor s ~: req s}"
   110 
   111   (*This action is omitted from prior treatments, which therefore are
   112     unrealistic: nobody asks the lift to do anything!  But adding this
   113     action invalidates many of the existing progress arguments: various
   114     "ensures" properties fail.*)
   115   button_press  :: "(state*state) set"
   116     "button_press ==
   117          {(s,s'). EX n. s' = s (|req := insert n (req s)|)
   118 		        & Min <= n & n <= Max}"
   119 
   120 
   121   Lift :: state program
   122     (*for the moment, we OMIT button_press*)
   123     "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
   124 		          ~ open s & req s = {}},
   125 			 {request_act, open_act, close_act,
   126 			  req_up, req_down, move_up, move_down},
   127 			 UNIV)"
   128 
   129 
   130   (** Invariants **)
   131 
   132   bounded :: state set
   133     "bounded == {s. Min <= floor s & floor s <= Max}"
   134 
   135   open_stop :: state set
   136     "open_stop == {s. open s --> stop s}"
   137   
   138   open_move :: state set
   139     "open_move == {s. open s --> move s}"
   140   
   141   stop_floor :: state set
   142     "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
   143   
   144   moving_up :: state set
   145     "moving_up == {s. ~ stop s & up s -->
   146                    (EX f. floor s <= f & f <= Max & f : req s)}"
   147   
   148   moving_down :: state set
   149     "moving_down == {s. ~ stop s & ~ up s -->
   150                      (EX f. Min <= f & f <= floor s & f : req s)}"
   151   
   152   metric :: [int,state] => int
   153     "metric ==
   154        %n s. if floor s < n then (if up s then n - floor s
   155 			          else (floor s - Min) + (n-Min))
   156              else
   157              if n < floor s then (if up s then (Max - floor s) + (Max-n)
   158 		                  else floor s - n)
   159              else Numeral0"
   160 
   161 locale floor =
   162   fixes 
   163     n	:: int
   164   assumes
   165     Min_le_n    "Min <= n"
   166     n_le_Max    "n <= Max"
   167   defines
   168 
   169 end