Use GameMap to communicate with server.

1. Use steps to specify start of game. Not coverage
2. AI training  options collected in separated type.
3. Provide ability to specify default searcher.

VSharp.API/VSharp.cs

@@ -188,10 +188,8 @@ private static Statistics StartExploration(
                     randomSeed: options.RandomSeed,
                     stepsLimit: options.StepsLimit,
                     oracle: options.Oracle,
-                    coverageToSwitchToAI:options.CoverageToSwitchToAI,
-                    stepsToPlay:options.StepsToPlay,
-                    serialize:options.Serialize,
-                    mapName:options.MapName);
+                    aiAgentTrainingOptions: options.AIAgentTrainingOptions
+                    );
 
             var fuzzerOptions =
                 new FuzzerOptions(

VSharp.API/VSharpOptions.cs

@@ -112,10 +112,7 @@ public readonly record struct VSharpOptions
     public readonly int RandomSeed = DefaultRandomSeed;
     public readonly uint StepsLimit = DefaultStepsLimit;
     public readonly Oracle? Oracle = null;
-    public readonly uint CoverageToSwitchToAI = 0;
-    public readonly uint StepsToPlay = 0;
-    public readonly string MapName = "";
-    public readonly bool Serialize = false;
+    public readonly AIAgentTrainingOptions? AIAgentTrainingOptions = null;
 
     /// <summary>
     /// Symbolic virtual machine options.
@@ -146,10 +143,7 @@ public VSharpOptions(
         int randomSeed = DefaultRandomSeed,
         uint stepsLimit = DefaultStepsLimit,
         Oracle? oracle = null,
-        uint coverageToSwitchToAI = 0,
-        uint stepsToPlay = 0,
-        string mapName = "",
-        bool serialize = false)
+        AIAgentTrainingOptions? aiAgentTrainingOptions = null)
     {
         Timeout = timeout;
         SolverTimeout = solverTimeout;
@@ -164,10 +158,7 @@ public VSharpOptions(
         RandomSeed = randomSeed;
         StepsLimit = stepsLimit;
         Oracle = oracle;
-        CoverageToSwitchToAI = coverageToSwitchToAI;
-        StepsToPlay = stepsToPlay;
-        MapName = mapName;
-        Serialize = serialize;
+        AIAgentTrainingOptions = aiAgentTrainingOptions;
     }
 
     /// <summary>

VSharp.Explorer/AISearcher.fs

@@ -5,14 +5,32 @@ open VSharp
 open VSharp.IL.Serializer
 open VSharp.ML.GameServer.Messages
 
-type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, stepsToPlay:uint) =
+type internal AISearcher(oracle:Oracle, aiAgentTrainingOptions: Option<AIAgentTrainingOptions>) =
+    let stepsToSwitchToAI =
+        match aiAgentTrainingOptions with
+        | None -> 0u<step>
+        | Some options -> options.stepsToSwitchToAI
+
+    let stepsToPlay =
+        match aiAgentTrainingOptions with
+        | None -> 0u<step>
+        | Some options -> options.stepsToPlay
+
     let mutable lastCollectedStatistics = Statistics()
+    let mutable defaultSearcherSteps = 0u<step>
     let mutable (gameState:Option<GameState>) = None
-    let mutable useDefaultSearcher = coverageToSwitchToAI > 0u
+    let mutable useDefaultSearcher = stepsToSwitchToAI > 0u<step>
     let mutable afterFirstAIPeek = false
     let mutable incorrectPredictedStateId = false
-    let defaultSearcher = BFSSearcher() :> IForwardSearcher  
-    let mutable stepsPlayed = 0u
+    let defaultSearcher =
+        match aiAgentTrainingOptions with
+        | None -> BFSSearcher() :> IForwardSearcher
+        | Some options ->
+            match options.defaultSearchStrategy with
+            | BFSMode -> BFSSearcher() :> IForwardSearcher
+            | DFSMode -> DFSSearcher() :> IForwardSearcher
+            | x -> failwithf $"Unexpected default searcher {x}. DFS and BFS supported for now."  
+    let mutable stepsPlayed = 0u<step>
     let isInAIMode () = (not useDefaultSearcher) && afterFirstAIPeek
     let q = ResizeArray<_>()
     let availableStates = HashSet<_>()
