diff --git a/VSharp.ML.AIAgent/launch_servers.py b/VSharp.ML.AIAgent/launch_servers.py index 975600c42..a36f3fdd6 100644 --- a/VSharp.ML.AIAgent/launch_servers.py +++ b/VSharp.ML.AIAgent/launch_servers.py @@ -132,6 +132,22 @@ def kill_server(server_instance: ServerInstanceInfo): os.kill(server_instance.pid, signal.SIGKILL) PROCS.remove(server_instance.pid) + wait_for_reset_retries = FeatureConfig.ON_GAME_SERVER_RESTART.wait_for_reset_retries + while wait_for_reset_retries: + logging.info( + f"Waiting for {server_instance} to die, {wait_for_reset_retries} retries left" + ) + if psutil.Process(server_instance.pid).status() in ( + psutil.STATUS_DEAD, + psutil.STATUS_ZOMBIE, + ): + break + time.sleep(FeatureConfig.ON_GAME_SERVER_RESTART.wait_for_reset_time) + wait_for_reset_retries -= 1 + + if wait_for_reset_retries == 0: + raise RuntimeError(f"{server_instance} could not be killed") + logging.info(f"killed {psutil.Process(server_instance.pid)}")