| products/sources/formale sprachen/VDM/VDMSL/SAFERSL/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Lqa.v Sprache: VDMOriginal von: 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} ¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
