"Send to Interpreter" re-expands all tests

[nickbattle]

If you expand a combinatorial trace, and then right-click and attempt to execute just one test (using "Send to Interpreter"), all of the tests are re-expanded before running the single test identified - though the test does then run as expected. The traces console displays the number of tests expanded.

This isn't noticeable with small numbers of tests, but if a trace expands to 10,000 tests or more, there is a significant delay before a single test can be re-executed. Each test is just a sequence of operation calls, so it should be possible to run an individual trace without re-expanding the whole set. This was wrong in 2.3.4, but I'm pretty sure this used to work correctly at some point.

[peterwvj]

I'm not sure how this is handled so I would need to check the code.

Anyway, I need to make sure I understand what you are saying. Are you suggesting that once the trace has been expanded, by running a full evaluation, Overture should cache the test sets such that a second expansion isn't needed?

[nickbattle]

Yes, I'm assuming that after the expansion, there is enough information available to execute each test "stand alone" - it would amount to saving the content of the CallSequence types. I know the XML we save for the results is perhaps too little for this - for example, the variable bindings are not saved (true?).

So I'm not sure of the best approach, but if the only way that I can debug that one-in-a-million test that fails is to re-generate the one million tests, that isn't very practical.

Thinking of it from a code generation perspective, it's almost as though "Send to Interpreter" would use the test description to "write a test in VDM" that is then parsed and executed for that one combination of calls and variables.

It looks like the code is currently calling the Interpreter'runtrace method with a test number. That is how VDMJ command line would run (say) just test 1234, but then VDMJ does not save a cache of test results for presentation to the user. So it has to expand all the tests in order to discover what test 1234 is :-)

[peterwvj]

Once the trace has been expanded we could store the resulting TestSequence in a map that associates trace definitions with test sequences. Then, if the user sends a test to the interpreter, we should be able use the latest TestSequence without having to re-generate it (assuming we know from which trace the single test originates). A binary representation of the test sequences is probably memory efficient and it can in principle be serialized/de-serialized to/from the file system using the Java API.

What do you think?

[nickbattle]

If you mean an in-memory map, then that associated would disappear between Overture runs? If the test sequence was held in the results XML, then as long as the results were preserved on file, the individual tests would be re-runnable? Or we could just use a separate serialised file, as you say, but when would you save it?

[peterwvj]

Yeah I'm not sure how easy it is to re-run the tests if we only have the XML. I guess I would need some way to rebuild the test (CallSequence?) again from that? That's why I thought it might be easier to store the TestSequence. Again, I'm unsure about how this works. If we can store the tests in a (static?) map that would maybe be easiest. I'm not sure when I would persist the TestSequence to file. I only thought about it as a way to reduce RAM usage.

[peterwvj]

Any thoughts on how to construct the test from the XML?

[nickbattle]

Perhaps it would be easiest to construct an expression in VDM directly from the XML, and then parse it and evaluate it? Most tests would be like "let x = expression in ( op(x); op2(x) )". A CallSequence is just a list of TraceVariables and CallStatements, so the variables create "lets" and the calls are just calls.

[peterwvj]

Okay I see what you mean. Maybe that works if the XML contains all the information we need. I'm not sure it includes trace variables though.

[nickbattle]

Right, it probably just has the "flattened" version, like "op(1); op2(1)" with the variables substituted. But that is not "safe" for re-running (other bugs pointed this out). So as well as the flattened form, we would also have to store the "full form", perhaps in VDM already.

Just thinking out loud :-)

[peterwvj]

You are very right. My problem is just how and where we store it. As I see it there are two ways to do this

1. Let's say we store the TestSequence in the project folder (the full forms). I think that's possible. Then in order to send a test to the interpreter we would need some way to build an expression from the corresponding CallSequence - a string - that we send to the debugger/interpreter. Is there an easy way to convert a CallSequence (trace variables and trace statements) to an equivalent expression that can be send to the interpreter?
2. Originally I thought about having the DBGPReaderV2 reader store the TestSequences in a data structure using a static field such that TestSequences would not dissapear between runs. I'm not wild about this since it involves use of static variables. However, if the TestSequence is stored on the server side then it should in principle suffice to only send the trace name and the test number. My point is that then we can avoid converting the CallSequence into an expression.

Any thoughts?

[nickbattle]

We should also be careful of not slowing down the test generation time, by creating re-executable VDM expressions that (most of the time) people don't want to execute. I don't think converting a CallSequence to VDM is hard, but it might add a lot of time if multiplied by 1,000,000 over a test expansion. Could it be (Java) serialised and written in base64 to the XML file? Though that might be just as slow as converting to VDM source. I thnk it's "just" a matter of the variables turning into "let name= value in (...)", and the op calls just being themselves (their toStrings would be good enough?).

I think we really need the testability to survive an Overture restart. With very large test numbers, people will want to close down and look at error cases later.

[peterwvj]

I don't think we need to convert all the CallSequences to VDM. Only the one we need to send to the interpreter. Let's say we have serialised the entire TestSequence and we want to execute test n. Then we de-serialise the TestSequence and convert CallSequence n to VDM and debug that VDM expression.

Assuming we have the trace let x in set {1,2} in op(x) that would generate two tests

x = 1; op(1) -- Test 1
x = 2; op(2) -- Test 2

But the arguments passed to the operation have been replaced by their value, right? How does that affect the conversion? Are you sure the toString of the operation calls are good enough?

[nickbattle]

If arguments have been converted, the (as above) the "let x=1" would be redundant, but the conversion could still be "let x=1 in (op(1))" instead of "let x=1 in (op(x))". We don't convert the arguments in some circumstances though, so we still need the lets in place.

[peterwvj]

Okay. So assuming that we add the "lets" then the toString of the operation calls should be fine right?

[nickbattle]

I think that's true, yes.

[peterwvj]

More input on this:

A (single) test is send to the interpreter using the Launch method, shown below, which is located in the TraceDebugLauncher class.

public void Launch(IVdmProject project, TraceInfo traceInfo, Integer traceNumber)

This method builds a launch configuration that instructs the debugger to execute the test (traceNumber really should've been named "testNumber").

For now let's assume that we have the CallSequence that represents the test we want to execute and that we can also generate the corresponding VDM expression e. Then we would need to update the Launch method to construct a different looking launch configuration that instructs the debugger to execute e.

For this to work I think we need to update the interpreter to, in addition to the XML file, also produce a file that contains a serialised version of the TestSequence that can be de-serialised in order to get hold of the CallSequence from which the VDM expression, e, is generated.