Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: World.vdmpp Sprache: VDM

Original von: VDM^©

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

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.