PROSAGA码农传奇-数据防泄漏-检测数据泄漏？

我有一棵元素树。我从某些元素中收集数据，并使用该数据创建一组节点。我想要一个断言来检查，如果仅访问节点集，则不可能访问其他数据，例如树中其他元素中的数据。也就是说，我要确保没有数据泄漏。这是我的元素树：
<pre><code>sig Element {
 data: Data,
 children: set Element
}
</code></pre>我从一些元素中收集数据。我将数据填充到节点中：
<pre><code>sig Node {
 data: Data
}
</code></pre>如果某人只能访问节点集，则不会发生数据泄漏，因为节点仅包含从树中的元素故意收集的数据。但是，出于调试目的，我向Node添加了一个字段以引用作为Node数据源的Element：
<pre><code>sig Node {
 data: Data,
 represents: Element
}
</code></pre>通过偶然的监督，该represents领域并未撤出。现在，有权访问节点集的人员也可以访问树，因此可以看到比该人员更多的数据。因此，存在数据泄漏的可能性。我想创建一个断言，检查模型是否存在潜在的数据泄漏：
<pre><code>assert No_data_leakage { ??? }
</code></pre>直观地说，我希望断言这样说：在此模型的值的Universe中，仅有权访问节点集的人只能访问节点集中的数据值，而没有其他权限。我该如何表达？以下是我的模型的简化版本。
<pre><code>open util/ordering[Element]
open util/ordering[Node]

sig Element {
    data: Data,
    children: set Element
}
one sig Root extends Element {}

sig Data {}

sig Node {
    data: Data,
    represents: Element
}

fact No_disconnected_elements {
    all e: Element |
        (e = Root) or (e in Root.^children)
}

fact Each_element_has_one_parent {
    no disj e, e', e'': Element | 
        (e in e'.children) and (e in e''.children) 
}

fact No_loops {
    no e: Element | e in e.^children
}

fact First_Node_data_is_first_Element_data {
 (Node <: first).data = (Element <: first).data
 (Node <: first).represents = (Element <: first)
}

fact Last_Node_data_is_last_Element_data {
 (Node <: last).data = (Element <: last).data
 (Node <: last).represents = (Element <: last)
}

fact Every_element_has_different_data {
   no disj e, e': Element | e.data = e'.data
}

run {} for 3 but 2 Node

assert No_data_leaks {
 // How to express this?
}
</code></pre>