Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool


Author: Peter Gorm Larsen and John Fitzgerald

This example is for all small traffic light control kernel presented in the VDM-SL book of John Fitzgerald and Peter Gorm Larsen. It was originally inspired by a similar model made in Z by Paul Ammann. A paper about this written long ago:

A safety kernel for traffic light control, Paul Ammann, Aerospace and Electronic Systems Magazine, IEEE, February 1996, Volume: 11 Issue: 2, pp. 13 - 19, ISSN: 0885-8985.

Properties Values
Language Version: classic
Entry point : DEFAULT`ToAmber(p3,kernel)


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


-- 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),

  kernel : Kernel 
         = mk_Kernel(lights,conflicts)


  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>)


-- changing the light to green for a given path

  ToGreen: Path * Kernel -> Kernel
  ToGreen(p,mk_Kernel(lights,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)) ==
  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)) ==
  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}