-- Kathi Fisler
-- February 7, 1995
-- Island Traffic Light Controller, version 3
-- Used corrected environmental assumption as proposed by ratan

MODULE main
VAR
  istate : {igreen, ired, icar_entering, icar_exiting};
  mstate : {mgreen, mred, mcar_entering, mcar_exiting};
  tstate : {dispatch, island_use, mainland_use, iclear, mclear};
  IGL : boolean; -- the lights
  IRL : boolean;
  MGL : boolean;
  MRL : boolean; 
  IU : boolean; -- in use
  MU : boolean; 
  IE : boolean; -- entering tunnel sensors
  ME : boolean; 
  IX : boolean; -- exiting tunnel sensors
  MX : boolean;
  IR : boolean; -- request tunnel
  MR : boolean; 
  IG : boolean; -- tunnel granted
  MG : boolean; 
  IY : boolean; -- tunnel yield
  MY : boolean; 
  TC : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16} ;
  IC : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16} ;
  

ASSIGN
  init(TC) := 0;

-- island controller

  init(istate) := ired;
  next(istate) := 
     case
        istate = igreen & IY : ired;
        istate = igreen & !IY & !IE : igreen;
        istate = igreen & !IY & IE : icar_entering;

        istate = icar_entering & IE : icar_entering;
        istate = icar_entering & !IE : igreen;

        istate = ired & !IX & !IG : ired;
        istate = ired & !IX & IG : igreen;
        istate = ired & IX : icar_exiting;

        istate = icar_exiting & IX : icar_exiting;
        istate = icar_exiting & !IX : ired;
     esac;

  IGL := istate = igreen | istate = icar_entering;
  IRL := istate = ired | istate = icar_exiting;
  IU := istate = igreen | istate = icar_entering;
  IR := istate = ired & IE;

-- mainland controller
  init(mstate) := mred;
  next(mstate) := 
     case
        mstate = mgreen & !(IC < 16) : mred;
        mstate = mgreen & (IC < 16) & MY : mred;
        mstate = mgreen & (IC < 16) & !MY & !ME : mgreen;
        mstate = mgreen & (IC < 16) & !MY & ME : mcar_entering;

        mstate = mcar_entering & ME : mcar_entering;
        mstate = mcar_entering & !ME : mgreen;

        mstate = mred & !MX & !MG : mred;
        mstate = mred & !MX & MG : mgreen;
        mstate = mred & MX : mcar_exiting;

        mstate = mcar_exiting & MX : mcar_exiting;
        mstate = mcar_exiting & !MX : mred;
     esac;

  MGL := mstate = mgreen | mstate = mcar_entering;
  MRL := mstate = mred | mstate = mcar_exiting;
  MU := mstate = mgreen | mstate = mcar_entering;
  MR := mstate = mred & ME;

-- tunnel controller
  init(tstate) := dispatch;
  next(tstate) :=
     case
        tstate = dispatch & !IR & !MR : dispatch;
        tstate = dispatch & IR & MU : mainland_use;
        tstate = dispatch & IR & !MU & (TC = 0) : dispatch;  
        tstate = dispatch & IR & !MU & !(TC = 0) : mclear;
        tstate = dispatch & !IR & MR & !(IC < 16) : dispatch;  
        tstate = dispatch & !IR & MR & (IC < 16) & IU : island_use;  
        tstate = dispatch & !IR & MR & (IC < 16) & !IU & (TC = 0) : dispatch;  
        tstate = dispatch & !IR & MR & (IC < 16) & !IU & !(TC = 0) : iclear;  

        tstate = island_use & IU : island_use;
        tstate = island_use & !IU : iclear;
        
        tstate = mainland_use & MU : mainland_use;
        tstate = mainland_use & !MU : mclear;
        
        tstate = iclear & !(TC = 0) : iclear;
        tstate = iclear & (TC = 0) : dispatch;

        tstate = mclear & !(TC = 0) : mclear;
        tstate = mclear & (TC = 0) : dispatch;
     esac;

  IY := tstate = island_use;
  MY := tstate = mainland_use;
  IG := (tstate = dispatch & IR & !MU & (TC = 0)) | 
        (tstate = mclear & (TC = 0));
  MG := (tstate = dispatch & !IR & MR & (IC < 16) & !IU & (TC = 0)) | 
        (tstate = iclear & (TC = 0));

DEFINE
  tcincr := (istate = igreen & !IY & IE) | 
            (mstate = mgreen & !MY & ME & (IC < 16));
  tcdecr := (istate = ired & IX) | (mstate = mred & MX);
  icdecr := istate = igreen & !IY & IE;
  icincr := mstate = mgreen & !MY & ME;

  tunnel_empty := TC = 0;

ASSIGN
  next(TC) := 
     case
        tcincr & (TC < 16) : TC + 1;
        tcdecr & (TC > 0) : TC - 1;
        1 : TC;
     esac;

  next(IC) :=
     case
        icdecr & (IC > 0) : IC - 1;
        icincr & (IC < 16): IC + 1;
        1 : IC;
     esac;

DEFINE
  env1 := (IE -> AF MX);
  env2 := A[!MX U IE];
  env3 := (ME -> AF IX);
  env4 := A[!IX U ME];
  env := env1 & env2 & env3 & env4;
  
  conda := !((istate = icar_exiting) & (mstate = mcar_exiting));

FAIRNESS IE
FAIRNESS ME
FAIRNESS !IE
FAIRNESS !ME

-- a test case to see how things are working
SPEC (AF conda) | A[conda U !env]

-- access never granted while cars in tunnel
SPEC AG ((IG | MG) -> (TC = 0))

-- tunnel used once granted
SPEC (AF (IG -> AF IU)) | A[(IG -> AF IU) U !env]
SPEC (AF (MG -> AF MU)) | A[(MG -> AF MU) U !env]

-- requests eventually granted
SPEC (AF (IR -> AF IG)) | A[(IR -> AF IG) U !env]
SPEC (AF (MR -> AF MG)) | A[(MR -> AF MG) U !env]

-- only change counters once per car
SPEC (AF ((IE & tcincr) -> A[!tcincr U !IE]))
     | A[((IE & tcincr) -> A[!tcincr U !IE]) U !env]

-- not incrementing and decrementing counters simultaneously
--SPEC AG !(tcincr & tcdecr)
SPEC AG !(icincr & icdecr)

-- never cars travelling both directions at once
SPEC AG (((IE <-> AX (AF MX)) & (ME <-> AX (AF IX))) -> 
                (((!IGL & AX IGL) -> tunnel_empty) &
                 ((!MGL & AX MGL) -> tunnel_empty) &
                 !(IGL & MGL)))

-- more generic liveness
SPEC (AF (IE -> AF IGL)) | A[(IE -> AF IGL) U !env]
SPEC (AF (ME -> AF MGL)) | A[(ME -> AF MGL) U !env]

-- never more than 16 cars on the island
SPEC (AF (IC <= 16)) | A[(IC <= 16) U !env]
SPEC (AF (icincr -> (IC < 16))) | A[(icincr -> (IC < 16)) U !env]
--SPEC (AF (((IC = 16) & ME) -> A[!MGL U (IC < 16)]))
--     | A[(((IC = 16) & ME) -> A[!MGL U (IC < 16)]) U !env]
SPEC (AF (TC + IC <= 16)) | A[(TC + IC <= 16) U !env]

-- yields acknowledged
SPEC (AF (IY -> AF !IU)) | A[(IY -> AF !IU) U !env]
SPEC (AF (MY -> AF !MU)) | A[(MY -> AF !MU) U !env]