Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/LibreOffice/external/curl/   (LibreOffice Version 25.8.3.2©)  Datei vom 5.10.2025 mit Größe 1 kB image not shown  

Quelle  World.vdmpp  Sprache: unbekannt

 
\section{World class}

The World class as its name tell is the class modelling the world where the system and environment will co-exist.

\begin{vdm_al}
class World is subclass of GLOBAL

types

instance variables

public static env      : [Environment] := nil;
public static timerRef : Timer := new Timer();
\end{vdm_al}

The World constructor its the responsible for connect system and environment, and its invoked with a scenario and a mode to test.

\begin{vdm_al}
operations

public World: seq of char * Mode ==> World
World(filename,mode) == 
  (  -- create an environment
     env := new Environment(filename);

     -- bind leads to the environment
     env.addLeadSensor(Pacemaker`atriaLead);
     env.addLeadSensor(Pacemaker`ventricleLead);
   
     -- bind accelerometer to the environment
     env.addAccelerometer(Pacemaker`accelerometer);
    
     -- bind leads to the controler
     Pacemaker`heartController.addLeadPacer(Pacemaker`atriaLead);
     Pacemaker`heartController.addLeadPacer(Pacemaker`ventricleLead);
    
     -- set up mode
     Pacemaker`heartController.setMode(mode);
  );
\end{vdm_al}

And Run is the operation that starts a test sequence.

\begin{vdm_al}
public Run: () ==> ()
Run () == (env.Run(); env.showResult());
  

end World
\end{vdm_al}

\subsection*{Test coverage}

\begin{rtinfo}
{tc.info}[World]
\end{rtinfo}

Messung V0.5 in Prozent
C=92 H=96 G=93

[Dauer der Verarbeitung: 0.9 Sekunden, vorverarbeitet 2026-09-27]