Quelle  RailwayGrid.vdmrt

\section{CyberRail class}
\begin{vdm_al}

class RailwayGrid

instance variables

private routeList : set of TransportPlan`Route; 
private grid : Grid := {};
private inactiveGrid : Grid := {};
private inactiveRouteID : set of (TransportPlan`Route | nat) := {};
private io : IO := new IO();

types

public String = seq of char;
public Plan = seq of TransportPlan`Route;
public Grid = set of Plan;


operations

--Constructor
public RailwayGrid : () ==> RailwayGrid 
RailwayGrid()==
( 
--duration(0)(
dcl R1 : TransportPlan`Route 
       := mk_TransportPlan`Route("A", "B", 42, "P1",200, 1), 
 R2 : TransportPlan`Route 
    := mk_TransportPlan`Route("A", "C", 42, "P1", 200, 2),
 R3 : TransportPlan`Route 
    := mk_TransportPlan`Route("B", "C", 99, "P1", 200, 3), 
 R4 : TransportPlan`Route 
    := mk_TransportPlan`Route("B", "D", 42, "P1", 200,4),
 R5 : TransportPlan`Route 
    := mk_TransportPlan`Route("B", "A", 42, "P1", 200,5), 
 R6 : TransportPlan`Route 
    := mk_TransportPlan`Route("C", "D", 42, "P1", 200,6),
 R7 : TransportPlan`Route 
    := mk_TransportPlan`Route("C", "A", 42, "P1", 200,7),
 R8 : TransportPlan`Route 
    := mk_TransportPlan`Route("D", "B", 42, "P1", 200,8), 
 R9 : TransportPlan`Route 
    := mk_TransportPlan`Route("D", "C", 42, "P1", 200,9),
 R10 : TransportPlan`Route 
     := mk_TransportPlan`Route("C", "B", 99, "P1", 200,10);
 
 routeList := {R1,R2,R3,R4,R5,R6,R7,R8,R9,R10}; 

 grid := recAlgo({},[], "A") union 
         recAlgo({},[], "B") union 
         recAlgo({},[], "C") union 
         recAlgo({},[], "D"); 
 writef (grid);
-- );
-- return self;
);

private recAlgo : Grid * Plan * String ==> Grid
recAlgo(grid, plan, station) ==
(
 dcl grid_temp : Grid := grid;
 for all r in set routeList  do
 (
  if( r.departureLocation = station and 
    not (exists p in set elems plan & 
    r.arrivalLocation = p.arrivalLocation or
    r.arrivalLocation = p.departureLocation) )
  then (
     dcl temp : Plan :=  plan ^ [r];
     grid_temp := grid_temp union {temp};
      grid_temp := recAlgo( grid_temp, temp, 
                            r.arrivalLocation);
     );
 );
  return grid_temp;
);

pure public getGrid: () ==> Grid
getGrid()==
(
 return grid;
);

public setInactiveRoute : nat ==> ()
setInactiveRoute(id)==
(
 duration(0) (
 inactiveRouteID := inactiveRouteID union {id};
 inactiveGrid := inactiveGrid union  
                 {tp | tp in set grid
                     & exists x in set elems tp & x.id_route = id};
 grid := {x | x in set grid 
            & id not in set {route.id_route | route in set elems x}}; 
 );
)
pre exists x in set routeList & x.id_route = id;




---------------------------------------------------------------------------------------------------------------
publictest)==()
test()== 
(
writefrecAlgo,] A) union 
         recAlgo({},[], "B")
        recAlgo({,[, "C" union
         recAlgo({},[],private grid : Grid : };
);

 writefGrid ==> )
 writef  : IO=new IO);
 (
 def  iofwriteval](".txt",,<append>)in skip;
 );

end RailwayGrid
\end{vdm_al}