Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMPP/MetroInterlockingPP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 4 kB

Quelle World.vdmpp Sprache: 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

quality87%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.