module traffic_light {
  type state_t = enum { RED, GREEN };
  var state : state_t;

  init {
    state = RED;
  }

  next {
    state' = (state == RED) ? GREEN : RED;
  }
}

module main {
  var red1, green1, red2, green2 : boolean;
  instance light1 : traffic_light;
  instance light2 : traffic_light;

  init {
    red1 = (light1.state == RED);
    green1 = (light1.state == GREEN);
    red2 = (light2.state == RED);
    green2 = (light2.state == GREEN);
  }

  next {
    havoc light1.state;
    havoc light2.state;
    red1' = (light1.state' == RED);
    green1' = (light1.state' == GREEN);
    red2' = (light2.state' == RED);
    green2' = (light2.state' == GREEN);
  }
}
