| products/sources/formale Sprachen/Isabelle/HOL/SPARK/Manual/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: root.bib Sprache: VDMOriginal von: VDM© |
|
||||||
|
\section{Lead class}
The Lead models a Pacemaker lead that read and write pulse values from and to the heart. Each lead its attached to a specific chamber and this is captured using the instance variable chamber. \begin{vdm_al} class Lead is subclass of GLOBAL instance variables private chamber : Chamber; private scheduledPulse : [(Time * Pulse)]; operations public Lead: Chamber ==> Lead Lead(chm) == ( chamber := chm; scheduledPulse := nil ); \end{vdm_al} This is an auxiliar function that inspect the chamber where this lead is attached to. \begin{vdm_al} public getChamber: () ==> Chamber getChamber () == return chamber; \end{vdm_al} Whenever theres an electrical pulse in that chamber the environment will call the following stimulate operation. \begin{vdm_al} public stimulate : Sense ==> () stimulate (s) == Pacemaker`heartController.sensorNotify(s,chamber); \end{vdm_al} \begin{vdm_al} public isFinished : () ==> () isFinished () == skip; \end{vdm_al} The following operation discharges a pulse to the heart. \begin{vdm_al} public addLeadPace : Pulse * Time ==> () addLeadPace (p,t) == if t <= time then dischargePulse(p,chamber) else (scheduledPulse := mk_(t,p); return); \end{vdm_al} \begin{vdm_al} private dischargePulse : Pulse * Chamber ==> () dischargePulse (p,c) == duration(4) World`env.handleEvent(p,c,time); \end{vdm_al} \begin{vdm_al} private followPlan : () ==> () followPlan () == ( dcl curTime : Time := time; if scheduledPulse <> nil then if(curTime >= scheduledPulse.#1) then (dischargePulse(scheduledPulse.#2,chamber); scheduledPulse := nil); ); \end{vdm_al} \begin{vdm_al} thread periodic (50E6,0,49,0) (followPlan) \end{vdm_al} \begin{vdm_al} sync mutex(addLeadPace); mutex(dischargePulse); mutex(followPlan); per isFinished => scheduledPulse = nil; end Lead \end{vdm_al} ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
