Turn integration tests into behavior-driven tests

Goal

We should analyze the existing integration tests, design an improved test architecture on the foundation of Cucumber, and implement that.

Issue

Currently, integration tests are implemented as simple quarkus integration tests in Java. But our tests require large inputs that are difficult to read within code: input programs, specifications, configurations. So we read these inputs from files instead, like this:

            Arguments.of(
                "verification: result true",
                Cpachecker.StartRunRequest.newBuilder()
                    .setProgramCode(getContentAsString(PROGRAM_TRUE))
                    .setConfig(getContentAsString(CONFIG_VERIFICATION))
                    .setSpecification(getContentAsString(SPECIFICATION))
                    .setMachineModel(Cpachecker.MachineModel.LINUX32)
                    .build(),
                /* expectedVerdict= */ Cpachecker.Verdict.TRUE),

This makes the tests difficult to read, because you always have to look up the content of the files to get the full picture.

To improve on this, we could use behavior-driven tests with cucumber.

Technical Details

The cucumber step definitions may reuse the existing code, IF useful.

First steps

After you are familiar with CPA-Daemon (setup and execute), you should implement a proof of concept and plan the further steps.

Proof of Concept

To start, make yourself familiar with Cucumber (documentation) and Gherkin, Cucumber's language for writing behavior-driven tests.

Then add cucumber to this project's build.gradle and create directory src/integrationTest/resource/features/. This will contain all our Gherkin feature specifications.

Write a first feature file src/integrationTest/resource/features/001-runVerification.feature. This file should contain a Gherkin Feature with a Scenario that describes the existing integration test testStartRun_validRequests with these inputs:

            Arguments.of(
                "verification: result true",
                Cpachecker.StartRunRequest.newBuilder()
                    .setProgramCode(getContentAsString(PROGRAM_TRUE))
                    .setConfig(getContentAsString(CONFIG_VERIFICATION))
                    .setSpecification(getContentAsString(SPECIFICATION))
                    .setMachineModel(Cpachecker.MachineModel.LINUX32)
                    .build(),
                /* expectedVerdict= */ Cpachecker.Verdict.TRUE),

Please make proposals for useful step definitions.

After that you can start implementing (documentation) the defined step definitions in a new Java file src/integrationTest/java/org/sosy_lab/cpachecker/grpc/testing/StepDefinitions.java.

Planning

Analyze the existing integration tests in src/integrationTest/java (they are often written as parameterized tests) and design the Cucumber step definitions that will be necessary to replace these tests. Please do this in an AsciiDoc-File that can later be used as documentation of the integration tests, and communicate your ideas through a merge request.