@@ -65,11 +83,12 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, stepsToPlay:
         states |> Seq.iter (availableStates.Add >> ignore)
     let reset () =
         defaultSearcher.Reset()
+        defaultSearcherSteps <- 0u<step>
         lastCollectedStatistics <- Statistics()
         gameState <- None
         afterFirstAIPeek <- false
         incorrectPredictedStateId <- false
-        useDefaultSearcher <- coverageToSwitchToAI > 0u
+        useDefaultSearcher <- stepsToSwitchToAI > 0u<step>
         q.Clear()
         availableStates.Clear()
     let update (parent, newSates) =
@@ -86,17 +105,20 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, stepsToPlay:
     let pick selector =
         if useDefaultSearcher
         then
+            defaultSearcherSteps <- defaultSearcherSteps + 1u<step>
             if Seq.length availableStates > 0
             then
                 let gameStateDelta = collectGameStateDelta ()                
                 updateGameState gameStateDelta
                 let statistics = computeStatistics gameState.Value
                 Application.applicationGraphDelta.Clear()
                 lastCollectedStatistics <- statistics
-                useDefaultSearcher <- (statistics.CoveredVerticesInZone * 100u) / statistics.TotalVisibleVerticesInZone  < coverageToSwitchToAI
+                useDefaultSearcher <- defaultSearcherSteps < stepsToSwitchToAI
             defaultSearcher.Pick()
         elif Seq.length availableStates = 0
         then None
+        elif Seq.length availableStates = 1
+        then Some (Seq.head availableStates)
         else
             let gameStateDelta = collectGameStateDelta ()
             updateGameState gameStateDelta
@@ -109,13 +131,11 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, stepsToPlay:
             if stepsToPlay = stepsPlayed
             then None
             else
-                let stateId, _ =
-                    let x,y = oracle.Predict gameState.Value
-                    x * 1u<stateId>, y
+                let stateId = oracle.Predict gameState.Value
                 afterFirstAIPeek <- true
                 let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId)                
                 lastCollectedStatistics <- statistics
-                stepsPlayed <- stepsPlayed + 1u
+                stepsPlayed <- stepsPlayed + 1u<step>
                 match state with
                 | Some state ->                
                     Some state

VSharp.Explorer/Explorer.fs

@@ -29,7 +29,9 @@ type private IExplorer =
 type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVMStatistics, reporter: IReporter) =
     let options = explorationOptions.svmOptions 
     let folderToStoreSerializationResult =
-        getFolderToStoreSerializationResult explorationOptions.outputDirectory.FullName options.mapName    
+        match options.aiAgentTrainingOptions with
+        | None -> ""
+        | Some options -> getFolderToStoreSerializationResult explorationOptions.outputDirectory.FullName options.mapName    
     let hasTimeout = explorationOptions.timeout.TotalMilliseconds > 0
 
     let solverTimeout =
@@ -78,7 +80,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
     let rec mkForwardSearcher mode =
         let getRandomSeedOption() = if options.randomSeed < 0 then None else Some options.randomSeed
         match mode with
-        | AIMode -> AISearcher(options.coverageToSwitchToAI, options.oracle.Value, options.stepsToPlay) :> IForwardSearcher
+        | AIMode -> AISearcher(options.oracle.Value, options.aiAgentTrainingOptions) :> IForwardSearcher
         | BFSMode -> BFSSearcher() :> IForwardSearcher
         | DFSMode -> DFSSearcher() :> IForwardSearcher
         | ShortestDistanceBasedMode -> ShortestDistanceBasedSearcher statistics :> IForwardSearcher
