Check if message type is empty after merging

Ref. #410
AdaCore · Aug 25, 2020 · bf52e03 · bf52e03
1 parent 39e3109
commit bf52e03
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 1 deletion.
diff --git a/rflx/model.py b/rflx/model.py
@@ -9,7 +9,7 @@
 
 from rflx.common import flat_name, generic_repr, indent, indent_next
 from rflx.contract import ensure, invariant
-from rflx.error import Location, RecordFluxError, Severity, Subsystem
+from rflx.error import Location, RecordFluxError, Severity, Subsystem, fail
 from rflx.expression import (
     TRUE,
     UNDEFINED,
@@ -1925,6 +1925,14 @@ def prune_dangling_states(
             }
 
             structure, types = prune_dangling_states(structure, types)
+            if not structure or not types:
+                fail(
+                    f'empty message type when merging field "{field.identifier}"',
+                    Subsystem.MODEL,
+                    Severity.ERROR,
+                    field.identifier.location,
+                )
+
             message = message.copy(structure=structure, types=types)
 
         return message

diff --git a/tests/test_model.py b/tests/test_model.py
@@ -1368,6 +1368,38 @@ def test_merge_message_constrained() -> None:
     assert merged == expected
 
 
+def test_merge_message_constrained_empty() -> None:
+    m1 = UnprovenMessage(
+        "P.M1",
+        [
+            Link(INITIAL, Field("F1")),
+            Link(Field("F1"), Field("F2"), Equal(Variable("F1"), Variable("True"))),
+            Link(Field("F1"), FINAL, Equal(Variable("F1"), Variable("False"))),
+            Link(Field("F2"), FINAL, Equal(Variable("F2"), Variable("True"))),
+        ],
+        {Field("F1"): BOOLEAN, Field("F2"): BOOLEAN},
+    )
+    m2 = UnprovenMessage(
+        "P.M2",
+        [
+            Link(INITIAL, Field("F3")),
+            Link(
+                Field("F3"),
+                FINAL,
+                And(
+                    Equal(Variable("F3_F1"), Variable("True")),
+                    Equal(Variable("F3_F2"), Variable("False")),
+                ),
+            ),
+        ],
+        {Field("F3"): m1},
+    )
+    with pytest.raises(
+        RecordFluxError, match=r'^model: error: empty message type when merging field "F3"$',
+    ):
+        m2.merged()
+
+
 def test_merge_message_error_name_conflict() -> None:
     m2_f2 = Field(ID("F2", Location((10, 5))))