From a8e64b7c67d119528f9946896e0e12521ae54a7a Mon Sep 17 00:00:00 2001 From: Parzival-05 Date: Sat, 9 Aug 2025 12:24:08 +0300 Subject: [PATCH 1/5] fix: Allow AISearcher to pick a step without relying on stepsPlayed --- VSharp.Explorer/AISearcher.fs | 45 ++++++++++++++++------------------- 1 file changed, 20 insertions(+), 25 deletions(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 639f2f651..7a8e6ef72 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -123,32 +123,27 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Runner && stepsToPlay = stepsPlayed then + let toPredict = + match aiMode with + | TrainingSendEachStep + | TrainingSendModel -> + if stepsPlayed > 0u then + gameStateDelta + else + gameState.Value + | Runner -> gameState.Value + + let stateId = oracle.Predict toPredict + afterFirstAIPeek <- true + let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId) + lastCollectedStatistics <- statistics + + match state with + | Some state -> Some state + | None -> + incorrectPredictedStateId <- true + oracle.Feedback(Feedback.IncorrectPredictedStateId stateId) None - else - let toPredict = - match aiMode with - | TrainingSendEachStep - | TrainingSendModel -> - if stepsPlayed > 0u then - gameStateDelta - else - gameState.Value - | Runner -> gameState.Value - - let stateId = oracle.Predict toPredict - - afterFirstAIPeek <- true - let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId) - lastCollectedStatistics <- statistics - stepsPlayed <- stepsPlayed + 1u - - match state with - | Some state -> Some state - | None -> - incorrectPredictedStateId <- true - oracle.Feedback(Feedback.IncorrectPredictedStateId stateId) - None static member updateGameState (delta: GameState) (gameState: Option) = match gameState with From cd23fbfaba7c34596287a05c493caf992d43052d Mon Sep 17 00:00:00 2001 From: Parzival-05 Date: Thu, 22 May 2025 01:56:18 +0300 Subject: [PATCH 2/5] feat: Add sending of steps count --- VSharp.ML.GameServer.Runner/Main.fs | 1 + VSharp.ML.GameServer/Messages.fs | 10 ++++++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/VSharp.ML.GameServer.Runner/Main.fs b/VSharp.ML.GameServer.Runner/Main.fs index 1b4b9a207..9f409b36f 100644 --- a/VSharp.ML.GameServer.Runner/Main.fs +++ b/VSharp.ML.GameServer.Runner/Main.fs @@ -239,6 +239,7 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) = GameOver( explorationResult.ActualCoverage, explorationResult.TestsCount, + explorationResult.StepsCount, explorationResult.ErrorsCount ) ) diff --git a/VSharp.ML.GameServer/Messages.fs b/VSharp.ML.GameServer/Messages.fs index 43c60c51b..7f13570f7 100644 --- a/VSharp.ML.GameServer/Messages.fs +++ b/VSharp.ML.GameServer/Messages.fs @@ -109,11 +109,13 @@ type GameOverMessageBody = interface IRawOutgoingMessageBody val ActualCoverage: uint val TestsCount: uint32 + val StepsCount: uint32 val ErrorsCount: uint32 - new(actualCoverage, testsCount, errorsCount) = + new(actualCoverage, testsCount, stepsCount, errorsCount) = { ActualCoverage = actualCoverage TestsCount = testsCount + StepsCount = stepsCount ErrorsCount = errorsCount } [] @@ -371,7 +373,7 @@ type IncorrectPredictedStateIdMessageBody = new(stateId) = { StateId = stateId } type OutgoingMessage = - | GameOver of uint * uint32 * uint32 + | GameOver of uint * uint32 * uint32 * uint32 | MoveReward of Reward | IncorrectPredictedStateId of uint | ReadyForNextStep of GameState @@ -397,8 +399,8 @@ let deserializeInputMessage (messageData: byte[]) = let serializeOutgoingMessage (message: OutgoingMessage) = match message with - | GameOver(actualCoverage, testsCount, errorsCount) -> - RawOutgoingMessage("GameOver", box (GameOverMessageBody(actualCoverage, testsCount, errorsCount))) + | GameOver(actualCoverage, testsCount, stepsCount, errorsCount) -> + RawOutgoingMessage("GameOver", box (GameOverMessageBody(actualCoverage, testsCount, stepsCount, errorsCount))) | MoveReward reward -> RawOutgoingMessage("MoveReward", reward) | IncorrectPredictedStateId stateId -> RawOutgoingMessage("IncorrectPredictedStateId", IncorrectPredictedStateIdMessageBody stateId) From e9cb37576b8c29625f79082b3da87287197e105f Mon Sep 17 00:00:00 2001 From: Parzival-05 Date: Thu, 22 May 2025 03:10:59 +0300 Subject: [PATCH 3/5] Rename PathCondition according to client's naming --- VSharp.Explorer/AISearcher.fs | 4 ++-- VSharp.ML.GameServer/Messages.fs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 7a8e6ef72..50116cd64 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -180,7 +180,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option val Position: uint // to basic block id - val PathCondition: PathConditionVertex + val PathConditionSize: PathConditionVertex val VisitedAgainVertices: uint val VisitedNotCoveredVerticesInZone: uint val VisitedNotCoveredVerticesOutOfZone: uint @@ -177,7 +177,7 @@ type State = ) = { Id = id Position = position - PathCondition = pathCondition + PathConditionSize = pathCondition VisitedAgainVertices = visitedAgainVertices VisitedNotCoveredVerticesInZone = visitedNotCoveredVerticesInZone VisitedNotCoveredVerticesOutOfZone = visitedNotCoveredVerticesOutOfZone From 9c58eda3fc1151df775a7066961bdedb6356fce2 Mon Sep 17 00:00:00 2001 From: Parzival-05 Date: Tue, 12 Aug 2025 14:52:25 +0300 Subject: [PATCH 4/5] Revert "Rename PathCondition according to client's naming" This reverts commit e9cb37576b8c29625f79082b3da87287197e105f. --- VSharp.Explorer/AISearcher.fs | 4 ++-- VSharp.ML.GameServer/Messages.fs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 50116cd64..7a8e6ef72 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -180,7 +180,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option val Position: uint // to basic block id - val PathConditionSize: PathConditionVertex + val PathCondition: PathConditionVertex val VisitedAgainVertices: uint val VisitedNotCoveredVerticesInZone: uint val VisitedNotCoveredVerticesOutOfZone: uint @@ -177,7 +177,7 @@ type State = ) = { Id = id Position = position - PathConditionSize = pathCondition + PathCondition = pathCondition VisitedAgainVertices = visitedAgainVertices VisitedNotCoveredVerticesInZone = visitedNotCoveredVerticesInZone VisitedNotCoveredVerticesOutOfZone = visitedNotCoveredVerticesOutOfZone From a24629b40daee2856ae6fa026cdadee57e8019f7 Mon Sep 17 00:00:00 2001 From: Parzival-05 Date: Sat, 16 Aug 2025 09:12:13 +0300 Subject: [PATCH 5/5] Fix AISearcher bug with stepsPlayed --- VSharp.Explorer/AISearcher.fs | 1 + 1 file changed, 1 insertion(+) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 7a8e6ef72..49a450b38 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -137,6 +137,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Seq.tryFind (fun s -> s.internalId = stateId) lastCollectedStatistics <- statistics + stepsPlayed <- stepsPlayed + 1u match state with | Some state -> Some state