The environment classis the class responsible for read a file containing inputs labelled bytimeand deliver them to the correct system sensor at the right time. It also collects the (re)actions from the systemand provides functionality to enable the inspection of them.
The starting point is the definition of the typesfor input and output.
\begin{vdm_al} class Environment issubclassof GLOBAL
types
public InputTP = (Time * seqof Inpline) inv inp == forall line insetelems inp.#2 & inp.#1 >= line.#4;
public Inpline = (Sense * Chamber * ActivityData * Time);
public Outline = (Pulse * Chamber * Time);
\end{vdm_al}
Then the io abstraction is defined as an instance variable of the VDM IO library, and the input and output variables are defined.
Also a boolean flag indicating that the environment is still sending stimuli to the environmet called busy is defined, and simtime represents the amount oftime we want to simulate.
\begin{vdm_al} instancevariables -- Environment
busy : bool := true;
-- Amount of time we want to simulate
simtime : Time;
\end{vdm_al}
Then we define the sensors attachment place where the ``physician will screw'' the leads and where the accelerometer isset up.
\begin{vdm_al} instancevariables -- Sensors
-- Leads
leads : map Chamber to Lead := {|->};
-- Accelerometer
accelerometer : Accelerometer;
\end{vdm_al}
The environment constructor reads the test file which name is provided in the variable fname, extracting the amount oftime we want to simulate and the inputs in that amount oftime.
Run is the main operation, starting a session ofsystem stimulation controlling the timeandsystem execution invoking the Step operation on the system components.
\begin{vdm_al}
public
Run: () ==> ()
Run () ==
( whilenot (isFinished() and
Pacemaker`heartController.isFinished() and
World`timerRef.GetTime() > simtime) do
(
createSignal();
Pacemaker`rateController.Step();
Pacemaker`heartController.Step();
World`timerRef.StepTime();
);
);
\end{vdm_al}
The createSignal operation delivers stimuli to the different components
choosing between all the inputs the ones that should be delivered at the current time.
\begin{vdm_al}
private
createSignal : () ==> ()
createSignal () ==
( iflen inplines > 0 then (dcl curtime : Time := World`timerRef.GetTime(),
done : bool := false; whilenot done do let mk_(sensed,chamber,accinfo,stime) = hd inplines inif stime <= curtime then
(
leads(chamber).stimulate(sensed);
accelerometer.stimulate(accinfo);
inplines := tl inplines;
done := len inplines = 0
) else done := true
); iflen inplines = 0 then busy := false;
);
\end{vdm_al}
The (re)actions from the pacemaker are delivered to the environment through the handleEvent operation which updates the collection of outputs.
\begin{vdm_al}
public
handleEvent : Pulse * Chamber * Time ==> ()
handleEvent(p,c,t) == outlines := outlines ^ [mk_(p,c,t)];
\end{vdm_al}
ShowResult is an operation used to inspect the output collection.
