Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: webserver.vdmpp Sprache: VDM

Original von: VDM^©

\section{VeMoController Class}

\begin{vdm_al}
-----------------------------------------------
-- Class: VeMoController
-- Description: VeMoController main controller for the VeMo system
-----------------------------------------------

--
-- class definition
--
class VeMoController

--
-- instance variables
--
instance variables
public ctrlUnits : inmap nat to Controller := {|->};
public lights : inmap nat to TrafficLight := {|->};
inv dom ctrlUnits inter dom lights = {};
inv forall id in set dom ctrlUnits & ctrlUnits(id).GetVehicleID() = id;
inv forall id in set dom lights & lights(id).GetID() = id;

--graphics
public static graphics : gui_Graphics := new gui_Graphics();

static env : Environment := World`env;

--
-- Types definition section
--
types

--
-- Operations definition section
--
operations

public VeMoController : () ==> VeMoController
VeMoController () ==
(
    graphics.init();
);

public addController: Controller ==> ()
addController(ctrl) ==
(
ctrlUnits := ctrlUnits munion {ctrl.GetVehicleID() |->  ctrl} ;

    let vecID = ctrl.GetVehicleID() in
    (
       graphics.addVehicle(vecID);

       let pos = ctrl.GetPosition() in
       graphics.updatePosition(vecID, pos.X(), pos.Y());

       let dir = ctrl.GetDirection() in
       graphics.updateDirection(
                                vecID,
                                Types`DirectionToGraphics(dir)
                                );

       for all unit in set rng ctrlUnits do
       graphics.connectVehicles(unit.GetVehicleID() ,vecID);
    )
)
pre ctrl.GetVehicleID() not in set (dom ctrlUnits union dom lights);
--and ctrl not in set dom controllerConnections;

public addTrafficLight: TrafficLight ==> ()
addTrafficLight(light) ==
(
    lights := lights munion {light.GetID() |-> light};
)
pre light.GetID() not in set dom lights
      and light.GetID() not in set dom ctrlUnits;

public getController : nat ==> Controller
getController(id) ==
(
  return ctrlUnits(id);
)
pre id in set dom ctrlUnits;

public getTrafficLight : nat ==> TrafficLight
getTrafficLight(id) ==
(
  return lights(id);
)
pre id in set dom lights;

public EnvironmentReady: () ==> ()
EnvironmentReady() == skip;

public CalculateInRange: () ==> ()
CalculateInRange() ==
(
   -- vehicles/controllers are denoted units in the following
   let units = rng ctrlUnits in
    -- for all units, find the ones in range.
    -- This could be optimized given that if one unit can see another unit,
    -- then they can see each other, no need to calculate the range again
    -- for units seeing each other. However this will be complex, given that
    -- one unit might have serveral units in its range that aren't in range
    -- of each other.
    for all unit in set units do
    (
     let pos = unit.GetPosition() in
           graphics.updatePosition(unit.GetVehicleID(), pos.X(), pos.Y());

     let dir = unit.GetDirection() in graphics.updateDirection(
                                      unit.GetVehicleID(),
                                      Types`DirectionToGraphics(dir));

     let inrange = FindInRangeWithOppositeDirection(unit, units)
     in
     (
       -- only request data, the way the loop is built will ensure that all
    -- units will request data.
       if(card inrange > 0)
       then
       for all oncomingVehicle in set inrange do
       (
         unit.AddTrafficData(oncomingVehicle.GetVehicleID()
              ,oncomingVehicle.GetTrafficData());

         let vehicleDTO = unit.getVehicleDTO() in
         oncomingVehicle.AddOncomingVehicle(vehicleDTO);
       );
  )
    );

    graphics.sleep();

-- synchronization, when we have calculated inrange allow vehicles to
--move again
    for all u in set rng ctrlUnits do u.EnvironmentReady();
);

--
-- Functions definition section
--
functions
public static OppositeDirection : Types`Direction -> Types`Direction
OppositeDirection(d) ==
cases d:
<NORTH> -> <SOUTH>,
<SOUTH> -> <NORTH>,
<EAST>  -> <WEST>,
<WEST>  -> <EAST>
end;

-- compare the range of a single vehicle/controller to a
-- set of vehicles/controllers
public  FindInRange : Controller * set of Controller -> set of Controller
FindInRange(v, vs) ==
   let inrange = { ir | ir in set vs & v <> ir and InRange(v,ir) = true }
   in
   inrange;


-- compare the range of two vehicles/controllers
public InRange : Controller * Controller -> bool
InRange(u1,u2) ==
let pos1 = u1.GetPosition(), pos2 = u2.GetPosition()
in
pos1.inRange(pos2, Config`Range);



-- compare the range of a single vehicle/controller to a set of
-- vehicles/controllers moving in the opposite direction
public FindInRangeWithOppositeDirection : Controller * set of Controller
-> set of Controller
FindInRangeWithOppositeDirection(u ,us) ==
let dir = OppositeDirection(u.GetDirection()) in
  let inrange = { ir | ir in set FindInRange(u, us) & dir = ir.GetDirection()}
    in inrange;

--
-- Values definition section
--
values

--
-- Thread definition section
--
thread
(
while true do
(
   CalculateInRange();
   env.goEnvironment();
)
)

--
-- sync definition section
--
sync
per CalculateInRange => #fin(EnvironmentReady) > #fin(CalculateInRange);

-- has heavy performance loss
mutex (CalculateInRange, addController, getController);
mutex (addController);
mutex (getController);
mutex (CalculateInRange)
end VeMoController

\end{vdm_al}

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

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.