|
\begin{vdm_al}
module PacemakerDDD
definitions
values
LRL : nat = 60; -- ppm
ARP : nat = 250; -- ms
VRP : nat = 320; -- ms
PVARP : nat = 250; -- ms
AVD : nat = 150; -- ms
VAD : nat = 850; -- ms
types
SenseTimeline = set of (Time * Chamber);
Chamber = <ATRIUM> | <VENTRICLE>;
Time = int;
Alarm = nat;
ReactionTimeline = set of (Time * Chamber);
functions
Pacemaker : Time * SenseTimeline -> ReactionTimeline
Pacemaker (t,s) == PM(mk_(1,t,s,{},1000,0,-ARP,-VRP)).#1;
PM : (Time * Time * SenseTimeline * ReactionTimeline * Alarm * Alarm * Time * Time) ->
ReactionTimeline * Alarm * Alarm * Time * Time
PM (mk_(i,t,s,r,AA,VA,LastA,LastV)) ==
if i = t
then mk_(r,AA,VA,LastA,LastV)
else if mk_(i,<ATRIUM>) in set s
then PM(c(i+1,t,s,SensedAtrium(i,r,AA,VA,LastA,LastV)))
elseif mk_(i,<VENTRICLE>) in set s
then PM(c(i+1,t,s,SensedVentricle(i,r,AA,VA,LastA,LastV)))
else PM(c(i+1,t,s,SensedNothing(i,r,AA,VA,LastA,LastV)));
SensedAtrium : Time * ReactionTimeline * Alarm * Alarm * Time * Time -> ReactionTimeline * Alarm * Alarm * Time * Time
SensedAtrium (t,r,AA,VA,LastA,LastV) ==
if t - LastA < ARP or VA > 0 or t - LastA < PVARP -- 5.4.2 or 5.4.5 or 5.4.3
then SensedNothing(t,r,AA,VA,LastA,LastV)
else mk_(r,0,t + AVD,t,LastV); -- valid sense + schedule Ventricle
SensedVentricle : Time * ReactionTimeline * Alarm * Alarm * Time * Time -> ReactionTimeline * Alarm * Alarm * Time * Time
SensedVentricle (t,r,AA,VA,LastA,LastV) ==
if t - LastV < VRP -- 5.4.3
then SensedNothing(t,r,AA,VA,LastA,LastV)
else mk_(r,t + VAD,0,LastA,t); -- valid sense + unset ventricle alarm
SensedNothing : Time * ReactionTimeline * Alarm * Alarm * Time * Time -> ReactionTimeline * Alarm * Alarm * Time * Time
SensedNothing (t, r, AA, VA,LastA,LastV) ==
if AA > 0 and t >= AA -- Atrium alarm is set and fired
then mk_(r union {mk_(t,<ATRIUM>)}, 0, t + AVD,t,LastV) -- atrial pulse + schedule ventrile
elseif VA > 0 and t >= VA -- Ventricle alarm is set and fired
then mk_(r union {mk_(t,<VENTRICLE>)}, t + VAD, 0,LastA,t) -- pulse ventricle + unset timer
else mk_(r, AA, VA,LastA,LastV); -- no alarms
-- Auxiliar funtcions
-- A curry function
c : Time * Time * SenseTimeline * (ReactionTimeline * Alarm * Alarm * Time * Time) ->
Time * Time * SenseTimeline * ReactionTimeline * Alarm * Alarm * Time * Time
c (i,t,s,mk_(r,a,v,la,lv)) == mk_(i,t,s,r,a,v,la,lv);
end PacemakerDDD
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
