| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 750 B |
|
Quellcode-Bibliothek GLOBAL.vdmpp Sprache: VDM |
|||||||||
|
\section{Global class}
This is the common parent of the other classes where the shared knowledge between all the object \begin{vdm_al} class GLOBAL types \end{vdm_al} While poling the leads either a pulse is sensed or nothing, that's modelled by the union ty \begin{vdm_al} -- Sensed activity public Sense = <NONE> | <PULSE>; \end{vdm_al} These senses are associated to the chamber where they were produced and again the uninon type is \begin{vdm_al} -- Heart chamber identifier public Chamber = <ATRIA> | <VENTRICLE>; \end{vdm_al} Diferently the output the accelerometer provides to the heart-controller is defined below consitently to the requirement analisys definition that is a linear order and \begin{vdm_al} -- Accelerometer output public ActivityData = nat1 inv a == a <= 7; \end{vdm_al} The heart controller can actuate in two different manners: either do nothing or discharge a pul \begin{vdm_al} -- Paced actvity public Pulse = <PULSE> | <TRI_PULSE>; \end{vdm_al} The operation modes are defined as a enumeration of the different quotes corresponding to each mode. \begin{vdm_al} -- Operation mode public Mode = <OFF> | <AOO> | <AOOR> | <AAT> | <DOO>; \end{vdm_al} Pulses per minute is an instance of nat1 \begin{vdm_al} -- PPM public PPM = nat1 inv ppm == ppm >= 30 and ppm <= 175; \end{vdm_al} And to promote readabillity Time is defined as nat type synonim. \begin{vdm_al} -- Time public Time = nat; end GLOBAL \end{vdm_al} ¤ 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.0.1Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28