Quelle hcm.vdmsl Sprache: VDM

\begin{vdm_al}

module HCM

imports from AUX all

exports all

definitions

types

  SwitchPositions ::
    mode: ControlModeSwitch
    aah : ControlButton;

  ControlModeSwitch = <Rot> | <Tran>;

  ControlButton = <Up> | <Down>;

  HandGripPosition:: vert  : AUX`AxisCommand
                     horiz : AUX`AxisCommand
                     trans : AUX`AxisCommand
                     twist : AUX`AxisCommand

-- add inv to exclude impossible combinations???

functions

  GripCommand: HandGripPosition * ControlModeSwitch +> AUX`SixDofCommand
  GripCommand(mk_HandGripPosition(vert,horiz,trans,twist),mode) ==
    let tran = {<X>    |-> horiz,
                <Y>    |-> if mode = <Tran> then trans else <Zero>,
                <Z>    |-> if mode = <Tran> then vert else <Zero>},
        rot  = {<Roll> |-> if mode = <Rot> then vert else <Zero>,
                <Pitch>|-> twist,
                <Yaw>  |->  if mode = <Rot> then trans else <Zero>}
    in
      mk_AUX`SixDofCommand(tran,rot)

end HCM

\end{vdm_al}

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.