Quelle RateController.vdmpp Sprache: VDM

\section{RateController class}

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

\begin{vdm_al}
class RateController is subclass of GLOBAL, BaseThread

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: nat1 * bool ==> RateController
RateController(p, isP) ==
   (LRL       := 60;
    MSR       := 120;
    threshold := MED;
    reactionT := 10; -- 10 s
    recoveryT := 2; -- 2 minutes;
    responseF := 8;
    sensed    := nil;
    interval  := 1/((LRL/60)/1000);
    finished  := false;
    period := p;
    isPeriodic := isP;
   );
\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}
private
increaseRate : () ==> ()
increaseRate () ==
   (
    interval := 1 / ((MSR / 60) / 1000);
    Pacemaker`heartController.SetPeriod(interval); --setInterval(interval)
   );

\end{vdm_al}

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

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

public
isFinished : () ==> ()
isFinished () == skip;

public Step: () ==> ()
Step() ==
  if (sensed <> nil)
  then controlRate();

\end{vdm_al}

The usual Step by thread substitution is done in the RateController class.
\begin{vdm_al}

--thread
-- while true do
--    controlRate();
\end{vdm_al}

And syncronization is added.

\begin{vdm_al}

sync
mutex(stimulate);

mutex(increaseRate,decreaseRate,getInterval);

per isFinished => finished;

mutex(Step);
--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}

quality98%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.