-- Comment to force html into preformatted mode <pre>
Type
	pitch_modes: enum {vert_speed, ias, alt_cap, alt_hold};
Var
  pitch_mode: pitch_modes;
  capture_armed: boolean;
  ideal_capture: boolean;

startstate
begin
  clear pitch_mode;
  capture_armed := false;
  ideal_capture := false;
end;

rule "ALT CAPTURE"
begin
  capture_armed := !capture_armed;
  ideal_capture := !ideal_capture;
end;

rule "HLD" 
begin
  pitch_mode := alt_hold;
  capture_armed := false;
end;

rule "IAS" 
begin
  pitch_mode := ias; 
end;

rule "VSPD" 
begin
  pitch_mode := vert_speed; 
end;

rule "near"
begin
  if capture_armed then
--    capture_armed := false;
    pitch_mode := alt_cap; 
  endif;
end;

rule "arrived"
begin
--  if pitch_mode = alt_cap then
--    pitch_mode := alt_hold;
--  endif;
  if capture_armed then
    pitch_mode := alt_hold;
    capture_armed := false;
  endif;
  if ideal_capture then
    ideal_capture := false;
  endif;
end;

invariant (ideal_capture = (capture_armed | pitch_mode = alt_cap));