Is your feature request related to a problem? Please describe.
batch-tamarin very helpfully stores traces (counterexamples, exist-traces) in json and dot output during analysis.
However, these are only directly accessible in the resulting file sets, and there is no obvious way to get to them unless the user inspects those files. Even then, the user typically first needs to convert them to a human-readable format.
Describe the solution you'd like
When viewing the batch-tamarin html summary page, for each proven exists-trace lemma or falsified forall lemma, the user should be able to click on a button to view the trace.
Describe alternatives you've considered
SVG is preferred over a bitmap format to enable better zooming on large graphs.
Additional context
This can be implemented directly if the user has graphviz installed, for example by using dot to generate svg files from the dot files. These can then be linked from the summary page.
Is your feature request related to a problem? Please describe.
batch-tamarin very helpfully stores traces (counterexamples, exist-traces) in json and dot output during analysis.
However, these are only directly accessible in the resulting file sets, and there is no obvious way to get to them unless the user inspects those files. Even then, the user typically first needs to convert them to a human-readable format.
Describe the solution you'd like
When viewing the batch-tamarin html summary page, for each proven exists-trace lemma or falsified forall lemma, the user should be able to click on a button to view the trace.
Describe alternatives you've considered
SVG is preferred over a bitmap format to enable better zooming on large graphs.
Additional context
This can be implemented directly if the user has graphviz installed, for example by using
dotto generate svg files from the dot files. These can then be linked from the summary page.