| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle ValveDriveAssembly.vdmpp Sprache: VDM |
|||||||||
|
\section{ValveDriveAssembly Class}
\begin{vdm_al} class ValveDriveAssembly instance variables thrusters : map ThrusterControl`ThrusterPosition to Thruster := {thr |-> new Thruster() | thr in set ThrusterControl`ThrusterSet}; operations public UpdateThrusters : set of ThrusterControl`ThrusterPosition ==> () UpdateThrusters(selected) == (for all a in set selected do thrusters(a).SetOn(); for all a in set ThrusterControl`ThrusterSet\selected do thrusters(a).SetOff()); public ThrustersOn : () ==> set of ThrusterControl`ThrusterPosition ThrustersOn() == return {thr | thr in set ThrusterControl`ThrusterSet & thrusters(thr).GetState() = <On>} end ValveDriveAssembly \end{vdm_al} The test coverage table for the ValveDriveAssembly class looks like: \begin{rtinfo}{vdm.tc}[ValveDriveAssembly] \end{rtinfo} ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28