gistfile1.txt

MODULE main
  VAR
      NS_Sensor : boolean;
      EW_Sensor : boolean;


      Light_Prev_State : {NS, EW};
      Light_State : {NS_Green, EW_Green};

ASSIGN

  init(NS_Sensor) := FALSE;
  init(EW_Sensor) := FALSE;

  -- Arbitrarily Set the Light State
  init(Light_State) := NS_Green;
  -- Arbitrariy initialize the previous state to NS
  init(Light_Prev_State) := EW;

  next(Light_State) :=
    case


    -- Current Light State is NS
    Light_State = NS_Green & !NS_Sensor & EW_Sensor : EW_Green;

    Light_State = NS_Green & NS_Sensor & !EW_Sensor : NS_Green;

    Light_State = NS_Green & NS_Sensor & EW_Sensor & Light_Prev_State = NS: EW_Green;

    Light_State = NS_Green & NS_Sensor & EW_Sensor & Light_Prev_State = EW : NS_Green;

    Light_State = NS_Green & !NS_Sensor & !EW_Sensor & Light_Prev_State = NS  : NS_Green;

    Light_State = NS_Green & !NS_Sensor & !EW_Sensor & Light_Prev_State = EW  : EW_Green;

     -- Current Light State is EW
    Light_State = EW_Green & !NS_Sensor & EW_Sensor : EW_Green;

    Light_State = EW_Green & NS_Sensor & !EW_Sensor : NS_Green;

    Light_State = EW_Green & NS_Sensor & EW_Sensor & Light_Prev_State = NS: EW_Green;

    Light_State = EW_Green & NS_Sensor & EW_Sensor & Light_Prev_State = EW : NS_Green;


    TRUE  : Light_State;
    esac;

    -- SENSORS

    next(NS_Sensor) :=
      case
        NS_Sensor = TRUE : {TRUE, FALSE};
        NS_Sensor = FALSE : {TRUE, FALSE};
        TRUE  : NS_Sensor;
      esac;

    next(EW_Sensor) :=
      case
        EW_Sensor = TRUE : {TRUE, FALSE};
        EW_Sensor = FALSE : {TRUE, FALSE};
        TRUE  : EW_Sensor;
      esac;

    -- LAST GREEN
    next(Light_Prev_State) :=
      case
        Light_State = NS_Green : NS;
        Light_State = EW_Green : EW;
      TRUE : Light_Prev_State;
      esac;

  -- SAFEY --
  -- NS and EW lights can never be green at the same time
  SPEC AG !( Light_State = NS_Green & Light_State = EW_Green)
  -- Check to make sure that the light state is active in one direction
  SPEC AG ( Light_State = NS_Green | Light_State = EW_Green)

  -- LIVELINESS --

  -- At some point, both North/South and East/West traffic can go
  SPEC AF (Light_State = NS_Green -> Light_State = EW_Green)

  -- North/south traffic will eventually be able to go
  SPEC AF (NS_Sensor = TRUE -> Light_State = NS_Green)

 -- ERROR - KNOWN BAD CONDITIONS
  -- SPEC AF !(NS_Sensor = TRUE -> Light_State = NS_Green)