// ----------------------------------------------------------------
// A traffic light controler
// ----------------------------------------------------------------
 
// executing control() with P=4, L=4, T=10, N=5
// yields 200000 action sequences in about 80s.

val P:ℕ; // number of paths
val L:ℕ; // number of traffic lights
val T:ℕ; // maximum time span
val N:ℕ; // maximum number of control cycles
axiom notZero ⇔ P > 0 ∧ L > 0 ∧ T > 0 ∧ N > 0;

// the basic types
type Path  = ℕ[P-1]; 
type Light = ℕ[L-1]; 
type Time  = ℕ[T]; 

// the times
val TR:Time = 1; // time red must be on before switching to green
val TA:Time = 1; // time amber must be on before switching to red

// the colors
type Color = ℕ[2];
val red = 0; val green = 1; val amber = 2;

// auxiliary types
type Conflict = Tuple[Path,Path]; 
type Control = Record[light:Light,path:Path,priority:Bool];

// the configuration of the crossing
type Crossing = Record[
  // which paths conflict with each other?
  conflicts: Set[Conflict],
  
  // which lights control which paths?
  controls: Set[Control], 
  
  // which lights give exclusive access?
  exclusive: Map[Light,Bool]
];

// the traffic light situation
type State = Record[
  colors: Map[Light,Color],    // color of each light 
  lastchanged: Map[Light,Time] // time each light switched last  
];

// the next action to be performed
type Action = Record[light:Light,delay:Time];

// -----------------------------------------------------------------
// public auxiliary operations
// -----------------------------------------------------------------

// the next color in the traffic light cycle
fun next(c:Color):Color = (c+1)%3;

// compute next light setting from current setting l and action a
proc switch(s:State,a:Action):State 
{
  var sv:State = s;
  sv.colors[a.light] = next(sv.colors[a.light]);
  for var i:ℕ[L]=0; i < L; i ≔ i+1 do
  {
    if i = a.light then
      sv.lastchanged[i] = 0;
    else
      sv.lastchanged[i] = sv.lastchanged[i]+a.delay;
  }
  return sv;
}

// do by actions times not overflow?
pred timebound(s:State, a:Action) ⇔ 
  ∀i:Light with i ≠ a.light. (s.lastchanged[i]+a.delay ≤ T);

// -----------------------------------------------------------------
// the core operations
// -----------------------------------------------------------------

// is action l for crossing c with light setting l valid?
pred valid(c:Crossing, s:State, a:Action) 
  // sample solution: 2 auxiliary predicates
  // in total 13 lines of formulas
⇔ ⊥;

// -----------------------------------------------------------------
// the execution of the system
// -----------------------------------------------------------------

type Actions = Array[N,Action];
type States = Array[N+1,State];
proc states(init:State,as:Actions): States
{
  var s:States = Array[N+1,State](init);
  print s;
  for var i:ℕ[N] = 0; i < N; i ≔ i+1 do
  {
    s[i+1]:= switch(s[i],as[i]);
  }
  return s;
}

// the execution of the system
proc control(c:Crossing): Actions
  // do not consider identities or symmetric duplicates
  requires ∀pt∈c.conflicts. (pt.1 < pt.2 ∧ pt.2 < P);
{
  var as: Actions = Array[N,Action](⟨light:0,delay:0⟩);
  val init = ⟨colors: Map[Light,Color](red),lastchanged: Map[Light,Time](0)⟩;
  var s:State = init;
  for var i:ℕ[N] = 0; i < N; i ≔ i+1 do
  {
    choose a:Action with valid(c,s,a) ∧ timebound(s,a);
    as[i] ≔ a;
    s ≔ switch(s,a);  
  }
  // print states(init,as);
  return as;
}

// a four path crossing where every car may move straight ahead (priority)
// or turn left or right, lights are not exclusive
proc c1(): Crossing 
{
  val cont = 
    { ⟨light:0,path:0,priority:⊤⟩, ⟨light:0,path:1,priority:⊥⟩, ⟨light:0,path:3,priority:⊥⟩,
      ⟨light:1,path:1,priority:⊤⟩, ⟨light:1,path:0,priority:⊥⟩, ⟨light:1,path:2,priority:⊥⟩,
      ⟨light:2,path:2,priority:⊤⟩, ⟨light:2,path:1,priority:⊥⟩, ⟨light:2,path:3,priority:⊥⟩,
      ⟨light:3,path:3,priority:⊤⟩, ⟨light:3,path:0,priority:⊥⟩, ⟨light:3,path:2,priority:⊥⟩ };
  val conf = 
    { ⟨0,1⟩, ⟨0,3⟩, ⟨1,2⟩, ⟨2,3⟩ };
  val excl = Map[Light,Bool](⊥);
  return ⟨conflicts:conf, controls:cont, exclusive:excl⟩;
}

// check system for this crossing
fun control1(): Actions = control(c1());

// -----------------------------------------------------------------
// end of file
// -----------------------------------------------------------------