1(*===========================================================================*) 2(* Autopilot Specification Example *) 3(* *) 4(* The Hol98 part of an intended comparison between PVS, ACL2 and HOL98. *) 5(* Copyright 1998, Mark Staples *) 6(* Modifications (April,June 1998) Konrad Slind. *) 7(*===========================================================================*) 8 9open HolKernel boolLib Parse bossLib 10 11(*---------------------------------------------------------------------------* 12 * We'll track information on inferences. * 13 *---------------------------------------------------------------------------*) 14 15val meter = Count.mk_meter(); 16 17 18(*---------------------------------------------------------------------------* 19 * Start the theory. * 20 *---------------------------------------------------------------------------*) 21 22val _ = new_theory "autopilot"; 23 24 25val _ = Hol_datatype `events = press_att_cws 26 | press_cas_eng 27 | press_alt_eng 28 | press_fpa_sel 29 | input_alt 30 | input_fpa 31 | input_cas 32 | alt_reached 33 | fpa_reached 34 | alt_gets_near`; 35 36 37val _ = Hol_datatype `off_eng = off | engaged`; 38 39 40val _ = Hol_datatype `mode_status 41 = armed 42 | Mode of off_eng`; 43 44 45val _ = Hol_datatype `disp_status 46 = pre_selected 47 | current`; 48 49 50val _ = Hol_datatype `altitude_vals 51 = away 52 | near_pre_selected 53 | at_pre_selected`; 54 55 56(*---------------------------------------------------------------------------* 57 * Define state-type projection and update functions. * 58 *---------------------------------------------------------------------------*) 59 60val _ = Hol_datatype `states = <| att_cws : off_eng; 61 cas_eng : off_eng; 62 fpa_sel : off_eng; 63 alt_eng : mode_status; 64 alt_disp : disp_status; 65 fpa_disp : disp_status; 66 cas_disp : disp_status; 67 altitude : altitude_vals |>`; 68 69 70(*---------------------------------------------------------------------------* 71 * State predicates. * 72 *---------------------------------------------------------------------------*) 73 74val tran_att_cws_def = 75 Define 76 `tran_att_cws st = 77 if st.att_cws = off 78 then st with 79 <| att_cws := engaged; 80 fpa_sel := off; 81 alt_eng := Mode off; 82 fpa_disp := current; 83 alt_disp := current|> 84 else st`; 85 86 87val tran_cas_eng_def = 88 Define 89 `tran_cas_eng st = 90 if st.cas_eng = off 91 then st with cas_eng := engaged 92 else (st with <|cas_disp := current; cas_eng := off|>)`; 93 94 95val tran_fpa_sel_def = 96 Define 97 `tran_fpa_sel st = 98 if st.fpa_sel = off 99 then st with 100 <| fpa_sel := engaged; 101 att_cws := off; 102 alt_eng := Mode off; 103 alt_disp := current|> 104 else (st with 105 <| fpa_sel := off; 106 fpa_disp := current; 107 att_cws := engaged; 108 alt_eng := Mode off; 109 alt_disp := current|>)`; 110 111val tran_alt_eng_def = 112 Define 113 `tran_alt_eng st = 114 if (st.alt_eng = Mode off) /\ 115 (st.alt_disp = pre_selected) 116 then (if ~(st.altitude = away) 117 then st with 118 <| att_cws := off; 119 fpa_sel := off; 120 alt_eng := Mode engaged; 121 fpa_disp := current|> 122 else (st with 123 <|att_cws := off; 124 fpa_sel := engaged; 125 alt_eng := armed|>)) 126 else st`; 127 128val tran_input_alt_def = 129 Define 130 `tran_input_alt st = 131 if st.alt_eng = Mode off 132 then st with alt_disp := pre_selected 133 else if (st.alt_eng = armed) \/ (st.alt_eng = Mode engaged) 134 then st with 135 <|alt_eng := Mode off; 136 alt_disp := pre_selected; 137 att_cws := engaged; 138 fpa_sel := off; 139 fpa_disp := current|> 140 else st`; 141 142val tran_input_fpa_def = 143 Define 144 `tran_input_fpa st = 145 if st.fpa_sel = off 146 then st with fpa_disp := pre_selected 147 else st`; 148 149 150val tran_input_cas_def = 151 Define 152 `tran_input_cas st = 153 if st.cas_eng = off then st with cas_disp := pre_selected else st`; 154 155 156val tran_alt_gets_near_def = 157 Define 158 `tran_alt_gets_near st = 159 if st.alt_eng = armed 160 then st with 161 <|altitude := near_pre_selected; 162 alt_eng := Mode engaged; 163 fpa_sel := off; 164 fpa_disp := current|> 165 else 166 (st with altitude := near_pre_selected)`; 167 168val tran_alt_reached_def = 169 Define 170 `tran_alt_reached st = 171 if st.alt_eng = armed 172 then st with 173 <|altitude := at_pre_selected; 174 alt_disp := current; 175 alt_eng := Mode engaged; 176 fpa_sel := off; 177 fpa_disp := current|> 178 else (st with <|altitude := at_pre_selected; alt_disp := current|>)`; 179 180val tran_fpa_reached_def = 181 Define 182 `tran_fpa_reached st = (st with fpa_disp := current)`; 183 184 185val tran_defs = 186 [ tran_att_cws_def, tran_alt_eng_def, tran_fpa_sel_def, tran_cas_eng_def, 187 tran_input_alt_def, tran_input_fpa_def, tran_input_cas_def, 188 tran_alt_reached_def, tran_fpa_reached_def, tran_alt_gets_near_def]; 189 190 191(*---------------------------------------------------------------------------* 192 * The transition function. * 193 *---------------------------------------------------------------------------*) 194 195val nextstate_def = 196 Define 197 `(nextstate st press_att_cws = tran_att_cws st) 198 /\ (nextstate st press_alt_eng = tran_alt_eng st) 199 /\ (nextstate st press_fpa_sel = tran_fpa_sel st) 200 /\ (nextstate st press_cas_eng = tran_cas_eng st) 201 /\ (nextstate st input_alt = tran_input_alt st) 202 /\ (nextstate st input_fpa = tran_input_fpa st) 203 /\ (nextstate st input_cas = tran_input_cas st) 204 /\ (nextstate st alt_reached = tran_alt_reached st) 205 /\ (nextstate st fpa_reached = tran_fpa_reached st) 206 /\ (nextstate st alt_gets_near = tran_alt_gets_near st)`; 207 208 209(*---------------------------------------------------------------------------* 210 * Initial state. * 211 *---------------------------------------------------------------------------*) 212 213val st0_def = 214 Define 215 `st0 = <|att_cws := engaged; 216 cas_eng := off; 217 fpa_sel := off; 218 alt_eng := Mode off; 219 alt_disp := current; 220 fpa_disp := current; 221 cas_disp := current; 222 altitude := away|>`; 223 224 225val is_initial_def = 226 Define 227 `is_initial st = 228 (st.att_cws = engaged) /\ 229 (st.cas_eng = off) /\ 230 (st.fpa_sel = off) /\ 231 (st.alt_eng = Mode off) /\ 232 (st.alt_disp = current) /\ 233 (st.fpa_disp = current) /\ 234 (st.cas_disp = current)`; 235 236 237val valid_state_def = 238 Define 239 `valid_state st = 240 ((st.att_cws = engaged) \/ (st.fpa_sel = engaged) \/ 241 (st.alt_eng = Mode engaged)) 242 /\ (~(st.alt_eng = Mode engaged) \/ ~(st.fpa_sel = engaged)) 243 /\ ((st.att_cws = engaged) 244 ==> ~(st.alt_eng = Mode engaged) /\ 245 ~(st.fpa_sel = engaged)) 246 /\ ((st.alt_eng = armed) ==> (st.fpa_sel = engaged))`; 247 248 249(*---------------------------------------------------------------------------* 250 * Proofs. First we build the simplification set. Note that standard * 251 * simplifications arising from datatype definitions get applied * 252 * automatically, and thus can be considered to be in every simplification * 253 * set. * 254 *---------------------------------------------------------------------------*) 255 256val ap_ss = std_ss && [nextstate_def, valid_state_def]; 257 258val st0_initial = prove (Term`is_initial st0`, 259 ZAP_TAC 260 (ap_ss && [is_initial_def,st0_def]) []); 261 262 263val is_initial_valid_state = prove(Term`is_initial st ==> valid_state st`, 264 ZAP_TAC 265 (ap_ss && [is_initial_def]) []); 266 267 268val st0_valid_state = prove (Term`valid_state st0`, 269 ZAP_TAC 270 (ap_ss && [is_initial_valid_state,st0_initial]) []); 271 272 273(*---------------------------------------------------------------------------* 274 * nextstate preserves valid_stateness. * 275 * It takes approx. 17 seconds of runtime on 80Meg Pentium 133Mhz. * 276 *---------------------------------------------------------------------------*) 277 278val nextstate_valid_state = 279Count.apply prove 280 (Term`!event. valid_state st ==> valid_state (nextstate st event)`, 281 Cases 282 THEN ZAP_TAC (ap_ss && tran_defs) []); 283 284 285(*---------------------------------------------------------------------------* 286 * Reachability. This could also be given as an inductive definition. * 287 *---------------------------------------------------------------------------*) 288 289val reachable_in_def = 290 Define 291 `(reachable_in 0 st = is_initial st) /\ 292 (reachable_in (SUC n) st = 293 ?pst ev. (st = nextstate pst ev) /\ reachable_in n pst)`; 294 295 296 297(*---------------------------------------------------------------------------* 298 * Every reachable state is valid. * 299 *---------------------------------------------------------------------------*) 300 301val reachable_valid_state = prove 302 (Term`!n st. reachable_in n st ==> valid_state st`, 303 Induct THEN 304 ZAP_TAC (std_ss && [reachable_in_def]) 305 [is_initial_valid_state,nextstate_valid_state]); 306 307 308(*---------------------------------------------------------------------------* 309 * A state is reachable if it is reachable in a finite number of steps. * 310 *---------------------------------------------------------------------------*) 311 312val is_reachable_def = Define `is_reachable st = ?n. reachable_in n st`; 313 314 315val is_reachable_valid_state = prove 316(Term`!st. is_reachable st ==> valid_state st`, 317 ZAP_TAC std_ss 318 [is_reachable_def,reachable_valid_state]); 319 320 321(*---------------------------------------------------------------------------* 322 * A couple of safety properties. * 323 *---------------------------------------------------------------------------*) 324 325val safety1 = store_thm( 326 "safety1", 327 ``!event st. 328 valid_state st 329 /\ (st.fpa_sel = engaged) 330 /\ ((nextstate st event).fpa_sel = off) 331 ==> 332 ((nextstate st event).fpa_disp = current)``, 333Induct 334 THEN ZAP_TAC (ap_ss && tran_defs) (tl (type_rws ``:off_eng``))); 335 336 337val safety2 = store_thm( 338 "safety2", 339 ``!event st. 340 valid_state st 341 /\ (st.alt_eng = Mode engaged) 342 /\ ~(event = input_alt) 343 /\ ((nextstate st event).alt_eng = Mode off) 344 ==> 345 ((nextstate st event).alt_disp = current)``, 346Induct 347 THEN ZAP_TAC (ap_ss && tran_defs) 348 (tl(type_rws ``:off_eng``) @ tl(type_rws ``:mode_status``))); 349 350 351(*---------------------------------------------------------------------------* 352 * Induction for reachable states. * 353 *---------------------------------------------------------------------------*) 354 355val reachable_induct = prove 356(Term`!P. (!st. is_initial st ==> P st) /\ 357 (!st e. is_reachable st ==> P (nextstate st e)) 358 ==> 359 !st. is_reachable st ==> P st`, 360 RW_TAC std_ss [is_reachable_def] 361 THEN Cases_on `n` 362 THEN PROVE_TAC [reachable_in_def]); 363 364 365val _ = Count.report (Count.read meter); 366 367val _ = export_theory() 368