|
\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}
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
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.
|
