Fix code generation for boolean relations with global variables

Ref. #1059

rflx/expression.py

@@ -1103,6 +1103,22 @@ def z3expr(self) -> z3.ExprRef:
             return -z3.Int(self.name)
         return z3.Int(self.name)
 
+    def copy(
+        self,
+        identifier: StrID = None,
+        negative: bool = None,
+        immutable: bool = None,
+        type_: rty.Type = None,
+        location: Location = None,
+    ) -> Variable:
+        return self.__class__(
+            ID(identifier) if identifier is not None else self.identifier,
+            negative if negative is not None else self.negative,
+            immutable if immutable is not None else self.immutable,
+            type_ if type_ is not None else self.type_,
+            location if location is not None else self.location,
+        )
+
 
 TRUE = Variable("True", type_=rty.BOOLEAN)
 FALSE = Variable("False", type_=rty.BOOLEAN)

rflx/generator/session.py

@@ -258,7 +258,10 @@ def _create_context(self) -> Tuple[List[ContextItem], List[ContextItem]]:
         if self._allocator.required:
             declaration_context.append(WithClause(self._prefix * self._allocator.unit_identifier))
 
-        if self._session_context.used_types or self._session_context.used_types_body:
+        if any(
+            t.parent not in [INTERNAL_PACKAGE, BUILTINS_PACKAGE]
+            for t in [*self._session_context.used_types, *self._session_context.used_types_body]
+        ):
             declaration_context.append(WithClause(self._prefix * const.TYPES_PACKAGE))
 
         body_context: List[ContextItem] = [
@@ -3419,27 +3422,51 @@ def func(expression: expr.Expr) -> expr.Expr:
                 and isinstance(expression.right, expr.Variable)
             ):
                 if expression.left == expr.Variable("True"):
-                    return expression.right
+                    return expression.right.copy(
+                        identifier=variable_id(expression.right.identifier, is_global)
+                    )
                 if expression.right == expr.Variable("True"):
-                    return expression.left
+                    return expression.left.copy(
+                        identifier=variable_id(expression.left.identifier, is_global)
+                    )
                 if expression.left == expr.Variable("False"):
-                    return expr.Not(expression.right)
+                    return expr.Not(
+                        expression.right.copy(
+                            identifier=variable_id(expression.right.identifier, is_global)
+                        )
+                    )
                 if expression.right == expr.Variable("False"):
-                    return expr.Not(expression.left)
+                    return expr.Not(
+                        expression.left.copy(
+                            identifier=variable_id(expression.left.identifier, is_global)
+                        )
+                    )
 
             if (
                 isinstance(expression, expr.NotEqual)
                 and isinstance(expression.left, expr.Variable)
                 and isinstance(expression.right, expr.Variable)
             ):
                 if expression.left == expr.Variable("True"):
-                    return expr.Not(expression.right)
+                    return expr.Not(
+                        expression.right.copy(
+                            identifier=variable_id(expression.right.identifier, is_global)
+                        )
+                    )
                 if expression.right == expr.Variable("True"):
-                    return expr.Not(expression.left)
+                    return expr.Not(
+                        expression.left.copy(
+                            identifier=variable_id(expression.left.identifier, is_global)
+                        )
+                    )
                 if expression.left == expr.Variable("False"):
-                    return expression.right
+                    return expression.right.copy(
+                        identifier=variable_id(expression.right.identifier, is_global)
+                    )
                 if expression.right == expr.Variable("False"):
-                    return expression.left
+                    return expression.left.copy(
+                        identifier=variable_id(expression.left.identifier, is_global)
+                    )
 
             if isinstance(expression, (expr.Equal, expr.NotEqual)) and isinstance(
                 expression.left.type_, rty.Enumeration
@@ -3526,13 +3553,7 @@ def func(expression: expr.Expr) -> expr.Expr:
                 _unsupported_expression(expression, "in expression")
 
             if isinstance(expression, expr.Variable):
-                return expr.Variable(
-                    variable_id(expression.identifier, is_global),
-                    expression.negative,
-                    expression.immutable,
-                    expression.type_,
-                    expression.location,
-                )
+                return expression.copy(identifier=variable_id(expression.identifier, is_global))
 
             return expression
 

tests/integration/specification_model_generator_test.py

@@ -858,3 +858,37 @@ def test_session_external_debug_output(debug: Debug, expected: str, tmp_path: Pa
     )
 
     assert utils.assert_executable_code(model, integration, tmp_path, debug=debug) == expected
+
+
+@pytest.mark.parametrize(
+    "global_rel, local_rel",
+    [("Global", "Local"), ("Global = True", "Local = True"), ("Global = False", "Local = False")],
+)
+def test_session_boolean_relations(global_rel: str, local_rel: str, tmp_path: Path) -> None:
+    spec = f"""
+        package Test is
+
+           generic
+           session Session with
+              Initial => Init,
+              Final => Terminated
+           is
+              Global : Boolean := False;
+           begin
+              state Init is
+                 Local : Boolean := False;
+              begin
+                 Global := {local_rel};
+                 Local := {global_rel};
+              transition
+                 goto Terminated
+                    if {global_rel} and {local_rel}
+                 goto Terminated
+              end Init;
+
+              state Terminated is null state;
+           end Session;
+
+        end Test;
+    """
+    utils.assert_compilable_code_string(spec, tmp_path)