Quelle test.vdmsl Sprache: VDM

\begin{vdm_al}

module TEST

imports from SAFER all,
        from HCM all,
        from TS all,
        from AUX all,
from GEOM
   operations
    InitGeom : () ==> ();
    ShowThrust : seq of seq of char ==> (),


   from GUI

    operations
      GetCommand : ()  ==> seq of seq of char;
      GUI_Init_Tcl : () ==> ()

  exports all

definitions

values

  switches_tran_up = mk_HCM`SwitchPositions(<Tran>,<Up>);

  switch_positions : set of HCM`SwitchPositions =
    {mk_HCM`SwitchPositions(mode,aah) |
       mode in set {<Tran>,<Rot>}, aah in set {<Up>,<Down>}};

  zero_grip : HCM`HandGripPosition = mk_HCM`HandGripPosition(<Zero>,<Zero>,
                                                             <Zero>,<Zero>);

  all_grip_positions : set of HCM`HandGripPosition =
    {mk_HCM`HandGripPosition(vert,horiz,trans,twist) |
     vert, horiz, trans, twist in set AUX`axis_command_set};

  all_rot_commands : set of AUX`RotCommand =
    {{<Roll> |-> a, <Pitch> |-> b, <Yaw> |-> c} |
     a, b, c in set AUX`axis_command_set};

  grip_positions : set of HCM`HandGripPosition
    =
    {mk_HCM`HandGripPosition(vert,horiz,trans,twist) |
     vert, horiz, trans, twist in set AUX`axis_command_set &
     vert = <Zero> and horiz = <Zero> and trans = <Zero> or
     vert = <Zero> and horiz = <Zero> and twist = <Zero> or
     vert = <Zero> and trans = <Zero> and twist = <Zero> or
     horiz = <Zero> and trans = <Zero> and twist = <Zero>};

  possibilities -- total of 972 cases
    : set of (HCM`SwitchPositions * HCM`HandGripPosition * AUX`RotCommand)
    =
    {mk_(switch,grip,aah_law) |
       switch in set switch_positions, grip in set grip_positions,
       aah_law in set all_rot_commands}

functions

  BigTest: () ->
    map (HCM`SwitchPositions * HCM`HandGripPosition * AUX`RotCommand) to
        TS`ThrusterSet
  BigTest() ==
    {mk_(switch,grip,aah_law) |-> SAFER`ControlCycle(switch,grip,aah_law) |
     switch in set switch_positions, grip in set grip_positions,
     aah_law in set all_rot_commands};

   HugeTest: () ->
     map (HCM`SwitchPositions * HCM`HandGripPosition * AUX`RotCommand) to
         TS`ThrusterSet
   HugeTest() ==
   {mk_(switch,grip,aah_law) |-> SAFER`ControlCycle(switch,grip,aah_law) |
    switch in set switch_positions, grip in set all_grip_positions,
    aah_law in set all_rot_commands};

  ConvertAxisCmd: seq of char -> AUX`AxisCommand
  ConvertAxisCmd(str) ==
    cases str:
      "neg" -> <Neg>,
      "pos" -> <Pos>,
      "zero" -> <Zero>,
      others -> undefined
    end;

  ConvertTIds: TS`ThrusterSet +> seq of seq of char
  ConvertTIds(ts) ==
    if ts = {}
    then []
    else let t in set ts
         in
    [ConvertTId(t)]^ ConvertTIds(ts\{t});

  ConvertTId: TS`ThrusterName +> seq of char
  ConvertTId(tnm) ==
    cases tnm:
       <B1>  -> "B1",
       <B2>  -> "B2",
       <B3>  -> "B3",
       <B4>  -> "B4",
       <F1>  -> "F1",
       <F2>  -> "F2",
       <F3>  -> "F3",
       <F4>  -> "F4",
       <L1R> -> "L1R",
       <L1F> -> "L1F",
       <R2R> -> "R2R",
       <R2F> -> "R2F",
       <L3R> -> "L3R",
       <L3F> -> "L3F",
       <R4R> -> "R4R",
       <R4F> -> "R4F",
       <D1R> -> "D1R",
       <D1F> -> "D1F",
       <D2R> -> "D2R",
       <D2F> -> "D2F",
       <U3R> -> "U3R",
       <U3F> -> "U3F",
       <U4R> -> "U4R",
       <U4F> -> "U4F"
     end;

operations

  StartTest: () ==> ()
  StartTest() == ( GUI`GUI_Init_Tcl();
                   GEOM`InitGeom() );

  RunTest: () ==> bool
  RunTest() ==
   let cl = GUI`GetCommand()
   in
     if cl = []
     then return false
     else let [mode,aah,horiz,trans,vert,twist,roll,pitch,yaw] = cl,
              ts = SAFER`ControlCycle(
                    mk_HCM`SwitchPositions(
                     if mode = "translation" then <Tran> else <Rot>,
                     if aah = "1" then <Up> else <Down> ),
                   mk_HCM`HandGripPosition(ConvertAxisCmd(vert),
                                           ConvertAxisCmd(horiz),
                      ConvertAxisCmd(trans),ConvertAxisCmd(twist)),
                   {<Roll> |-> ConvertAxisCmd(roll),
                    <Pitch> |-> ConvertAxisCmd(pitch),
                    <Yaw> |-> ConvertAxisCmd(yaw)})
  in
    (GEOM`ShowThrust(ConvertTIds(ts));
            return true );


  Loop : () ==> ()
  Loop() ==
  (
    StartTest();
    while RunTest() do skip;
    GEOM`ShowThrust(["stop"])
  );

  Move: () ==> ()
  Move() ==
   GEOM`ShowThrust(["move"]);

  NoMove: () ==> ()
  NoMove() ==
   GEOM`ShowThrust(["nomove"]);

end TEST

\end{vdm_al}
\stopline

\newpage
\section*{Test Coverage}

\begin{rtinfo}{safer.vdm.ts}
\end{rtinfo}

quality97%

¤ Dauer der Verarbeitung: 0.1 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.