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/VDMSL/trafficSL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 2 kB

Quelle traffic.vdmsl Sprache: VDM

-- Traffic light control kernel
-- For Chapter 5 (Basic Elements)
-- First Version: Without timing constraints

values

-- The following value definitions are used to construct a
-- representation of the junction shown in Figure 5.2

  p1 : Path = mk_token("A1North");

  p2 : Path = mk_token("A1South");

  p3 : Path = mk_token("A66East");

  p4 : Path = mk_token("A66West");

  lights : map Path to Light
         = {p1 |-> <Red>,
            p2 |-> <Red>,
            p3 |-> <Green>,
            p4 |-> <Green>};

  conflicts : set of Conflict
            = {mk_Conflict(p1,p3),
               mk_Conflict(p1,p4),
               mk_Conflict(p2,p3),
               mk_Conflict(p2,p4),
               mk_Conflict(p3,p1),
               mk_Conflict(p4,p1),
               mk_Conflict(p3,p2),
               mk_Conflict(p4,p2)};

  kernel : Kernel
         = mk_Kernel(lights,conflicts)

types

  Light = <Red> | <Amber> | <Green>;

  Time = real
  inv t == t >= 0;

  Path = token;

  Conflict :: path1: Path
              path2: Path
  inv mk_Conflict(path1,path2) == path1 <> path2;

-- the kernel data structure has two components representing
-- 1) a mapping with the current status of the lights for each
-- direction and 2) an unordered collection of conflicts between
-- paths.

  Kernel :: lights    : map Path to Light
            conflicts : set of Conflict
  inv mk_Kernel(ls,cs) ==
        forall c in set cs &
              mk_Conflict(c.path2,c.path1) in set cs and
              c.path1 in set dom ls and
       c.path2 in set dom ls and
              (ls(c.path1) = <Red> or ls(c.path2) = <Red>)

functions

-- changing the light to green for a given path

  ToGreen: Path * Kernel -> Kernel
  ToGreen(p,mk_Kernel(lights,conflicts)) ==
    mk_Kernel(ChgLight(lights,p,<Green>),conflicts)
  pre p in set dom lights and
      lights(p) = <Red> and
      forall mk_Conflict(p1,p2) in set conflicts &
             (p = p1 => lights(p2) = <Red>);

-- changing the light to red for a given path

  ToRed: Path * Kernel -> Kernel
  ToRed(p,mk_Kernel(lights,conflicts)) ==
    mk_Kernel(ChgLight(lights,p,<Red>),conflicts)
  pre p in set dom lights and lights(p) = <Amber>;

-- changing the light to amber for a given path

  ToAmber: Path * Kernel -> Kernel
  ToAmber(p,mk_Kernel(lights,conflicts)) ==
    mk_Kernel(ChgLight(lights,p,<Amber>),conflicts)
  pre p in set dom lights and lights(p) = <Green>;

  ChgLight: (map Path to Light) * Path * Light -> (map Path to Light)
  ChgLight(lights,p,colour) ==
    lights ++ {p |-> colour}

quality93%

¤ Dauer der Verarbeitung: 0.14 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.