|
\section{HeartController class}
This is the core class monitoring and regulating the heart.
\begin{vdm_al}
class HeartController is subclass of GLOBAL, BaseThread
instance variables
leads : map Chamber to Lead;
sensed : map Chamber to Sense;
mode : Mode;
finished : bool;
FixedAV : Time;
lastpulse : Time;
ARP : Time;
interval : Time;
\end{vdm_al}
\begin{vdm_al}
operations
public
HeartController : nat1 * bool ==> HeartController
HeartController(p, isP) ==
(
leads := {|->};
sensed := {|->};
mode := <DOO>;
finished := false;
FixedAV := 150;
lastpulse := 0;
ARP := 250;
interval:= Pacemaker`rateController.getInterval();
period := p;
isPeriodic := isP;
);
\end{vdm_al}
\begin{vdm_al}
public
addLeadPacer : Lead ==> ()
addLeadPacer (lead) ==
leads := leads ++ {lead.getChamber() |-> lead};
\end{vdm_al}
\begin{vdm_al}
public
pace : () ==> ()
pace () ==
(cases mode :
<AOO> -> PaceAOO(),
<AAT> -> PaceAAT(),
<DOO> -> PaceDOO(),
<OFF> -> skip,
others -> error
end;
sensed := {|->}
);
\end{vdm_al}
AOO mode.
\begin{vdm_al}
private
PaceAOO : () ==> ()
PaceAOO () ==
let curTime : Time = World`timerRef.GetTime()
in if (interval + lastpulse <= curTime)
then (
lastpulse := curTime;
leads(<ATRIA>).addLeadPace(<PULSE>,curTime)
)
else skip
;
\end{vdm_al}
AAT mode.
\begin{vdm_al}
private
PaceAAT : () ==> ()
PaceAAT () ==
let curTime : Time = World`timerRef.GetTime()
in if <ATRIA> in set dom sensed and sensed(<ATRIA>) = <PULSE>
then if curTime - lastpulse <= ARP
then skip
else (
lastpulse := curTime;
leads(<ATRIA>).addLeadPace(<TRI_PULSE>,curTime)
)
elseif (interval + lastpulse <= curTime)
then (
lastpulse := curTime;
leads(<ATRIA>).addLeadPace(<PULSE>,curTime)
)
else skip
;
\end{vdm_al}
DOO mode.
\begin{vdm_al}
private
PaceDOO : () ==> ()
PaceDOO () ==
let curTime : Time = World`timerRef.GetTime()
in (if (interval + lastpulse <= curTime)
then (
lastpulse := curTime;
leads(<ATRIA>).addLeadPace(<PULSE>,curTime);
leads(<VENTRICLE>).addLeadPace(<PULSE>,FixedAV + curTime)
)
else skip;
)
;
\end{vdm_al}
\begin{vdm_al}
public
finish : () ==> ()
finish () == finished := true;
public
isFinished : () ==> ()
isFinished () == for all lead in set rng leads do
lead.isFinished();
\end{vdm_al}
\begin{vdm_al}
public
sensorNotify : Sense * Chamber ==> ()
sensorNotify (s,c) ==
(sensed := sensed ++ {c |-> s});
\end{vdm_al}
\begin{vdm_al}
public
setInterval : Time ==> ()
setInterval (t) == interval := t;
\end{vdm_al}
To switch the operating modes one should use
\begin{vdm_al}
public
setMode : Mode ==> ()
setMode (m) ==
(mode := m);
public Step: () ==> ()
Step() ==
pace();
\end{vdm_al}
The changes in this class are the Step function that is transformed to a thread
\begin{vdm_al}
--thread
-- (while true do
-- (
-- pace();
-- World`timerRef.WaitRelative(interval);
-- );
-- );
\end{vdm_al}
And the introduction of syncronization primitives. A mutex to the functions that access and write the sensed variable and isFinished.
\begin{vdm_al}
sync
per isFinished => sensed = {|->} and finished;
mutex(sensorNotify,pace);
end HeartController
\end{vdm_al}
[ zur Elbe Produktseite wechseln0.20Quellennavigators
Analyse erneut starten
]
|
