Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: factorial.sml Sprache: VDM

Original von: 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}

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