products/sources/formale Sprachen/VDM/VDMRT/VDMRT image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: TrafficData.vdmrt   Sprache: VDM

Original von: VDM©

\section{TrafficData Class}


\begin{vdm_al}
-----------------------------------------------
-- Class: TrafficData
-- Description:  TrafficData is the base for different types of 
-- messages in the system.
-----------------------------------------------

--
-- class definition
--
class TrafficData

--
-- instance variables
--
instance variables
private dir: Types`Direction;
private pos: Position;
private message: MessageType;
private timeToLive : nat;

--
-- Types definition section
--
types   
public MessageType = <LowGrip> | <Congestion> | <LeftTurn> | <RedLight>;

--
-- Operations definition section
--
operations
public TrafficData: MessageType * Position * Types`Direction ==> TrafficData
 TrafficData(m,p,d) ==
  (
  pos := p ;
  message := m;
  dir := d;
  timeToLive := time + Config`TrafficDataLifeTime;
  );

public GetPosition: () ==> Position 
 GetPosition() ==
 return pos;
 
public GetMessage: () ==> MessageType
 GetMessage() ==
 return message;

public GetDirection: () ==> Types`Direction 
GetDirection() ==
return dir;
 
public Expired : () ==> bool
Expired() ==
return time >= timeToLive;

public ToString : () ==> seq of char 
ToString() ==
return "traffic data reporting " 
  ^ MessageTypeToString(message) 
  ^ " moved " ^ Types`DirectionToString(dir) 
  ^ " at " ^ pos.toString()  
  ^ " with lifetime " 
  ^ Printer`intToString(timeToLive - time);

--
-- Functions definition section
--
functions

public static MessageTypeToString : MessageType -> seq of char 
MessageTypeToString(m) ==
(
cases m:
<LowGrip>-> "Low Grip",
<Congestion>-> "Congestion ",
<LeftTurn>-> "Left Turn",
<RedLight> -> "Red Light"
end
)

--
-- Values definition section
--
values

end TrafficData


\end{vdm_al}

\begin{rtinfo}
[TotalxCoverage]{vdm.tc}[TrafficData]
\end{rtinfo}

¤ Dauer der Verarbeitung: 0.4 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff