| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMSL/pacemakerSL/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 3 kB |
|
Quelle PacemakerDDD.vdmsl Sprache: VDM |
|||||||||
|
\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 * 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 * Ala 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 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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28