event-b - Event-B 总功能证明义务

Question

我有如下问题：A定义了一个集合并且X具有不变类型的总函数

X ∈ A --> BOOL

和一个事件A_setSate：

A_setSate =
  WHEN X(A) = TRUE
  THEN X(A) := FALSE

问题是证明义务事件保存（INV）A_setState不能保存不变量X∈ A--> BOOL：

我知道这是因为不变量不够强，但我无法创建更强的不变量。

完整示例：示例截图

Answer 1

该示例看起来正确。

请检查是否安装了 Atelier B 验证器，罗丹手册包含相关说明。

（在评论中进行了一些澄清后，此答案已更新。）