-
Notifications
You must be signed in to change notification settings - Fork 5
removing pathConditionRoot from the states #98
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
gsvgit
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fix edges addition between state and PathCondition.
VSharp.Explorer/AISearcher.fs
Outdated
|
|
||
| index_pcToState.[firstFreePositionInPcToState] <- | ||
| int64 pathConditionVerticesIds[state.PathCondition.Id] | ||
| int64 pathConditionVerticesIds[state.PathCondition.[firstFreePositionInPcToState]] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks strange. You should add edges between state and all vertices in state.PathCondition.
VSharp.ML.GameServer/Messages.fs
Outdated
| | StandardFunctionApplication = 45 | ||
| | Cast = 46 | ||
| | Combine = 47 | ||
| | PathConditionRoot = 48 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This line can be removed too.
VSharp.IL/Serializer.fs
Outdated
| ) | ||
|
|
||
| pathConditionDelta.Add pathConditionRoot | ||
| let pathConditionId = [| for p in pathCondition -> termsWithId.[p] |] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why "id"? Why not just pathCondition?
VSharp.Explorer/AISearcher.fs
Outdated
| |> Array.iteri (fun i pcId -> | ||
| let j = firstFreePositionInPcToState + i | ||
| index_pcToState[j] <- int64 pathConditionVerticesIds[pcId] | ||
| index_pcToState[numOfParentOfEdges + j] <- int64 stateIds[state.Id]) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why so strange position in index_pcToState to write?
VSharp.Explorer/AISearcher.fs
Outdated
| let shapeOfPcToState = [| 2L; gameState.States.Length |] | ||
| let index_pcToState = Array.zeroCreate (2 * gameState.States.Length) | ||
|
|
||
| let pathConditionNum = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would be better to move pathConditionNum calculation closer to this line to prevent redundant iterations over states. Look at the numOfParentOfEdges calculation.
Anya497
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good job!
removed pathConditionRoot from the states