class World

values
    private system: InterlockingSystem = new InterlockingSystem();

    private lines: seq of InterlockingSystem`MetroLine =
    [
        LinearLine("Central line", [ Track(1, 0, <Underground>, 2) -- 1
                                   , Track(2, 0, <Underwater>, 1)
                                   , Track(3, 0, <Underwater>, 1)
                                   , Track(4, 0, <Underwater>, 1) -- 2
                                   , Track(5, 0, <Underground>, 2)
                                   , Track(6, 0, <Underground>, 2)
                                   , Track(7, 0, <Underground>, 2) -- 3
                                   , Track(8, 0, <Overground>, 2)
                                   , Track(9, 0, <Overground>, 2)
                                   , Track(9, 1, <Elevated>, 1) ]), -- 4
        
        CircularLine("Circle line", [ Track(4, 1, <Underground>, 1) -- 5
                                    , Track(3, 1, <Underground>, 1)
                                    , Track(2, 1, <Overground>, 1)
                                    , Track(1, 1, <Overground>, 1) -- 6
                                    , Track(1, 0, <Underground>, 2)
                                    , Track(2, 0, <Underwater>, 1)
                                    , Track(3, 0, <Underwater>, 1)
                                    , Track(4, 0, <Underwater>, 1)
                                    , Track(5, 0, <Underground>, 2) -- 7
                                    , Track(5, 1, <Underground>, 1)
                                    , Track(4, 1, <Underground>, 1) ])
    ];
    
    private units: seq of MetroUnit = [ new MetroUnit(mk_token(i)) | i in set { 1, ..., 7 } ];
    
    private stateCharacters: map MetroUnit`MetroUnitState to char = { <Running> |-> 'R', <Stopped> |-> ' ' };
    
functions
    private static Track: nat * nat * InterlockingSystem`TrackKind * nat1 -> InterlockingSystem`Track
                   Track(x, y, kind, capacity) == mk_InterlockingSystem`Track(mk_(x, y), kind, capacity);
    
    private static CircularLine: InterlockingSystem`MetroLineName * seq of InterlockingSystem`Track -> InterlockingSystem`MetroLine
                   CircularLine(name, tracks) == InterlockingSystem`CreateCircularLine(name, tracks);
    
    private static LinearLine: InterlockingSystem`MetroLineName * seq of InterlockingSystem`Track -> InterlockingSystem`MetroLine
                   LinearLine(name, tracks) == InterlockingSystem`CreateLinearLine(name, tracks);
    
operations
    public World: () ==> World
           World() == InitialiseSystem();
    
    private InitialiseSystem: () ==> ()
            InitialiseSystem() ==
            (
                for line in lines do system.AddLine(line);
                for unit in units do system.AddUnit(unit);
                
                units(1).Relocate(lines(1), 1);
                units(2).Relocate(lines(1), 4);
                units(3).Relocate(lines(1), 7);
                units(4).Relocate(lines(1), 10);
                
                units(5).Relocate(lines(2), 1);
                units(6).Relocate(lines(2), 4);
                units(7).Relocate(lines(2), 9);
            );
    
    public Run: nat ==> ()
           Run(stepLimit) ==
                for all step in set { 1, ..., stepLimit } do
                (
                    TickWorld();
                    Print(step);
                );
    
    private TickWorld: () ==> ()
            TickWorld() ==
            (
                system.Tick();
                for unit in units do unit.Tick();
            );
    
    private Pad: seq of char ==> seq of char
            Pad(chars) ==
                if len chars = 1 then
                    return "  " ^ chars
                else if len chars = 2 then
                    return " " ^ chars
                else
                    return chars;
                    
    private Print: nat1 ==> ()
            Print(step) ==
                def stepText = Pad(VDMUtil`val2seq_of_char[nat1](step));
                    states = [ stateCharacters(u.GetState()) | u in seq units ]
                in 
                    IO`println(stepText ^ ": " ^ states);
    
end World