Adding support to generate counterexamples' .dot graphs in automatic mode

[claudiacauli]

I'm working on an application that needs to fetch a counterexample dependency graph (if any) and do some post-processing on it. I'm happy with the counterexample trace that is found by autoprove, but the cex's .dot file seems to be generated only in interactive mode. I skimmed through the code and it seems that indeed the .dot generation is triggered only when clicking from browser.

Is there another way to get a counterexample's .dot that I'm missing?
If not, can the generation of the .dot be supported also when using the --prove flag?

Thanks!

[cascremers]

Hi, Sorry, this is a feature that is on our todo list, but no one has picked it up yet. Note that for post-processing it might be more efficient to use the json output that can be generated in parallel. (Same issue though, currently only for the interactive GUI mode.) Maybe someone is around who would like to pick this up? (graph json & dot output in non-interactive mode) Best, Cas

…

On Wed, Feb 8, 2023 at 1:25 PM Claudia Cauli ***@***.***> wrote: I'm working on an application that needs to fetch a counterexample dependency graph (if any) and do some post-processing on it. I'm happy with the counterexample trace that is found by *autoprove*, but the cex's .dot file seems to be generated only in interactive mode. I skimmed through the code and it seems that indeed the .dot generation is triggered only when clicking from browser. Is there another way to get a counterexample's .dot that I'm missing? If not, can the generation of the .dot be supported also when using the --prove flag? Thanks! — Reply to this email directly, view it on GitHub <#523>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALJWOE5FQ5HUPDTBVKFPK3WWOGDPANCNFSM6AAAAAAUVGDOYY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[claudiacauli]

Thanks for your fast response!

I found a little trick that seems to work from cli without using any browser.
It simulates accessing URLs from cli (and it works as the naming of the web URLs seems to follow a precise pattern).

I share the idea here in case it's helpful to others:

1. Run the Tamarin command, e.g. tamarin-prover interactive FILENAME.spthy --prove=LEMMA_NAME .
2. The server is started on some port, in my case http://127.0.0.1:3001.
3. Trigger autoprove by curling the URL: curl http://127.0.0.1:3001/thy/trace/NUMBER/autoprove/idfs/0/proof/LEMMA_NAME. I have the impression that NUMBER depends on how many other theory files are contained in the same folder. I have only one, so my number = 1.
4. The curl command of (3) returns a .json object with a redirect field, e.g. {"redirect":"/thy/trace/NUMBER+1/overview/proof/LEMMA_NAME/_/STEPSPATH"}. Let's call this redirectLink.
5. Replace overview with graph in the redirectLink and curl this new link to a file: curl http://127.0.0.1:3001/thy/trace/NUMBER+1/graph/proof/LEMMA_NAME/_/STEPSPATH -o CEX.png
6. The counterexample .png is now saved on the CEX.png file AND both the .dot and .png can be found in Tamarin's temporal cache folder (${TMPDIR}tamarin-prover-cache-${USER}).

Obviously, this might not work in most conditions and it would be much better if there was an option to fetch the graphs in non-interactive mode.

Thanks!