Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMRT/CMRT/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 1 kB

Quellcode-Bibliothek TrafficLight.vdmrt Sprache: VDM

\section{TrafficLight Class}

\begin{vdm_al}
-----------------------------------------------
-- Class: TrafficLight
-- Description: TrafficLight the VDM project
-----------------------------------------------

--
-- class definition
--
class TrafficLight

--
-- instance variables
--
instance variables

private pos: Position;
private greenLightTime : nat1;
private greenDir: Types`Direction;
private id : nat;
--
-- Types definition section
--
types

--
-- Operations definition section
--
operations

public TrafficLight: nat * Position * nat1 ==> TrafficLight
TrafficLight(identifier ,p, t) ==
(
pos := p ;
greenLightTime := t;
id := identifier;

greenDir := <NORTH>
);

public AddTrafficData: TrafficData ==> ()
AddTrafficData(data) ==
is not yet specified;

public GetTrafficData: () ==> set of TrafficData
GetTrafficData() ==
is not yet specified;

public GetPosition: () ==> Position
GetPosition() ==
return pos;

public GreenLightPath: () ==> Types`Direction
GreenLightPath() ==
return greenDir;

pure public GetID: () ==> nat
GetID() ==
return id;

private Step: () ==> ()
Step() ==
(
    if (time mod greenLightTime) = 0
    then
    (
  greenDir := CrossDirection(greenDir);
    )
);

--
-- Functions definition section
--
functions

public static CrossDirection : Types`Direction -> Types`Direction
CrossDirection(d) ==
cases d:
<NORTH> -> <EAST>,
<SOUTH> -> <WEST>,
<EAST>  -> <NORTH>,
<WEST>  -> <SOUTH>
end;

--
-- Values definition section
--
values

--
-- Thread definition section
--
thread
periodic (1000,10,900,0) (Step)


--
-- sync definition section
--
sync
mutex(GreenLightPath);
mutex(Step,GreenLightPath);

end TrafficLight

\end{vdm_al}

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

quality85%

¤ 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.11Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.