Quelle Controller.vdmrt Sprache: VDM

\section{Controller Class}

\begin{vdm_al}
-----------------------------------------------
-- Class: Controller
-- Description: Controller is main class in
-- every independent VeMo unit
-----------------------------------------------

--
-- class definition
--
class Controller

--
-- instance variables
--
instance variables
-- traffic data issued by this controller, that will be passed on
-- other controllers.
private internalTrafficData : seq of TrafficData := [];
inv len internalTrafficData <=  Config`TrafficDataKeeptNumber;
-- traffic data from other controllers moving in the opposite direction,
private externalTrafficData : seq of TrafficData := [];
-- this will not be passes on as it makes no sense with the current
-- warning types.
inv len externalTrafficData <= Config`TrafficDataKeeptNumber;

--keep track of whom we have communicated with.
private communicatedWith : seq of nat := [];
inv len communicatedWith <= Config`TrafficDataKeeptNumber;

private traffic : Traffic;
-- the vehicle the VeMo system Controller is placed in.
private vemoVehicle : Vehicle;

private canRun : bool := true;
--
-- Types definition section
--
types

--
-- Operations definition section
--
operations

public Controller : Vehicle ==> Controller
Controller (vehicle) ==
(
vemoVehicle := vehicle;
traffic := new Traffic();
);

async public AddOncomingVehicle: VehicleData ==> ()
AddOncomingVehicle(vd) ==
(
if not traffic.ExistVehicleData(vd)
then
let v = new Vehicle(vd) in
traffic.AddVehicle(v);
);

public AddTrafficData:  nat * seq of TrafficData ==> ()
AddTrafficData(vemoUnitID, data) ==
(
--we cant use empty data
if data = []
then
return;

--did we already exchange information?
if vemoUnitID in set elems communicatedWith
then
return;

--keep track of who we have communicated with
if len communicatedWith < Config`TrafficDataKeeptNumber
then
communicatedWith := communicatedWith ^ [vemoUnitID]
else
communicatedWith := tl communicatedWith ^ [vemoUnitID];

-- add traffic
if(len externalTrafficData < Config`TrafficDataKeeptNumber)
then
externalTrafficData := externalTrafficData ^ data
else
externalTrafficData :=  tl externalTrafficData ^ data;

for d in data do
(
  World`env.handleEvent("Vehicle: " ^ Printer`natToString(GetVehicleID()) ^
       " received " ^  d.ToString());
);

VeMoController`graphics.receivedMessage(GetVehicleID());
);

private AddInternalTrafficData: TrafficData ==> ()
AddInternalTrafficData(data) ==
(
if(len internalTrafficData < Config`TrafficDataKeeptNumber)
then
internalTrafficData := internalTrafficData ^ [data]
else
internalTrafficData :=  tl internalTrafficData ^ [data];
);

public GetTrafficData: () ==> [seq of TrafficData]
GetTrafficData() ==
-- deep copy
return [ new TrafficData(internalTrafficData(i).GetMessage(),
       internalTrafficData(i).GetPosition(),
        internalTrafficData(i).GetDirection())
      | i in set inds internalTrafficData ];


pure public GetVehicleID : () ==> nat
GetVehicleID()== return vemoVehicle.GetID();

pure public GetPosition : () ==> [Position]
GetPosition() ==
return vemoVehicle.GetPosition();

pure public GetDirection: () ==> [Types`Direction]
GetDirection() ==
return vemoVehicle.GetDirection();

public getVehicle : () ==> [Vehicle]
getVehicle() ==
return  vemoVehicle;

public getVehicleDTO : () ==> [VehicleData]
getVehicleDTO() == vemoVehicle.getDTO();

public EnvironmentReady: () ==> ()
EnvironmentReady() == if(canRun = false) then canRun := true;

public Step: () ==> ()
Step() ==
(
  vemoVehicle.Move();

--check expired internal data
for all td in set elems internalTrafficData do
(
  if td.Expired()
  then
  (
  --remove td
  internalTrafficData := [internalTrafficData(i)
       | i in set inds internalTrafficData
       & internalTrafficData(i) <> td];
  )
);

--check for lowgrip, and check if already set at position.
if vemoVehicle.getLowGrip() = true
then
(
--The position check will only be relevant if the car has speed 0
if vemoVehicle.GetSpeed() = 0 =>
not exists data in set elems internalTrafficData
     & Position`Compare(data.GetPosition(), GetPosition()) and
                data.GetPosition() <>  GetPosition()and
                data.GetMessage() = <LowGrip>
then
let lowGripMsg = new TrafficData(<LowGrip>, GetPosition().deepCopy()
          , GetDirection())
in
AddInternalTrafficData(lowGripMsg);
);

--check for turnindicator, and check if already set at position.
if vemoVehicle.TurnIndicator() = <LEFT>
then
(
--The position check will only be relevant if the car has speed 0
if vemoVehicle.GetSpeed() = 0 =>
not exists data in set elems internalTrafficData
     & Position`Compare(data.GetPosition(), GetPosition())
     and  data.GetMessage() = <LeftTurn>
then
let turnMsg = new TrafficData(<LeftTurn>, GetPosition().deepCopy()
         ,GetDirection())
in
AddInternalTrafficData(turnMsg);
);

  --check for congestion, and check if already set at position.
if traffic.Congestion() = true
then
(
--The position check will only be relevant if the car has speed 0
if vemoVehicle.GetSpeed() = 0 =>
not exists data in set elems internalTrafficData
     & Position`Compare(data.GetPosition(), GetPosition())
       and  data.GetMessage() = <Congestion>
  then
  (
  let congMsg = new TrafficData(<Congestion>, GetPosition().deepCopy()
          , GetDirection())
   in
   (
    AddInternalTrafficData(congMsg);
   )
  )
);

);

async public run : () ==> ()
run() == start(self)

--
-- Functions definition section
--
functions

--
-- Values definition section
--
values

--
-- Thread definition section
--
thread
while true do
duration(500)
(
  Step();
  canRun := false;
)

--
-- sync definition section
--
sync
per Step => canRun;
mutex(AddInternalTrafficData,GetTrafficData);
mutex(AddInternalTrafficData);
mutex(Step)

end Controller

\end{vdm_al}

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

quality96%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.