Plan Builder Service and Back-to-Back Testing

[manthonyaiello]

This PR adds

• a SPARK implementation of the Plan Builder service, which proves at SPARK silver.
• unit-level, white-box back-to-back testing for the Plan Builder service that demonstrates functional match between the C++ and SPARK code.

Note: this PR should not be merged as-is, because the testing required breaking changes to the C++ implementation of the Plan Builder service. The PR is therefore marked as a draft. Once it's been reviewed, it should be closed with a note that it is inappropriate for merging - however we feel that the work is nevertheless interesting as a demonstration of research results.

To run the tests:

OpenUxAS$ ./anod build uxas
OpenUxAS$ ./anod build uxas-ada
OpenUxAS$ tests/ada/experiments/plan-builder-e2e-tests

There is a README.md in tests/ada/experiments.