Refine settings for improved dumping of automata to files#787
Refine settings for improved dumping of automata to files#787bahnwaerter wants to merge 3 commits into
Conversation
This change refines the existing automata dumping settings to enable more detailed and configurable automata dump options. The enhanced settings align with the 'WitnessPrinter' settings and simplify the dump configuration in BenchExec runs, particularly for reuse interpolant automata (incremental verification). The change also introduces a standardized naming convention for the dumped files (using 'TaskIdentifier' for proper filename patterns).
bahnwaerter
force-pushed
the
wip/mb/improve-automata-dumping
branch
from
4dd4437 to
889af75
Compare
schuessf
left a comment
schuessf
left a comment
There was a problem hiding this comment.
I just had a quick look over these changes. Overall, it looks good, I have just a few comments.
| } | ||
|
|
||
| final String filename = mPref.dumpPath() + File.separator + mIcfg.getIdentifier() + "_" + iteration + ".bpl"; | ||
| final String filename = mPref.dumpAutomataDirectory() + File.separator + mIcfg.getIdentifier() + "_" + iteration + ".bpl"; |
There was a problem hiding this comment.
This line does not actually dump an automaton, but a path program. So maybe revert the name of this method to dumpPath (or something similar) again.
There was a problem hiding this comment.
That is indeed a special case. However, it was already like that in the previous implementation. Back then, the setting was internally called just dump path, but the exposed setting was named automata dump path. If the Dumper for the specific debug text information of each CEGAR iteration is no longer needed, we can remove it entirely (most Dumper methods aren't used anymore). @Heizmann do you agree to a removal?
There was a problem hiding this comment.
Alternatively, we could introduce a separate setting for this. But that leads to having more settings, which isn't so nice either.
There was a problem hiding this comment.
Okay, if this is not really needed anymore, you could also remove it.
I would definitely not introduce another setting for this. If we want to keep it, we could instead make this setting more general (as the previous dumpPath suggested; then also rename the corresponding settings label).
There was a problem hiding this comment.
I finally removed the obsolete Dumper that misused the automata dump settings. I hope @Heizmann and @maul-esel really don't need it anymore.
There was a problem hiding this comment.
I don't remember ever using Dumper.
But be careful: I wouldn't expect this kind of debug functionality to be called routinely. But it may still be useful to add calls to it when debugging a specific issue. Just because there are no calls in checked-in code doesn't mean it isn't used from time to time. 🤔
There was a problem hiding this comment.
So we should keep the Dumper after all?
If necessary, I can revert the removal and either misuse the automata dump settings or introduce another setting for the Dumper. What’s the plan?
The file dumper misused the automata dump settings to write CEGAR debug information to a text file. Since this is no longer needed, this change remove the obsolete dumper.
3 participants
This change refines the existing automata dumping settings to enable more detailed and configurable automata dump options. The enhanced settings align with the
WitnessPrintersettings and simplify the dump configuration in BenchExec runs, particularly for reuse interpolant automata (incremental verification). The change also introduces a standardized naming convention for the dumped files (usingTaskIdentifierfor proper filename patterns).