Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMPP/PacemakerConcPP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 2 kB

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.15 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.