Overture Tool

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