"Failed to generate tests" on invariant violation in traces

[mortenhaahr]

When writing traces for combinatorial testing and accidentally violating a type invariant the message provided is non-explanatory and very difficult to debug in big systems.

System: VSCode for Ubuntu v1.73.1 (Debian)

Steps to reproduce:

1. Copy and paste the code below into a vdmpp file.
2. Go to "Combinatorial Testing" in the sidebar.
3. Press "Generate test outline".
4. Unfold "Test".
5. Click "Test`bad_message" and click "Generate Tests"
6. Observe that the error message given is "Failed to generate tests".

Suggested solution: Provide more information on where the error comes from. Ideally which invariant is violated and with which values.

class Test
types
public Point = nat1
    inv p == p < 9;

functions
    public assert_true : Point -> bool
    assert_true(p) == true
    post (true);

traces
    bad_message: (
        let p : Point = 9 in -- Invariant of Point violated. 
            assert_true(p);
    );
end Test

[nickbattle]

Good point! You can probably see what is happening here: the generation process is not linked to the debugger as an "execution" (it uses the LSP protocol rather than the DAP protocol to contact the language server), and hence when the constraint violation is encountered, it just pops out with an unhelpful error, rather than dropping into the debugger as it would if it was an execution.

So apologies for the trouble this probably caused.

Running the trace on the VDMJ command line is slightly better (and this is always something that is worth trying, when you have unusual issues). It reports:

Runtime: Error 4060: Type invariant violated for Point in 'Test' (piece.vdmpp) at line 13:13

So that's better, but if it was less obvious you would still be unable to debug the problem. I think the way forward here is to try to get the error text back to the Client somehow as a first step - crudely, we can use the "Output" window, or perhaps a popup notification.

But to enable generation to be debuggable, it has to use the DAP protocol. It may be possible to look at adding a "generate" command (we'll think of a better name) that would only be used in the circumstance where the trace expansion fails - this would be like the "runtrace" command that is used to debug individual expanded tests ("Send to Interpreter"). That's fairly crude, but at least there would be a way to debug trace expansion problems then.

The ideal solution would be to have the Combinatorial Testing UI use the DAP protocol for expansion, but that is a much harder thing to change.

I'll see what I can do...

[nickbattle]

I had a quick look at how to allow traces to be expanded within a debugging environment. It is possible, but it is quite a significant change. Getting a more sensible error messages back should be a lot easier.

I'll post updates here, if I get either of these ideas to work :)

[nickbattle]

I've added a couple of changes for this. It will (crudely) print the exception to stderr, which appears in the Output window. Then if this happens, there is a new command in the console called generate <trace name>. It (deliberately) doesn't appear in the help list, like runtrace, though that's easy to change. If you use this command, it will give you the full debug power of VSCode, so it will stop at the invariant violation and allow you to look at values etc.

Screen shot below. I'm still testing. It will appear in 4.5.0-SNAPSHOT, hopefully.

[nickbattle]

The standard error (console) output now indicates that you can debug the problem using the generate command:

Exception during trace expansion:

Error 4060: Type invariant violated for Point in 'Test' (/home/nick/vscode.tests/TestPP/CT.vdmpp) at line 13:13
You can debug this using the 'generate' console command

I think this is about as good as we can do, without more complex changes in the CT UI. Marking as fixed in VDMJ.

[nickbattle]

Incidentally, since the generate command is doing a debuggable execution, you can add breakpoints to traces and then step through them as they are expanded. The apparent order of evaluation might be confusing with more complex traces, as "inner" patterns are expanded multiple times because of "outer" patterns, but it is interesting to try this :-)

[nickbattle]

Closing this, as the "generate" does provide a way forward. It would be better for the UI to generate traces this way (or provide a way to debug generation), but that's an enhancement.