c
module automobile {
  var light_on : boolean;
  var door_open : boolean;
  var time : int;

  init {
    light_on = false;
    door_open = false;
    time = 0;
  }

  next {
    if (door_open) {
      light_on' = true;
      time' = 0;
    } else {
      if (time < 30) {
        light_on' = light_on;
        time' = time + 1;
      } else {
        light_on' = false;
        time' = 0;
      }
    }
  }

  transition {
    door_open' = (any i : int :: 0 <= i < N :: door_open[i]);
  }
}

module main {
  const N : int;
  var door_open : array[N] boolean;

  instance auto : automobile(light_on, door_open[0], time);

  init {
    door_open[0] = false;
    door_open[1] = false;
    // Initialize other door_open values as needed
  }

  next {
    door_open[0]' = ...; // Update door_open values based on external inputs
    door_open[1]' = ...;
    // Update other door_open values as needed
  }
}
