Shai: Support returning structured verification data in RPC responses

[shonfeder]

With #2138 in place, we now have support for nearly all important CLI functions (test and simulate are really just calls to check with some pre-determined configs.

However, we are currently only able to reply with:

• A parsed TLA Module if the operation succeeds
• A message with an error code if the operation fails

We now need to adjust the architecture of the pass chains so we can get back key output like counter-examples, and structured information about key kinds of errors.

• Identify the outputs needed by MBT in Atomcraft
  • looks to be mainly only the logs output and traces
• Draft plan for returning this data from the PassChainExecutor
  • Add class to represent a counter example #2185
• Make changes to PassChainExecutor
• Use returned data to return data from RPC

[shonfeder]

For returning the logging data, Igor suggested we just a log-appender, that we can register with our current logging system. Then we just need to get the counter-example (and maybe some ancillary data) out of the pass chain. I think that should be pretty straight forward :)

[shonfeder]

After reviewing the log configuration code, and thinking things over a bit, it doesn't look like we can simply add a log appender with the current architecture -- at least not if we intend the server to be able to handle concurrent requests. In the current architecture, the logger collects output from all threads, and I don't see an immediately obvious way of segregating the logging output into different pass chain executions without pretty pervasive alterations to the architecture.

This leads me to think we should instead focus on collecting the useful data during the pass chain execution, rather than trying to dump all the logs into an RPC response. It should be easier to implement, and will give better quality data in response too, I think.

[andrey-kuprianov]

@shonfeder I have a general request, with the particular instance for this case. When asking the questions like "Identify the outputs needed by MBT in Atomcraft", could you please ask us these questions directly? I don't remember being asked that, and I don't see where the answer "looks to be mainly only the logs output and traces" comes from... In particular, I don't actually think this is what we want. What we want is:

• either a short description of an error, preferably with pointers to concrete locations in the input files.
• or a counterexample trace, if we are talking about the check operation.

In general, would be really great to have a joint meeting and discuss this. Let's try to set up one

[shonfeder]

Hi, Andrey! We should definitely make time to discuss MBT needs. I'll get an invite out.

In the proper order of things the final version of the RPC data returned should absolutely be based on requirements gathered from your side. In the future I'll loop MBT in on issues that aim to meet MBT requirements!

In this case, the work has been proceeding with less rigorous planning or status updates than optimal. The checked off TODO item you're referring to is misleading: the actual data currently being returned in #2186 is much closer to what you're requesting, and this issue has ended up being more about returning some data at all from the Apalache passes, rather than about returning the data in RPC in its final form.

Certainly, I had every intention of consulting with MBT prior to declaring the data returned sufficient :)

[andrey-kuprianov]

Ok, great to hear:) yes, async communication saves lots of time, but can also misleading in some cases, as the complete context is missing. I am looking forward to a sync meeting, and after that we should have the right communication balance for the future. Thanks, Shon!

[shonfeder]

async communication saves lots of time, but can also misleading in some cases, as the complete context is missing

True! Tho I can and should also improve my ticket tracking hygiene so it served better as a way to communicate and coordinate with MBT work. Thanks for pointing out the deficiency here.