@@ -339,7 +341,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
         (* TODO: checking for timeout here is not fine-grained enough (that is, we can work significantly beyond the
                  timeout, but we'll live with it for now. *)
         while not isStopped && not <| isStepsLimitReached() && not <| isTimeoutReached() && pick() do
-            if options.serialize
+            if options.aiAgentTrainingOptions.IsSome && options.aiAgentTrainingOptions.Value.serializeSteps
             then
                 dumpGameState (System.IO.Path.Combine(folderToStoreSerializationResult, string firstFreeEpisodeNumber))
                 firstFreeEpisodeNumber <- firstFreeEpisodeNumber + 1

VSharp.Explorer/Options.fs

@@ -34,9 +34,26 @@ type FuzzerOptions = {
 
 [<Struct>]
 type Oracle =
-    val Predict: GameState -> uint*float
+    val Predict: GameState -> uint<stateId>
     val Feedback: Feedback -> unit
     new (predict, feedback) = {Predict=predict; Feedback = feedback}
+
+/// <summary>
+/// Options used in AI agent training.
+/// </summary>
+/// <param name="stepsToSwitchToAI">Number of steps of default searcher prior to switch to AI mode.</param>
+/// <param name="stepsToPlay">Number of steps to play in AI mode.</param>
+/// <param name="defaultSearchStrategy">Default searcher that will be used to play few initial steps.</param>
+/// <param name="serializeSteps">Determine whether steps should be serialized.</param>
+/// <param name="mapName">Name of map to play.</param>
+type AIAgentTrainingOptions =
+    {
+        stepsToSwitchToAI: uint<step>
+        stepsToPlay: uint<step>
+        defaultSearchStrategy: searchMode
+        serializeSteps: bool
+        mapName: string    
+    }
 
 type SVMOptions = {
     explorationMode : explorationMode
@@ -51,10 +68,7 @@ type SVMOptions = {
     randomSeed : int
     stepsLimit : uint
     oracle: Option<Oracle>
-    coverageToSwitchToAI: uint
-    stepsToPlay: uint
-    serialize: bool
-    mapName: string
+    aiAgentTrainingOptions: Option<AIAgentTrainingOptions>
 }
 
 type explorationModeOptions =

VSharp.IL/CFG.fs

@@ -368,7 +368,7 @@ and CfgInfo internal (method : MethodWithBody, getNextBasicBlockGlobalId: unit -
     do
         let startVertices =
             [|
-             yield 0<offsets>
+             yield 0<byte_offset>
              for handler in exceptionHandlers do
                  yield handler.handlerOffset
                  match handler.ehcType with

VSharp.IL/ILRewriter.fs

@@ -1078,7 +1078,7 @@ type ILRewriter(body : rawMethodBody, m : MethodBase) =
 
         // TODO: unify code with Instruction.fs (parseInstruction)
         let mutable branch = false
-        let mutable offset = 0<offsets>
+        let mutable offset = 0<byte_offset>
         let codeSize : offset = Offset.from codeSize
         while offset < codeSize do
             let startOffset = offset
@@ -1088,11 +1088,11 @@ type ILRewriter(body : rawMethodBody, m : MethodBase) =
             let size =
                 match op.OperandType with
                 | OperandType.InlineNone
-                | OperandType.InlineSwitch -> 0<offsets>
+                | OperandType.InlineSwitch -> 0<byte_offset>
                 | OperandType.ShortInlineVar
                 | OperandType.ShortInlineI
-                | OperandType.ShortInlineBrTarget -> 1<offsets>
-                | OperandType.InlineVar -> 2<offsets>
+                | OperandType.ShortInlineBrTarget -> 1<byte_offset>
+                | OperandType.InlineVar -> 2<byte_offset>
                 | OperandType.InlineI
                 | OperandType.InlineMethod
                 | OperandType.InlineType
@@ -1101,9 +1101,9 @@ type ILRewriter(body : rawMethodBody, m : MethodBase) =
                 | OperandType.InlineTok
                 | OperandType.ShortInlineR
                 | OperandType.InlineField
-                | OperandType.InlineBrTarget -> 4<offsets>
+                | OperandType.InlineBrTarget -> 4<byte_offset>
                 | OperandType.InlineI8
-                | OperandType.InlineR -> 8<offsets>
+                | OperandType.InlineR -> 8<byte_offset>
                 | _ -> __unreachable__()
 
             if offset + size > codeSize then invalidProgram "IL stream unexpectedly ended!"
@@ -1133,10 +1133,10 @@ type ILRewriter(body : rawMethodBody, m : MethodBase) =
             | OperandType.InlineR ->
                 instr.arg <- Arg64 <| BitConverter.ToInt64(code, int offset)
             | OperandType.ShortInlineBrTarget ->
-                instr.arg <- offset + 1<offsets> + (code.[int offset] |> sbyte |> int |> Offset.from) |> int |> Arg32
+                instr.arg <- offset + 1<byte_offset> + (code.[int offset] |> sbyte |> int |> Offset.from) |> int |> Arg32
                 branch <- true;
             | OperandType.InlineBrTarget ->
-                instr.arg <- offset + 4<offsets> + NumberCreator.extractOffset code offset |> int |> Arg32
+                instr.arg <- offset + 4<byte_offset> + NumberCreator.extractOffset code offset |> int |> Arg32
                 branch <- true;
             | OperandType.InlineSwitch ->
                 let sizeOfInt = Offset.from sizeof<int>

VSharp.IL/MethodBody.fs

@@ -334,10 +334,10 @@ type MethodWithBody internal (m : MethodBase) =
 
 module MethodBody =
 
-    let private operandType2operandSize = [| 4<offsets>; 4<offsets>; 4<offsets>; 8<offsets>; 4<offsets>
-                                             0<offsets>; -1<offsets>; 8<offsets>; 4<offsets>; 4<offsets>
-                                             4<offsets>; 4<offsets>; 4<offsets>; 4<offsets>; 2<offsets>
-                                             1<offsets>; 1<offsets>; 4<offsets>; 1<offsets>|]
+    let private operandType2operandSize = [| 4<byte_offset>; 4<byte_offset>; 4<byte_offset>; 8<byte_offset>; 4<byte_offset>
+                                             0<byte_offset>; -1<byte_offset>; 8<byte_offset>; 4<byte_offset>; 4<byte_offset>
+                                             4<byte_offset>; 4<byte_offset>; 4<byte_offset>; 4<byte_offset>; 2<byte_offset>
+                                             1<byte_offset>; 1<byte_offset>; 4<byte_offset>; 1<byte_offset>|]
 
     let private jumpTargetsForNext (opCode : OpCode) _ (pos : offset) =
         let nextInstruction = pos + Offset.from opCode.Size + operandType2operandSize[int opCode.OperandType]
@@ -364,9 +364,9 @@ module MethodBody =
     let private inlineSwitch (opCode : OpCode) ilBytes (pos : offset) =
         let opcodeSize = Offset.from opCode.Size
         let n = NumberCreator.extractUnsignedInt32 ilBytes (pos + opcodeSize) |> int
-        let nextInstruction = pos + opcodeSize + 4<offsets> * n + 4<offsets>
+        let nextInstruction = pos + opcodeSize + 4<byte_offset> * n + 4<byte_offset>
         let nextOffsets =
-            List.init n (fun x -> nextInstruction + Offset.from (NumberCreator.extractInt32 ilBytes (pos + opcodeSize + 4<offsets> * (x + 1))))
+            List.init n (fun x -> nextInstruction + Offset.from (NumberCreator.extractInt32 ilBytes (pos + opcodeSize + 4<byte_offset> * (x + 1))))
         ConditionalBranch(nextInstruction, nextOffsets)
 
     let private jumpTargetsForReturn _ _ _ = Return

VSharp.IL/OpCodes.fs

@@ -233,9 +233,7 @@ type OpCodeValues =
     | Refanytype        = 0xFE1Ds
     | Readonly_         = 0xFE1Es
 
-[<Measure>]
-type offsets
-type offset = int<offsets>
+type offset = int<byte_offset>
 module Offset =
     let from (x : int) : offset = LanguagePrimitives.Int32WithMeasure x
 

VSharp.IL/Serializer.fs

@@ -269,7 +269,7 @@ let collectGameState (basicBlocks:ResizeArray<BasicBlock>) =
             currentBasicBlock.AssociatedStates
             |> Seq.map (fun s ->
                 State(s.Id,
-                      uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1<offsets>,
+                      (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1<byte_offset>) * 1u<byte_offset>,
                       s.PathConditionSize,
                       s.VisitedAgainVertices,
                       s.VisitedNotCoveredVerticesInZone,
@@ -289,7 +289,7 @@ let collectGameState (basicBlocks:ResizeArray<BasicBlock>) =
         GameMapVertex(
             currentBasicBlock.Id,
             currentBasicBlock.IsGoal,
-            uint <| currentBasicBlock.FinalOffset - currentBasicBlock.StartOffset + 1<offsets>,
+            uint <| currentBasicBlock.FinalOffset - currentBasicBlock.StartOffset + 1<byte_offset>,
             currentBasicBlock.IsCovered,
             currentBasicBlock.IsVisited,
             currentBasicBlock.IsTouched,