module auto_pilot

type definitions

  Switch : { on, off };
  mcStatus_type : { ATTmode, ALTmode, FPAarmed, FPAunarmed };

monitored variables

  mALTcurrent : int;
  mALTdesired : int;
  mALTsw : Switch;
  mATTsw : Switch;
  mCAScurrent : int;
  mCASdesired : int;
  mCASsw : Switch;
  mFPAcurrent : int;
  mFPAdesired : int;
  mFPAsw : Switch;

controlled variables

  cALTdisplay : int;
  cCASdisplay : int;
  cFPAdisplay : int;

internal variables

  tALTpresel : bool;
  tCASmode   : bool;
  tCASpresel : bool;
  tFPApresel : bool;
  tNear      : bool;
  mcStatus   : mcStatus_type;

guarantees

  FPAdisengage =
     (@F  ( (mcStatus = FPAarmed or mcStatus = FPAunarmed) ) 
      =>
      not tFPApresel');

  ALTdisengage =
    @F  ( (mcStatus = ALTmode) )  =>  not tALTpresel'; 

definitions

  /*---- Begin modeless condition table: cALTdisplay ------------*/

  var cALTdisplay =
    if
      [] tALTpresel      -> mALTdesired
      []  not tALTpresel -> mALTcurrent
    fi

  /*---- Begin modeless condition table: cCASdisplay ------------*/

  var cCASdisplay =
    if
      [] tCASpresel     -> mCASdesired
      [] not tCASpresel -> mCAScurrent
    fi

  /*---- Begin modeless condition table: cFPAdisplay ------------*/

  var cFPAdisplay =
    if
      [] tFPApresel     -> mFPAdesired
      [] not tFPApresel -> mFPAcurrent
    fi

  /*---- Begin mode transition table: mcStatus ------------------*/

  var mcStatus initially ATTmode :=
    case mcStatus
      [] ATTmode ->
         ev
           [] ( @T  ( (mALTsw = on) )  when
               (tALTpresel and tNear)) -> ALTmode

           [] ( @T  ( (mALTsw = on) )  when
               (tALTpresel and  not tNear)) -> FPAarmed

           []  @T  ( (mFPAsw = on) )  -> FPAunarmed
         ve

      [] ALTmode ->
         ev
           []  @T  ( (mATTsw = on) )  or  @C  ( mALTdesired )  -> ATTmode

           []  @T  ( (mFPAsw = on) )  -> FPAunarmed
         ve

      [] FPAarmed ->
         ev
           []  @T  ( (mATTsw = on) )  or
               @C  ( mALTdesired )  or  @T  ( (mFPAsw = on) )  -> ATTmode

           [] ( @T  ( tNear )  with mALTdesired = mALTdesired') -> ALTmode
         ve

      [] FPAunarmed ->
         ev
           []  @T  ( (mATTsw = on) )  or  @T  ( (mFPAsw = on) )  -> ATTmode

           [] ( @T  ( (mALTsw = on) )  when
               (tALTpresel and tNear)) -> ALTmode

           [] ( @T  ( (mALTsw = on) )  when
               (tALTpresel and  not tNear)) -> FPAarmed
         ve

    esac

  /*---- Begin event table: tALTpresel --------------------------*/

  var tALTpresel initially false :=
    case mcStatus
      [] ATTmode ->
        ev
          []  @C  ( mALTdesired )  ->
              true 
          []  @T  ( (mFPAsw = on) )  ->
              false 
        ve
      [] ALTmode, FPAarmed ->
        ev
          []  never  ->
              true 
          []  @T  ( (mATTsw = on) )  or
               @T  ( (mFPAsw = on) )  or
                @C  ( mALTdesired )  or
                 @T  ( (mALTdesired = mALTcurrent) )  ->
              false 
        ve
      [] FPAunarmed ->
        ev
          []  @C  ( mALTdesired )  ->
              true 
          []  @T  ( (mATTsw = on) )  or  @T  ( (mFPAsw = on) )  ->
              false 
        ve
    esac

  /*---- Begin modeless event table: tCASmode -------------------*/

  var tCASmode initially false :=
    ev
      [] ( @T  ( (mCASsw = on) )  when  not tCASmode) ->
          true 
      [] ( @T  ( (mCASsw = on) )  when tCASmode) ->
          false 
    ve

  /*---- Begin modeless event table: tCASpresel -----------------*/

  var tCASpresel initially false :=
    ev
      [] ( @C  ( mCASdesired )  with
           mCASdesired' != mCAScurrent') ->
          true 
      [] ( @T  ( (mCASsw = on) )  when tCASmode) or
          ( @T  ( (mCASdesired = mCAScurrent) )  when tCASmode) ->
          false 
    ve

  /*---- Begin event table: tFPApresel --------------------------*/

  var tFPApresel initially false :=
    case mcStatus
      [] ATTmode ->
        ev
          []  @C  ( mFPAdesired )  ->
              true 
          [] ( @T  ( (mALTsw = on) )  when
               (tALTpresel and tNear)) ->
              false 
        ve
      [] ALTmode ->
        ev
          []  @C  ( mFPAdesired )  ->
              true 
          []  @T  ( (mATTsw = on) )  or  @C  ( mALTdesired )  ->
              false 
        ve
      [] FPAarmed ->
        ev
          [] ( @C  ( mFPAdesired )  with
               mFPAdesired' != mFPAcurrent') ->
              true 
          []  @T  ( (mATTsw = on) )  or
             @T  ( (mFPAsw = on) )  or   
                (@T  ( tNear ) with mALTdesired = mALTdesired') or
                 @C  ( mALTdesired )  or
                  @T  ( (mFPAdesired = mFPAcurrent) )  ->
              false 
        ve
      [] FPAunarmed ->
        ev
          [] ( @C  ( mFPAdesired )  with
               mFPAdesired' != mFPAcurrent') ->
              true 
          [] ( @T  ( (mALTsw = on) )  when
               (tALTpresel and tNear)) or
               @T  ( (mATTsw = on) )  or
                @T  ( (mFPAsw = on) )  or
                 @T  ( (mFPAdesired = mFPAcurrent) )  ->
              false 
        ve
    esac

  /*---- Begin modeless condition table: tNear ------------------*/

  var tNear =
    if
      [] mALTdesired - mALTcurrent <= 1200 ->
          true 
      [] mALTdesired - mALTcurrent > 1200 ->
          false 
    fi


end module // auto_pilot