-
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
base: mlSearcher
Are you sure you want to change the base?
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?
| parentOf[j] <- int64 stateIds[state.Id] | ||
| parentOf[numOfParentOfEdges + j] <- int64 stateIds[children]) | ||
|
|
||
| firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length |
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 like you missed firstFreePositionInParentsOf updating step.
| state.PathCondition | ||
| |> Array.iteri (fun i pcId -> | ||
| let j = firstFreePositionInPcToState + i | ||
| index_pcToState[j] <- int64 pathConditionVerticesIds[pcId] |
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 like you forgot to update firstFreePositionInPcToState.
| |> 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?
removed pathConditionRoot from the states