products/Sources/formale Sprachen/VDM/VDMRT/PacemakerRT image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: RateController.vdmrt   Sprache: VDM

Original von: VDM©

\section{RateController class}

The RateController is the class that models the rate adaptation control.

\begin{vdm_al}
class RateController is subclass of GLOBAL

instance variables
 rateplan : map Time to Time;
 sensed   : [ActivityData];
 interval : Time;
 finished : bool;

 
\end{vdm_al}

\begin{vdm_al}
instance variables
-- programmable values
 LRL       : PPM;
 MSR       : PPM;
 threshold : nat1;
 reactionT : Time;
 recoveryT : Time;
 responseF : nat1;

inv threshold < 8
    and
    reactionT in set {10,...,50}
    and
    recoveryT in set {2,...,16}
    and 
    responseF <= 16;
\end{vdm_al} 

The Constructor initializes the instance variables with the 
default values as consulted in (citation needed);

\begin{vdm_al}
operations
  
 public 
 RateController: () ==> RateController
 RateController() ==
   (LRL       := 60;
    MSR       := 120;
    threshold := MED;
    reactionT := 10; -- 10 s
    recoveryT := 2; -- 2 minutes;
    responseF := 8;
    sensed    := nil
    interval  := 1/((LRL/60)/10000);
    finished  := false;

   );
\end{vdm_al} 

\begin{vdm_al}
public
getInterval : () ==> Time
getInterval () == return interval;
\end{vdm_al}


\begin{vdm_al}
 private
 controlRate : () ==> ()
 controlRate () == 
    (
    (if sensed > threshold
     then increaseRate()
     elseif sensed < threshold
     then decreaseRate()
     else skip;
     );
    sensed := nil;
    );
\end{vdm_al}

\begin{vdm_al}

 public 
 stimulate : ActivityData ==> ()
 stimulate (ad) == sensed := ad;
\end{vdm_al} 


\begin{vdm_al}
 public
 increaseRate : () ==> ()
 increaseRate () == 
   (
    interval := 1 / ((MSR / 60) / 10000);
    Pacemaker`heartController.setInterval(interval)
   );

\end{vdm_al}

\begin{vdm_al}
 public
 decreaseRate : () ==> ()
 decreaseRate () == 
   (
    interval := 1 / ((LRL / 60) / 10000);
    Pacemaker`heartController.setInterval(interval)
   );
\end{vdm_al}

\begin{vdm_al}
 public 
 finish : () ==> ()
 finish () == finished := true

 public 
 isFinished : () ==> ()
 isFinished () == skip
\end{vdm_al}

\begin{vdm_al}

thread
 while true do
    controlRate();
    

sync
mutex(stimulate);

per isFinished => finished;

per controlRate => sensed <> nil;
\end{vdm_al} 

\begin{vdm_al}
values

--V-LOW 1
--LOW 2
--MED-LOW 4
MED : ActivityData = 4;
--MED-HIGH 4
--HIGH 6
--V-HIGH 6

end RateController
\end{vdm_al} 

¤ Dauer der Verarbeitung: 0.15 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

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.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff