module traffic_light
{
  // Define the states of the traffic light
  type state_t = enum { red, green };

  // Variable to hold the current state of the traffic light
  var current_state : state_t;

  // Initialize the traffic light in the red state
  init {
    current_state = red;
  }

  // Define the state transition logic
  next {
    current_state' = (current_state == red) ? green : red;
  }
}

module main
{
  // Instance of the traffic light
  instance tl : traffic_light;

  // Control block to simulate the traffic light transitions
  control {
    v = unroll(10); // Unroll the model for 10 steps
    check;
    print_results;
    v.print_cex(tl.current_state);
  }
}
