Diagnostic traces with UPPAAL 4.1.20-stratego-9

[pacalet]

I am testing UPPAAL 4.1.20-stratego-9 (rev. 67D95DBCE6B8B4ED), January 2022, macOS version. I cannot find a way to generate a counter-example trace from the verifier in the GUI.

I checked the Some option of the Engine Options / Diagnostic Trace menu, my property is the kind of property for which a counter-example trace makes sense: A[] a+b <= 6, and it fails. But I do not see any button or menu item to export a counter-example trace in the Verifier tab.

So I thought that the export to the simulator could be somehow automatic, as explained in the documentation but there is nothing like a counter-example trace in the symbolic or concrete simulator.

I checked with verifyta -f trace -t 0 model.xml (same verifyta version as the GUI): it generates a trace.

What am I doing wrong in the GUI or where is this button/menu item that I did not find yet?

[yrke]

Hi

If I understand you correctly,

When running a query with a diagnostic trace (given one is found), you should see a popup like this:

When answering yes the found trace will be opened in the Symbolic Simulator tab, you can then switch to the trace and inspect it. You can also export the trace using the "Save" button in the lower left corner.

I hope this helps you,

Regards, Kenneth

[pacalet]

I tested under Debian 11.2 (Bullseye) and yes, this popup appears. Then I tested again under macOS (Monterey 12.1) and no, there is no such popup, not even hidden by other windows. This looks like a bug. Shall I open an issue?

[yrke]

Yes, that would be very helpful, and thanks for letting us know.