-- handleEvent receives the responses from the system -- and checks whether the response time for the matching -- stimulus was less than or equal to 10000 time units protected handleEvent: Event ==> ()
handleEvent (pev) == duration (0) logSysToEnv(pev.getEvent()) post checkResponseTimes(e2s,s2e,10000);
-- createSignal generates the stimuli for the system
createSignal: () ==> ()
createSignal () == duration (0) if (carddom e2s < max_stimuli) then
( dcl num : nat := getNum();
logEnvToSys(num);
raiseInterrupt("HandleTMC", num) );
-- start the thread of the task public Run: () ==> ()
Run () == start(self)
thread periodic (1000,0,0,0) (createSignal)
end TransmitTMC
\end{vdm_al}
¤ 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.0.13Bemerkung:
(vorverarbeitet)
¤
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.