\section{Test of VDMController}

\begin{vdm_al}
------------------------------------------------
-- Class: TestVDMController
-- Description:  Test the VDMController class 
-----------------------------------------------

--
-- class definition
--
class TestVDMController is subclass of TestCase

--
-- instance variables
--
instance variables
private pos : Position;
--
-- Operations definition section
--
operations
public TestVDMController: seq of char ==> TestVDMController
TestVDMController(s) ==
(
 TestCase(s);
);

protected SetUp: () ==> ()
SetUp () == pos := new Position(1,1); 

protected RunTest: () ==> ()
RunTest () ==
(
 Printer`OutAlways("Testing VDMController");
 start(self);
 self.IsFinished();
);
  
  
private runner : () ==> ()
runner () ==
(
 dcl vec : Vehicle := new Vehicle(2, pos, 1, <NORTH>),
 vec2 : Vehicle := new Vehicle(3, new Position(1,3), 1, <SOUTH>),
 ctrl : Controller := new Controller(vec),
 ctrl2 : Controller := new Controller(vec2),
 vec3 : Vehicle := new Vehicle(4, new Position(1,3), 1, <EAST>),
 vdmCtrl : VDMController := new VDMController(),
 trfLight : TrafficLight := new TrafficLight(11, new Position(1,3), 5);
 
 --test call of inrange and data exchange
 vec.setLowGrip(true);
 vdmCtrl.addController(ctrl);
 vdmCtrl.addController(ctrl2);
 AssertTrue(vdmCtrl.getController(2) = ctrl);
 
 start(vdmCtrl);
 start(ctrl);
 
 vdmCtrl.Step();
 let vs = ctrl.GetTrafficData() in
  (
  skip;
   let v = vs(1) in
   (
    AssertTrue(v.GetPosition().X() = 1);
    AssertTrue(v.GetPosition().Y() = 2);
    AssertTrue(v.GetMessage() = <LowGrip>);
    AssertTrue(v.GetDirection() = <NORTH>);
   )
  );
  
  --test opposite direction
  AssertTrue(VDMController`OppositeDirection(vec3.GetDirection()) = <WEST>);  
  vec3.SetDirection(<WEST>);
  AssertTrue(VDMController`OppositeDirection(vec3.GetDirection()) = <EAST>);
  
  -- test trafficlight
  vdmCtrl.addTrafficLight(trfLight);
  let t = vdmCtrl.getTrafficLight(11) in
  (
   AssertTrue(t.GetID() = 11);
  AssertTrue(Position`Compare(t.GetPosition(), new Position(1,3)));
  )
);
  
  
private IsFinished : () ==> ()
IsFinished () ==  skip;

  
protected TearDown: () ==> ()
TearDown () == skip;


thread
(
 runner(); 
)

--
-- sync definition section
--
sync
 per IsFinished => #fin(runner) > 0;

end TestVDMController

\end{vdm_al}

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