Issue 993: Fix tests and generation of SPARK test code

.github/workflows/tests.yml

@@ -99,7 +99,7 @@ jobs:
   installation:
     name: Installation
     needs: skip_check_general
-    if: ${{ needs.skip_check_python.outputs.should_skip != 'true' }}
+    if: ${{ needs.skip_check_general.outputs.should_skip != 'true' }}
     runs-on: ubuntu-20.04
     steps:
     - uses: actions/checkout@v2
@@ -464,7 +464,7 @@ jobs:
       - id: skip_check
         uses: fkirc/skip-duplicate-actions@v3.4.0
         with:
-          paths: '[".github/workflows/**", "*.gpr", "tests/spark/**"]'
+          paths: '[".github/workflows/**", "*.gpr", "rflx/**", "tests/**"]'
 
   verification_spark:
     name: Verification

tests/integration/specification_model_generator_test.py

@@ -446,9 +446,7 @@ def test_refinement_with_self(tmp_path: Path) -> None:
     )
 
 
-@pytest.mark.verification
-def test_definite_message_with_builtin_type(tmp_path: Path) -> None:
-    spec = """\
+DEFINITE_MESSAGE_WITH_BUILTIN_TYPE_SPEC = """\
        package Test is
 
           type Length is range 0 .. 2 ** 7 - 1 with Size => 7;
@@ -464,8 +462,17 @@ def test_definite_message_with_builtin_type(tmp_path: Path) -> None:
 
        end Test;
         """
-    utils.assert_compilable_code_string(spec, tmp_path)
-    utils.assert_provable_code_string(spec, tmp_path, units=["rflx-test-message"])
+
+
+def test_definite_message_with_builtin_type(tmp_path: Path) -> None:
+    utils.assert_compilable_code_string(DEFINITE_MESSAGE_WITH_BUILTIN_TYPE_SPEC, tmp_path)
+
+
+@pytest.mark.verification
+def test_definite_message_with_builtin_type_provability(tmp_path: Path) -> None:
+    utils.assert_provable_code_string(
+        DEFINITE_MESSAGE_WITH_BUILTIN_TYPE_SPEC, tmp_path, units=["rflx-test-message"]
+    )
 
 
 def test_message_expression_value_outside_type_range(tmp_path: Path) -> None:
@@ -538,9 +545,7 @@ def test_feature_integration(tmp_path: Path) -> None:
     utils.assert_compilable_code_specs([SPEC_DIR / "feature_integration.rflx"], tmp_path)
 
 
-@pytest.mark.verification
-def test_parameterized_message(tmp_path: Path) -> None:
-    spec = """\
+PARAMETERIZED_MESSAGE_SPEC = """\
         package Test is
 
            type Length is range 1 .. 2 ** 14 - 1 with Size => 16;
@@ -559,13 +564,20 @@ def test_parameterized_message(tmp_path: Path) -> None:
 
         end Test;
         """
-    utils.assert_compilable_code_string(spec, tmp_path)
-    utils.assert_provable_code_string(spec, tmp_path, units=["rflx-test-message"])
+
+
+def test_parameterized_message(tmp_path: Path) -> None:
+    utils.assert_compilable_code_string(PARAMETERIZED_MESSAGE_SPEC, tmp_path)
 
 
 @pytest.mark.verification
-def test_definite_parameterized_message(tmp_path: Path) -> None:
-    spec = """\
+def test_parameterized_message_provability(tmp_path: Path) -> None:
+    utils.assert_provable_code_string(
+        PARAMETERIZED_MESSAGE_SPEC, tmp_path, units=["rflx-test-message"]
+    )
+
+
+DEFINITE_PARAMETERIZED_MESSAGE_SPEC = """\
         package Test is
 
            type Length is range 1 .. 2 ** 14 - 1 with Size => 16;
@@ -578,8 +590,17 @@ def test_definite_parameterized_message(tmp_path: Path) -> None:
 
         end Test;
         """
-    utils.assert_compilable_code_string(spec, tmp_path)
-    utils.assert_provable_code_string(spec, tmp_path, units=["rflx-test-message"])
+
+
+def test_definite_parameterized_message(tmp_path: Path) -> None:
+    utils.assert_compilable_code_string(DEFINITE_PARAMETERIZED_MESSAGE_SPEC, tmp_path)
+
+
+@pytest.mark.verification
+def test_definite_parameterized_message_provability(tmp_path: Path) -> None:
+    utils.assert_provable_code_string(
+        DEFINITE_PARAMETERIZED_MESSAGE_SPEC, tmp_path, units=["rflx-test-message"]
+    )
 
 
 def test_session_type_conversion_in_assignment(tmp_path: Path) -> None:

tools/generate_spark_test_code.py

@@ -2,13 +2,16 @@
 
 """Generate the SPARK code for the test project and all feature tests."""
 
+from __future__ import annotations
+
 import filecmp
 import logging
-import sys
 from pathlib import Path
 
+from rflx.common import unique
 from rflx.generator import Generator
 from rflx.integration import Integration
+from rflx.model import Model, Session, Type
 from rflx.specification import Parser
 from tests.const import SPEC_DIR
 from tests.unit.generator_test import MODELS
@@ -35,17 +38,25 @@
 ]
 
 
-def main() -> int:
+def main() -> None:
+    generate_spark_tests()
+    generate_feature_tests()
+
+
+def generate_spark_tests() -> None:
+    remove_ada_files(OUTPUT_DIRECTORY)
+
     parser = Parser()
     parser.parse(*SPECIFICATION_FILES)
+    model = merge_models([parser.create_model(), *MODELS])
+    Generator(
+        "RFLX",
+        reproducible=True,
+        ignore_unsupported_checksum=True,
+    ).generate(model, Integration(), OUTPUT_DIRECTORY)
 
-    for model in [parser.create_model(), *MODELS]:
-        Generator(
-            "RFLX",
-            reproducible=True,
-            ignore_unsupported_checksum=True,
-        ).generate(model, Integration(), OUTPUT_DIRECTORY)
 
+def generate_feature_tests() -> None:
     generate(SHARED_DIRECTORY)
     shared_files = {f.name: f for f in (SHARED_DIRECTORY / "generated").iterdir()}
 
@@ -56,12 +67,13 @@ def main() -> int:
                 f.unlink()
                 f.symlink_to(f"../../shared/generated/{f.name}")
 
-    return 0
-
 
 def generate(feature_test: Path) -> None:
     output_directory = feature_test / "generated"
     output_directory.mkdir(exist_ok=True)
+
+    remove_ada_files(output_directory)
+
     parser = Parser()
     parser.parse(feature_test / "test.rflx")
     Generator(
@@ -71,5 +83,22 @@ def generate(feature_test: Path) -> None:
     ).generate(parser.create_model(), parser.get_integration(), output_directory)
 
 
+def remove_ada_files(directory: Path) -> None:
+    for f in directory.glob("*.ad?"):
+        print(f"Removing {f}")
+        f.unlink()
+
+
+def merge_models(models: list[Model]) -> Model:
+    types: list[Type] = []
+    sessions: list[Session] = []
+
+    for m in models:
+        types.extend(m.types)
+        sessions.extend(m.sessions)
+
+    return Model(list(unique(types)), list(unique(sessions)))
+
+
 if __name__ == "__main__":
-    sys.exit(main())
+    main()