Skip to content

Commit 47a76a3

Browse files
authored
Fix steps counting (#97)
* fix: Allow AISearcher to pick a step without relying on stepsPlayed * feat: Add sending of steps count * Rename PathCondition according to client's naming * Revert "Rename PathCondition according to client's naming" This reverts commit e9cb375. * Fix AISearcher bug with stepsPlayed
1 parent 403a9a5 commit 47a76a3

File tree

3 files changed

+28
-29
lines changed

3 files changed

+28
-29
lines changed

VSharp.Explorer/AISearcher.fs

Lines changed: 21 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -123,32 +123,28 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
123123

124124
Application.applicationGraphDelta.Clear()
125125

126-
if aiMode <> Runner && stepsToPlay = stepsPlayed then
126+
let toPredict =
127+
match aiMode with
128+
| TrainingSendEachStep
129+
| TrainingSendModel ->
130+
if stepsPlayed > 0u<step> then
131+
gameStateDelta
132+
else
133+
gameState.Value
134+
| Runner -> gameState.Value
135+
136+
let stateId = oracle.Predict toPredict
137+
afterFirstAIPeek <- true
138+
let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId)
139+
lastCollectedStatistics <- statistics
140+
stepsPlayed <- stepsPlayed + 1u<step>
141+
142+
match state with
143+
| Some state -> Some state
144+
| None ->
145+
incorrectPredictedStateId <- true
146+
oracle.Feedback(Feedback.IncorrectPredictedStateId stateId)
127147
None
128-
else
129-
let toPredict =
130-
match aiMode with
131-
| TrainingSendEachStep
132-
| TrainingSendModel ->
133-
if stepsPlayed > 0u<step> then
134-
gameStateDelta
135-
else
136-
gameState.Value
137-
| Runner -> gameState.Value
138-
139-
let stateId = oracle.Predict toPredict
140-
141-
afterFirstAIPeek <- true
142-
let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId)
143-
lastCollectedStatistics <- statistics
144-
stepsPlayed <- stepsPlayed + 1u<step>
145-
146-
match state with
147-
| Some state -> Some state
148-
| None ->
149-
incorrectPredictedStateId <- true
150-
oracle.Feedback(Feedback.IncorrectPredictedStateId stateId)
151-
None
152148

153149
static member updateGameState (delta: GameState) (gameState: Option<GameState>) =
154150
match gameState with

VSharp.ML.GameServer.Runner/Main.fs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -239,6 +239,7 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
239239
GameOver(
240240
explorationResult.ActualCoverage,
241241
explorationResult.TestsCount,
242+
explorationResult.StepsCount,
242243
explorationResult.ErrorsCount
243244
)
244245
)

VSharp.ML.GameServer/Messages.fs

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -109,11 +109,13 @@ type GameOverMessageBody =
109109
interface IRawOutgoingMessageBody
110110
val ActualCoverage: uint<percent>
111111
val TestsCount: uint32<test>
112+
val StepsCount: uint32<step>
112113
val ErrorsCount: uint32<error>
113114

114-
new(actualCoverage, testsCount, errorsCount) =
115+
new(actualCoverage, testsCount, stepsCount, errorsCount) =
115116
{ ActualCoverage = actualCoverage
116117
TestsCount = testsCount
118+
StepsCount = stepsCount
117119
ErrorsCount = errorsCount }
118120

119121
[<Struct>]
@@ -371,7 +373,7 @@ type IncorrectPredictedStateIdMessageBody =
371373
new(stateId) = { StateId = stateId }
372374

373375
type OutgoingMessage =
374-
| GameOver of uint<percent> * uint32<test> * uint32<error>
376+
| GameOver of uint<percent> * uint32<test> * uint32<step> * uint32<error>
375377
| MoveReward of Reward
376378
| IncorrectPredictedStateId of uint<stateId>
377379
| ReadyForNextStep of GameState
@@ -397,8 +399,8 @@ let deserializeInputMessage (messageData: byte[]) =
397399

398400
let serializeOutgoingMessage (message: OutgoingMessage) =
399401
match message with
400-
| GameOver(actualCoverage, testsCount, errorsCount) ->
401-
RawOutgoingMessage("GameOver", box (GameOverMessageBody(actualCoverage, testsCount, errorsCount)))
402+
| GameOver(actualCoverage, testsCount, stepsCount, errorsCount) ->
403+
RawOutgoingMessage("GameOver", box (GameOverMessageBody(actualCoverage, testsCount, stepsCount, errorsCount)))
402404
| MoveReward reward -> RawOutgoingMessage("MoveReward", reward)
403405
| IncorrectPredictedStateId stateId ->
404406
RawOutgoingMessage("IncorrectPredictedStateId", IncorrectPredictedStateIdMessageBody stateId)

0 commit comments

Comments
 (0)