Skip to content

Commit 64b5bf5

Browse files
Anya497Anya497
committed
Reset dictionary with path condition vertices. Refactor.
1 parent 1dd6401 commit 64b5bf5

File tree

1 file changed

+88
-78
lines changed

1 file changed

+88
-78
lines changed

‎VSharp.ML.GameServer.Runner/Main.fs

+88-78
Original file line numberDiff line numberDiff line change
@@ -23,22 +23,22 @@ type ExplorationResult =
2323
val TestsCount: uint<test>
2424
val ErrorsCount: uint<error>
2525
val StepsCount: uint<step>
26+
2627
new(actualCoverage, testsCount, errorsCount, stepsCount) =
27-
{
28-
ActualCoverage = actualCoverage
29-
TestsCount = testsCount
30-
ErrorsCount = errorsCount
31-
StepsCount = stepsCount
32-
}
28+
{ ActualCoverage = actualCoverage
29+
TestsCount = testsCount
30+
ErrorsCount = errorsCount
31+
StepsCount = stepsCount }
3332

3433
type Mode =
3534
| Server = 0
3635
| Generator = 1
36+
3737
type CliArguments =
3838
| [<Unique>] Port of int
3939
| [<Unique>] DatasetBasePath of string
4040
| [<Unique>] DatasetDescription of string
41-
| [<Unique ; Mandatory>] Mode of Mode
41+
| [<Unique; Mandatory>] Mode of Mode
4242
| [<Unique>] OutFolder of string
4343
| [<Unique>] StepsToSerialize of uint
4444
| [<Unique>] UseGPU
@@ -62,21 +62,21 @@ type CliArguments =
6262
let mutable inTrainMode = true
6363

6464
let explore (gameMap: GameMap) options =
65-
let assembly =
66-
RunnerProgram.TryLoadAssembly <| FileInfo gameMap.AssemblyFullName
67-
let method =
68-
RunnerProgram.ResolveMethod (assembly, gameMap.NameOfObjectToCover)
69-
let statistics =
70-
TestGenerator.Cover (method, options)
65+
let assembly = RunnerProgram.TryLoadAssembly <| FileInfo gameMap.AssemblyFullName
66+
let method = RunnerProgram.ResolveMethod(assembly, gameMap.NameOfObjectToCover)
67+
let statistics = TestGenerator.Cover(method, options)
68+
7169
let actualCoverage =
7270
try
7371
let testsDir = statistics.OutputDir
7472
let _expectedCoverage = 100
75-
let exploredMethodInfo =
76-
AssemblyManager.NormalizeMethod method
73+
let exploredMethodInfo = AssemblyManager.NormalizeMethod method
74+
7775
let status, actualCoverage, message =
78-
VSharp.Test.TestResultChecker.Check (testsDir, exploredMethodInfo :?> MethodInfo, _expectedCoverage)
76+
VSharp.Test.TestResultChecker.Check(testsDir, exploredMethodInfo :?> MethodInfo, _expectedCoverage)
77+
7978
printfn $"Actual coverage for {gameMap.MapName}: {actualCoverage}"
79+
8080
if actualCoverage < 0 then
8181
0u<percent>
8282
else
@@ -85,7 +85,7 @@ let explore (gameMap: GameMap) options =
8585
printfn $"Coverage checking problem:{e.Message} \n {e.StackTrace}"
8686
0u<percent>
8787

