module traffic_light_system
{
  // Define the state variable.
  var is_red : boolean;

  // Initialize the traffic light to red.
  init {
    is_red = true;
  }

  // Define the state transition.
  next {
    is_red' = !is_red;
  }

  // Control block to simulate the behavior.
  control {
    // Simulate for 10 cycles to observe the behavior.
    v = simulate(10);
    print_results;
  }
}
