diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 8ca789acf..f597e15a5 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -41,7 +41,8 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo edges.AddRange delta.Map let activeStates = vertices |> Seq.collect (fun v -> v.States) |> HashSet let states = - s.States |> Array.filter (fun s -> activeStates.Contains s.Id && (not <| updatedStates.Contains s.Id)) + s.States + |> Array.filter (fun s -> activeStates.Contains s.Id && (not <| updatedStates.Contains s.Id)) |> Array.map (fun s -> State(s.Id , s.Position , s.PredictedUsefulness diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs index b693df596..89de71ed3 100644 --- a/VSharp.Explorer/Explorer.fs +++ b/VSharp.Explorer/Explorer.fs @@ -303,13 +303,13 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM goodStates @ iieStates @ errors | _ -> sIsStopped <- true - goodStates @ iieStates @ errors - Application.moveState loc s (Seq.cast<_> newStates) + goodStates @ iieStates @ errors for newState in newStates do let historyCopy = System.Collections.Generic.Dictionary<_,_>() for kvp in s._history do historyCopy.Add(kvp.Key, kvp.Value) newState._history <- historyCopy s.children <- s.children @ newStates + Application.moveState loc s (Seq.cast<_> newStates) statistics.TrackFork s newStates searcher.UpdateStates s newStates if sIsStopped then diff --git a/VSharp.IL/CFG.fs b/VSharp.IL/CFG.fs index aa9306a21..6d1d66877 100644 --- a/VSharp.IL/CFG.fs +++ b/VSharp.IL/CFG.fs @@ -708,6 +708,8 @@ module Application = let terminateState (state: IGraphTrackableState) = // TODO: gsv: propagate this into application graph let removed = state.CodeLocation.BasicBlock.AssociatedStates.Remove state + let added = applicationGraphDelta.TouchedBasicBlocks.Add state.CodeLocation.BasicBlock + let added = applicationGraphDelta.TouchedStates.Add state visualizer.TerminateState state let addCallEdge = graph.AddCallEdge diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index 7f0e061f8..5510ee593 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -246,7 +246,7 @@ let collectGameState (basicBlocks:ResizeArray) (serialize: bool) = s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone, s.History |> Seq.map (fun kvp -> StateHistoryElem(kvp.Key.Id, kvp.Value)) |> Array.ofSeq, - s.Children |> Array.map (fun s -> s.Id) |> Array.filter activeStates.Contains + s.Children |> Array.map (fun s -> s.Id) // |> Array.filter activeStates.Contains ) |> allStates.Add |> ignore diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index fee14abf2..7421fccf1 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -447,10 +447,8 @@ module CilState = let clone = { x with state = x.state } let mkCilState state' = if LanguagePrimitives.PhysicalEquality state' x.state then x - else - let s = clone.Copy(state') - s.internalId <- getNextStateId() - s + else clone.Copy(state') + StatedConditionalExecution x.state conditionInvocation (fun state k -> thenBranch (mkCilState state) k) (fun state k -> elseBranch (mkCilState state) k) @@ -486,7 +484,7 @@ module CilState = // -------------------- Changing inner state -------------------- member x.Copy(state : state) = - { x with state = state } + { x with state = state ;internalId = getNextStateId(); children = [] } // This function copies cilState, instead of mutation member x.ChangeState state' : cilState =