88-
ExplorationResult (
88+
ExplorationResult(
8989
actualCoverage,
9090
statistics.TestsCount * 1u<test>,
9191
statistics.ErrorsCount * 1u<error>,
@@ -94,11 +94,12 @@ let explore (gameMap: GameMap) options =
9494

9595

9696
let loadGameMaps (datasetDescriptionFilePath: string) =
97-
let jsonString =
98-
File.ReadAllText datasetDescriptionFilePath
99-
let maps = ResizeArray<GameMap> ()
97+
let jsonString = File.ReadAllText datasetDescriptionFilePath
98+
let maps = ResizeArray<GameMap>()
99+
100100
for map in System.Text.Json.JsonSerializer.Deserialize<GameMap[]> jsonString do
101101
maps.Add map
102+
102103
maps
103104

104105
let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
@@ -111,6 +112,7 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
111112
serializeOutgoingMessage message
112113
|> System.Text.Encoding.UTF8.GetBytes
113114
|> ByteSegment
115+
114116
webSocket.send Text byteResponse true
115117

116118
let oracle =
@@ -123,87 +125,99 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
123125
| Feedback.ServerError s -> OutgoingMessage.ServerError s
124126
| Feedback.MoveReward reward -> OutgoingMessage.MoveReward reward
125127
| Feedback.IncorrectPredictedStateId i -> OutgoingMessage.IncorrectPredictedStateId i
128+
126129
do! sendResponse message
127130
}
131+
128132
match Async.RunSynchronously res with
129-
| Choice1Of2 () -> ()
133+
| Choice1Of2() -> ()
130134
| Choice2Of2 error -> failwithf $"Error: %A{error}"
131135

132136
let predict =
133137
let mutable cnt = 0u
138+
134139
fun (gameState: GameState) ->
135140
let toDot drawHistory =
136-
let file = Path.Join ("dot", $"{cnt}.dot")
141+
let file = Path.Join("dot", $"{cnt}.dot")
137142
gameState.ToDot file drawHistory
138143
cnt <- cnt + 1u
139144
//toDot false
140145
let res =
141146
socket {
142147
do! sendResponse (ReadyForNextStep gameState)
143148
let! msg = webSocket.read ()
149+
144150
let res =
145151
match msg with
146152
| (Text, data, true) ->
147153
let msg = deserializeInputMessage data
154+
148155
match msg with
149156
| Step stepParams -> (stepParams.StateId)
150157
| _ -> failwithf $"Unexpected message: %A{msg}"
151158
| _ -> failwithf $"Unexpected message: %A{msg}"
159+
152160
return res
153161
}
162+
154163
match Async.RunSynchronously res with
155164
| Choice1Of2 i -> i
156165
| Choice2Of2 error -> failwithf $"Error: %A{error}"
157166

158-
Oracle (predict, feedback)
167+
Oracle(predict, feedback)
159168

160169
while loop do
161170
let! msg = webSocket.read ()
171+
162172
match msg with
163173
| (Text, data, true) ->
164174
let message = deserializeInputMessage data
175+
165176
match message with
166177
| ServerStop -> loop <- false
167178
| Start gameMap ->
168179
printfn $"Start map {gameMap.MapName}, port {port}"
169180
let stepsToStart = gameMap.StepsToStart
170181
let stepsToPlay = gameMap.StepsToPlay
182+
171183
let aiTrainingOptions =
172-
{
173-
stepsToSwitchToAI = stepsToStart
174-
stepsToPlay = stepsToPlay
175-
defaultSearchStrategy =
176-
match gameMap.DefaultSearcher with
177-
| searcher.BFS -> BFSMode
178-
| searcher.DFS -> DFSMode
179-
| x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now."
180-
serializeSteps = false
181-
mapName = gameMap.MapName
182-
oracle = Some oracle
183-
}
184+
{ stepsToSwitchToAI = stepsToStart
185+
stepsToPlay = stepsToPlay
186+
defaultSearchStrategy =
187+
match gameMap.DefaultSearcher with
188+
| searcher.BFS -> BFSMode
189+
| searcher.DFS -> DFSMode
190+
| x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now."
191+
serializeSteps = false
192+
mapName = gameMap.MapName
193+
oracle = Some oracle }
194+
184195
let options =
185-
VSharpOptions (
196+
VSharpOptions(
186197
timeout = 15 * 60,
187198
outputDirectory = outputDirectory,
188199
searchStrategy = SearchStrategy.AI,
189200
aiAgentTrainingOptions = aiTrainingOptions,
190201
stepsLimit = uint (stepsToPlay + stepsToStart),
191202
solverTimeout = 2
192203
)
193-
let explorationResult =
194-
explore gameMap options
204+
205+
let explorationResult = explore gameMap options
195206

196207
Application.reset ()
197-
API.Reset ()
198-
HashMap.hashMap.Clear ()
208+
API.Reset()
209+
HashMap.hashMap.Clear()
210+
Serializer.pathConditionVertices.Clear()
211+
199212
do!
200213
sendResponse (
201-
GameOver (
214+
GameOver(
202215
explorationResult.ActualCoverage,
203216
explorationResult.TestsCount,
204217
explorationResult.ErrorsCount
205218
)
206219
)
220+
207221
printfn $"Finish map {gameMap.MapName}, port {port}"
208222
| x -> failwithf $"Unexpected message: %A{x}"
209223

@@ -215,65 +229,68 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
215229
}
216230

217231
let app port outputDirectory : WebPart =
218-
choose
219-
[
220-
path "/gameServer" >=> handShake (ws port outputDirectory)
221-
]
232+
choose [ path "/gameServer" >=> handShake (ws port outputDirectory) ]
222233

223234
let generateDataForPretraining outputDirectory datasetBasePath (maps: ResizeArray<GameMap>) stepsToSerialize =
224235
for map in maps do
225236
if map.StepsToStart = 0u<step> then
226237
printfn $"Generation for {map.MapName} started."
238+
227239
let map =
228-
GameMap (
240+
GameMap(
229241
map.StepsToPlay,
230242
map.StepsToStart,
231-
Path.Combine (datasetBasePath, map.AssemblyFullName),
243+
Path.Combine(datasetBasePath, map.AssemblyFullName),
232244
map.DefaultSearcher,
233245
map.NameOfObjectToCover,
234246
map.MapName
235247
)
248+
236249
let aiTrainingOptions =
237-
{
238-
stepsToSwitchToAI = 0u<step>
239-
stepsToPlay = 0u<step>
240-
defaultSearchStrategy = searchMode.BFSMode
241-
serializeSteps = true
242-
mapName = map.MapName
243-
oracle = None
244-
}
250+
{ stepsToSwitchToAI = 0u<step>
251+
stepsToPlay = 0u<step>
252+
defaultSearchStrategy = searchMode.BFSMode
253+
serializeSteps = true
254+
mapName = map.MapName
255+
oracle = None }
245256

246257
let options =
247-
VSharpOptions (
258+
VSharpOptions(
248259
timeout = 5 * 60,
249260
outputDirectory = outputDirectory,
250261
searchStrategy = SearchStrategy.ExecutionTreeContributedCoverage,
251262
stepsLimit = stepsToSerialize,
252263
solverTimeout = 2,
253264
aiAgentTrainingOptions = aiTrainingOptions
254265
)
266+
255267
let folderForResults =
256268
Serializer.getFolderToStoreSerializationResult outputDirectory map.MapName
269+
257270
if Directory.Exists folderForResults then
258-
Directory.Delete (folderForResults, true)
259-
let _ =
260-
Directory.CreateDirectory folderForResults
271+
Directory.Delete(folderForResults, true)
272+
273+
let _ = Directory.CreateDirectory folderForResults
261274

262275
let explorationResult = explore map options
263-
File.WriteAllText (
264-
Path.Join (folderForResults, "result"),
276+
277+
File.WriteAllText(
278+
Path.Join(folderForResults, "result"),
265279
$"{explorationResult.ActualCoverage} {explorationResult.TestsCount} {explorationResult.StepsCount} {explorationResult.ErrorsCount}"
266280
)
281+
267282
printfn
268283
$"Generation for {map.MapName} finished with coverage {explorationResult.ActualCoverage}, tests {explorationResult.TestsCount}, steps {explorationResult.StepsCount},errors {explorationResult.ErrorsCount}."
284+
269285
Application.reset ()
270-
API.Reset ()
271-
HashMap.hashMap.Clear ()
286+
API.Reset()
287+
HashMap.hashMap.Clear()
272288

273289
[<EntryPoint>]
274290
let main args =
275291
let parser =
276-
ArgumentParser.Create<CliArguments> (programName = "VSharp.ML.GameServer.Runner.exe")
292+
ArgumentParser.Create<CliArguments>(programName = "VSharp.ML.GameServer.Runner.exe")
293+
277294
let args = parser.Parse args
278295

279296
let mode = args.GetResult <@ Mode @>
@@ -298,19 +315,16 @@ let main args =
298315
| Some steps -> steps
299316
| None -> 500u
300317

301-
let useGPU =
302-
(args.TryGetResult <@ UseGPU @>).IsSome
318+
let useGPU = (args.TryGetResult <@ UseGPU @>).IsSome
303319

304-
let optimize =
305-
(args.TryGetResult <@ Optimize @>).IsSome
320+
let optimize = (args.TryGetResult <@ Optimize @>).IsSome
306321

307-
let outputDirectory =
308-
Path.Combine (Directory.GetCurrentDirectory (), string port)
322+
let outputDirectory = Path.Combine(Directory.GetCurrentDirectory(), string port)
309323

310324
if Directory.Exists outputDirectory then
311-
Directory.Delete (outputDirectory, true)
312-
let testsDirInfo =
313-
Directory.CreateDirectory outputDirectory
325+
Directory.Delete(outputDirectory, true)
326+
327+
let testsDirInfo = Directory.CreateDirectory outputDirectory
314328
printfn $"outputDir: {outputDirectory}"
315329

316330
match mode with
@@ -319,11 +333,7 @@ let main args =
319333
startWebServer
320334
{ defaultConfig with
321335
logger = Targets.create Verbose [||]
322-
bindings =
323-
[
324-
HttpBinding.createSimple HTTP "127.0.0.1" port
325-
]
326-
}
336+
bindings = [ HttpBinding.createSimple HTTP "127.0.0.1" port ] }
327337
(app port outputDirectory)
328338
with e ->
329339
printfn $"Failed on port {port}"

0 commit comments

Comments
 (0)