diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 49a450b38..fe79c1027 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -361,8 +361,12 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Array.sumBy(fun s -> s.PathCondition.Length) + let shapeOfPcToState = [| 2L; pathConditionNum |] + let index_pcToState = Array.zeroCreate (2 * pathConditionNum) let shapeOfHistoryAttributes = [| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |] @@ -383,13 +387,13 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Array.iteri (fun i pcId -> + let j = firstFreePositionInPcToState + i + index_pcToState[j] <- int64 pathConditionVerticesIds[pcId] + index_pcToState[pathConditionNum + j] <- int64 stateIds[state.Id]) + + firstFreePositionInPcToState <- firstFreePositionInPcToState + state.PathCondition.Length state.History |> Array.iteri (fun i historyElem -> diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index 81550267b..9a7857b6e 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -495,20 +495,13 @@ let collectGameState (basicBlocks: ResizeArray) filterStates process for term in pathCondition do pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices) - let pathConditionRoot = - PathConditionVertex( - id = getFirstFreePathConditionVertexId (), - pathConditionVertexType = pathConditionVertexType.PathConditionRoot, - children = [| for p in pathCondition -> termsWithId.[p] |] - ) - - pathConditionDelta.Add pathConditionRoot + let pathCondition = [| for p in pathCondition -> termsWithId.[p] |] State( s.Id, (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) * 1u, - pathConditionRoot, + pathCondition, s.VisitedAgainVertices, s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone, diff --git a/VSharp.ML.GameServer/Messages.fs b/VSharp.ML.GameServer/Messages.fs index 7f13570f7..d85a49f0c 100644 --- a/VSharp.ML.GameServer/Messages.fs +++ b/VSharp.ML.GameServer/Messages.fs @@ -72,7 +72,6 @@ type pathConditionVertexType = | StandardFunctionApplication = 45 | Cast = 46 | Combine = 47 - | PathConditionRoot = 48 [] @@ -153,7 +152,7 @@ type StateHistoryElem = type State = val Id: uint val Position: uint // to basic block id - val PathCondition: PathConditionVertex + val PathCondition: array> val VisitedAgainVertices: uint val VisitedNotCoveredVerticesInZone: uint val VisitedNotCoveredVerticesOutOfZone: uint