Open
Conversation
0dfc4b7 to
6843761
Compare
Member
|
We should add an actual test to the testing harness that merges the nodes and makes assertions about them. For example, it should be added to this test harness that the node merging is happening correctly: https://github.com/runtimeverification/kontrol/blob/master/src/tests/integration/test_foundry_prove.py#L236 |
Contributor
Author
Contributor
|
@nwatson22 brought up another challenge in adding this example to our test suite: the merge node functionality requires the user to accurately specify nodes to be merged, and it might be nontrivial to identify and add such nodes to the kcfg in this example. This should be partially addressed in #163, but it requires additional changes and is not being worked on at the moment. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a test with a high branching factor in order to test new features like node merging and branch parallelization.
The test splits into 8 branches in total (and this can be increased by increasing the length of the
proofarray). It takes 1h to run on my machine.