\section{class Interface}

\begin{vdm_al}
class Interface

instance variables
  ws : WorkSpace := new WorkSpace() 

types 

public
Input = seq of nat
inv inp == len inp = 9;

public
ThrusterMatrix = seq of seq of bool
inv tm == len tm = 4 and forall i in set inds tm & len tm(i) = 6

operations

public
SetupTopology: () ==> ()
SetupTopology () ==
  ws.SetupTopology();

public
RunControlCycle: Input ==> ThrusterMatrix
RunControlCycle (inp) ==
  let mk_(x,p,y,z,m,ab,ah) = TransformInput (inp) in
  let ts = ws.ControlCycle (x,p,y,z,m,ab,ah) in
  return GenerateThrusterMatrix (ts);

functions

TransformInput: Input -> Command`Direction * Command`Direction *
                 Command`Direction * Command`Direction * 
                 HandControlUnit`Mode * HandControlUnit`Button * 
                 Command`AxisMap 
TransformInput (inp) ==
  let [mode,aah,horiz,trans,vert,twist,roll,pitch,yaw] = inp in
   mk_( ConvertAxisCmd(horiz), 
   ConvertAxisCmd(twist),
   ConvertAxisCmd(trans),
   ConvertAxisCmd(vert),
   if mode = 1 then <Tran> else <Rot>,
   if aah = 0 then <Up> else <Down>,
   { <axis3> |-> ConvertAxisCmd(roll), 
         <axis1> |-> ConvertAxisCmd(pitch),
          <axis2> |-> ConvertAxisCmd(yaw) } );

ConvertAxisCmd: nat -> Command`Direction
ConvertAxisCmd(n) ==
  cases n:
    0 -> <Neg>,
    1 -> <Pos>,
    2 -> <Zero>,
    others -> undefined
  end;

GenerateThrusterMatrix: set of ThrusterControl`ThrusterPosition +> 
                        ThrusterMatrix
GenerateThrusterMatrix (ts) ==
  let tson = { GenerateThrusterLabel (t) | t in set ts } in
  [ [ mk_(j,i) in set tson | i in set {1,...,6} ]
    | j in set {1,...,4} ];

GenerateThrusterLabel: ThrusterControl`ThrusterPosition +> nat * nat
GenerateThrusterLabel (tnm) ==
  cases tnm:
     <B1>  -> mk_(1,4),
     <B2>  -> mk_(2,4),
     <B3>  -> mk_(4,4),
     <B4>  -> mk_(3,4),
     <F1>  -> mk_(1,1),
     <F2>  -> mk_(2,1),
     <F3>  -> mk_(4,1),
     <F4>  -> mk_(3,1),
     <L1R> -> mk_(1,2),
     <L1F> -> mk_(1,3),
     <R2R> -> mk_(2,2),
     <R2F> -> mk_(2,3),
     <L3R> -> mk_(4,2),
     <L3F> -> mk_(4,3),
     <R4R> -> mk_(3,2),
     <R4F> -> mk_(3,3),
     <D1R> -> mk_(1,6),
     <D1F> -> mk_(1,5),
     <D2R> -> mk_(2,6),
     <D2F> -> mk_(2,5),
     <U3R> -> mk_(4,6),
     <U3F> -> mk_(4,5),
     <U4R> -> mk_(3,6),
     <U4F> -> mk_(3,5)
   end;

values

thrusters = mk_(<Pos>,<Zero>,<Zero>,<Zero>,<Tran>,<Down>,
                { <Roll> |-> <Zero>, <Pitch> |-> <Zero>, <Yaw> |-> <Zero> })

end Interface
\end{vdm_al}

\begin{rtinfo}{vdm.tc}[Interface]
\end{rtinfo}