SSL Vehicle.vdmrt   Interaktion und
PortierbarkeitVDM

\section{Vehicle Class}

\begin{vdm_al}
-----------------------------------------------
-- Class: Vehicle
-- Description:  Vehicle class describes the physical moving 
-- elements in the system
-----------------------------------------------

--
-- class definition
--
class Vehicle

--
-- instance variables
--
instance variables

private dir: Types`Direction;
private speed : nat;
private lowgrip : bool;
private turnIndicator : Indicator := <NONE>;
private pos : Position;
private id : nat;
--
-- Types definition section
--
types  
public Indicator = <LEFT> | <RIGHT> | <NONE>;
--
-- Operations definition section
--
operations

public Vehicle:  nat * Position * nat * Types`Direction ==> Vehicle
Vehicle(identifier, p, s, d) ==
(
  pos := p;
  speed := s;
  dir := d;
  id := identifier;
  lowgrip := false;
);


public Vehicle:  VehicleData ==> Vehicle
Vehicle(vdDTO) ==
(
  pos := vdDTO.GetPosition();
  speed := vdDTO.GetSpeed();
  dir := vdDTO.GetDirection();
  id := vdDTO.GetID();
  lowgrip := vdDTO.getLowGrip();
);


pure public GetDirection: () ==> Types`Direction 
GetDirection() ==
return dir;

async public SetDirection: Types`Direction  ==> ()
SetDirection(d) ==
(
dir := d;
);

public GetSpeed: () ==> nat 
GetSpeed() ==
return speed;
 
async public SetSpeed: nat ==> () 
SetSpeed(s) ==
speed := s;

public getLowGrip: () ==> bool 
getLowGrip() ==
(
return lowgrip
);

async public setLowGrip: bool ==> () 
setLowGrip(lg) ==
(
lowgrip := lg;
);
 
public TurnIndicator: () ==> Indicator 
TurnIndicator() ==
return turnIndicator; 
 
async public setTurnIndicator: Indicator ==> () 
setTurnIndicator(indicator) ==
( 
 turnIndicator := indicator;
);
 
pure public GetPosition: () ==> Position 
GetPosition() ==
return pos.deepCopy();

async public SetPosition: Position ==> () 
SetPosition(p) ==
pos := p;

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

public Move : () ==> ()
Move() ==
(
 cases dir:
 <NORTH> -> pos.setY(pos.Y() + speed),  
 <SOUTH> -> pos.setY(pos.Y() - speed),  
 <EAST>  -> pos.setX(pos.X() + speed), 
 <WEST>  -> pos.setX(pos.X() - speed) 
 end;

);
  
public getDTO : () ==> VehicleData
getDTO() ==
(
 let vd = new VehicleData(id, pos, speed, dir, lowgrip) in 
 return vd;
)
  
--
-- Functions definition section
--
functions
  
public static IndicatorToString : Indicator -> seq of char 
IndicatorToString(i) ==
(
cases i:
<LEFT>-> "LEFT",
<RIGHT>-> "RIGHT",
<NONE>-> "NONE"
end
)



--
-- Values definition section
--
values

--
-- sync definition section
--
sync
 mutex(Move);
 mutex(Move, SetPosition);
 mutex(SetPosition);
 mutex(SetDirection);
 --mutex(GetDirection, SetDirection);
 mutex(SetSpeed);
 mutex(GetSpeed, SetSpeed);
 mutex(setLowGrip);
 mutex(getLowGrip, setLowGrip);
 mutex(setTurnIndicator);
 mutex(TurnIndicator,setTurnIndicator);
 
end Vehicle


\end{vdm_al}

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