Skip to content

fixed random search where only one path is explored even with limit > 1 #212

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

Merged
merged 2 commits into from
Nov 13, 2019
Merged

fixed random search where only one path is explored even with limit > 1 #212

merged 2 commits into from
Nov 13, 2019

Conversation

richardnnn
Copy link

@richardnnn richardnnn commented Nov 7, 2019

Right now the RandomSearch always returns after finishing one path, this PR tries to fix this problem and allow it to explore mutiple paths specified by search.RandomSearch.path_limit. The previous code will fail the added test but should pass after merged.

Now after cg.randomize_choices set to not NONE , the search will randomly try different paths.

@ankushdesai
Copy link

@cyrille-artho This pull request fixes a bug in RandomSearch implementation.

@cyrille-artho
Copy link
Member

Thank you very much for finding and fixing this as well as adding a test.
If you don't mind, would you please remove commented-out code as well as the extra line break that you inserted?

Copy link
Member

@cyrille-artho cyrille-artho left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See my comment: Please clean up the patch by removing commented-out code and extra whitespace.

@cyrille-artho cyrille-artho merged commit 26e11d1 into javapathfinder:master Nov 13, 2019
@cyrille-artho
Copy link
Member

Thank you very much! I have merged the two patches into one and merged it.

@richardnnn
Copy link
Author

Happy to help :)

varad64 pushed a commit to varad64/jpf-core that referenced this pull request Aug 12, 2023
cyrille-artho pushed a commit that referenced this pull request Aug 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants