Add flags for graphical output of exploration #24
Conversation
This file contains 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
margnus1
force-pushed
the
trace-dump
branch
7 times, most recently
from
259b4d2
to
e16a432
Compare
It is thus renamed IIDVCSeqTrace.
For now, the utility functions that were shared have been made public on Trace.
TraceRecorder now stores which messages correspond to a certain event, which allows them to be shown in the exploration tree.
This is an attempted fix aimed at a perceived flaw in --dump-spec, in that it generates specs that are "technically correct", by only matching one trace due to containing IIDs that are unique to that trace, but "miss the point" in what characterises the trace. This change does sometimes result in larger specs, but hopefully closer to what a human would write.
They are also used by TraceDumper, even when HAVE_BOOST_UNIT_TEST_FRAMEWORK is undefined.
Open
Open
|
I'm unlikely to have the time to work on features like this. If anyone likes it, feel free to take up the mantle. |
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.
This PR adds three flags.
--dump-traceswrites a graphviz graph of the happens-before order of all explored traces to a file.--dump-treewrites a graphviz graph of the exploration tree to a file.--dump-specwrites a minimalDPORDriver_test::trace_set_specof all explored equivalence classes to a file.Missing features:
--show-races, that draws red edges in the exploration tree of all races that had a reversal scheduled.