|
\begin{vdm_al}
class Actuator is subclass of IIOSSTYPES
instance variables
actuatorID : nat;
operations
public Actuator: (nat) ==> Actuator
Actuator(actID) ==
(
actuatorID := actID;
return self;
);
public SetValues : EventId * PigPosition ==> ()
SetValues(eventId, val) ==
(
-- eventID, eventType, text, eventTime
World`env.handleEvent(eventId, <SHOW_PIG>,
" PigPosition " ^ VDMUtil`val2seq_of_char[PigPosition](val),
time);
);
sync
mutex(SetValues);
end Actuator
\end{vdm_al}
\begin{rtinfo}
[TotalxCoverage]{vdm.tc}[Actuator]
\end{rtinfo}
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
