|
\begin{vdm_al}
class InsertAddress is subclass of EnvironmentTask
operations
public InsertAddress: EventDispatcher * nat ==> InsertAddress
InsertAddress (ped, pno) == EnvironmentTask("InsertAddress", ped, pno);
-- handleEvent receives the responses from the system
-- and checks whether the response time for the matching
-- stimulus was less than or equal to 2000 time units
protected handleEvent: Event ==> ()
handleEvent (pev) == duration (0) logSysToEnv(pev.getEvent());
-- post checkResponseTimes(e2s,s2e,6000);
-- createSignal generates the stimuli for the system
createSignal: () ==> ()
createSignal () ==
duration (0)
if (card dom e2s < max_stimuli) then
( dcl num : nat := getNum();
logEnvToSys(num);
raiseInterrupt("HandleKeyPress", num) );
-- start the thread of the task
public Run: () ==> ()
Run () == start(self)
thread
periodic (1000,0,0,0) (createSignal)
end InsertAddress
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
