module traffic_light
{
  type phase_t = enum { R, G, Y };

  var main_phase : phase_t;
  var sec_phase : phase_t;
  var sec_vehicle : boolean;

  output mG, mY, mR : boolean;
  output sG, sY, sR : boolean;

  init {
    main_phase = G;
    sec_phase = R;
    sec_vehicle = false;
  }

  next {
    case
      (sec_vehicle && sec_phase == R) : {
        mG = false;
        mY = true;
        mR = false;
        sG = false;
        sY = false;
        sR = true;
      }
      (sec_vehicle && sec_phase == G) : {
        mG = false;
        mY = true;
        mR = false;
        sG = false;
        sY = false;
        sR = true;
      }
      (sec_vehicle && sec_phase == Y) : {
        mG = false;
        mY = true;
        mR = false;
        sG = false;
        sY = false;
        sR = true;
      }
      (!sec_vehicle && main_phase == G) : {
        mG = true;
        mY = false;
        mR = false;
        sG = false;
        sY = false;
        sR = true;
      }
      (!sec_vehicle && main_phase == Y) : {
        mG = false;
        mY = false;
        mR = true;
        sG = false;
        sY = false;
        sR = true;
      }
      (!sec_vehicle && main_phase == R) : {
        mG = false;
        mY = false;
        mR = true;
        sG = false;
        sY = false;
        sR = true;
      }
    esac
  }
}
