Quelle VDMController.vdmrt Sprache: VDM

\section{VDMController Class}

\begin{vdm_al}
-----------------------------------------------
-- Class: VDMController
-- Description: VDMController main controller for the VDM system
-----------------------------------------------

--
-- class definition
--
class VDMController

--
-- 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;

--
-- Types definition section
--
types

--
-- Operations definition section
--
operations

public addController: Controller ==> ()
addController(ctrl) ==
(
    ctrlUnits := ctrlUnits munion {ctrl.GetVehicleID() |->  ctrl} ;
)
pre ctrl.GetVehicleID() not in set (dom ctrlUnits union dom lights);

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 Step: () ==> ()
Step() ==
(
   CalculateInRange();
);

public CalculateInRange: () ==> ()
CalculateInRange() ==
(
   -- vehicles
   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 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);
       );
      )
    )
);

--
-- 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
  (
   duration(1000)
   Step()
  )
)

--
-- sync definition section
--
sync
per Step => #fin(addController) > 0;
-- has heavy performance loss
mutex (CalculateInRange, addController, getController);
mutex (addController);
mutex (getController);
mutex (CalculateInRange)
end VDMController

\end{vdm_al}

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

quality87%

¤ Dauer der Verarbeitung: 0.12 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.