modeling - 事件 B，形式化建模：如何将集合的所有元素影响到关系

Question

我在使用 Event-B 时遇到了很多麻烦。

我想将一组客户与每个客户编号建立关系

我有这种类型的关系：

cli(PERSON) = NAT1 （人是有限集）

如果我有一部分人

where group <: PERSON

我想影响 cli 关系我会直观地写什么：

! x . x : group | cli(x) = numcli

我是否以正确的方式建模？有什么方法可以得到我想要的矫揉造作吗？

Answer 1

我有点猜测你想要实现什么：cli将一个人映射到一个数字：

VARIABLES
  cli
INVARIANTS
  cli : PERSON +-> NAT1

您想要一个事件（我们称之为ev）分配给一组人（称为group）相同的号码：

ev = ANY
  group, numcli
WHERE
  group <: PERSON
  numcli : NAT1
THEN
  cli := cli <+ (group**{numcli})
END

group ** {numcli}是一组对（关系），其中第一个元素是 的元素，group第二个是numcli. 运算符<+（关系覆盖）从第一个元素的右操作数中删除所有元素，cli并添加右操作数。即groupin的映射cli被替换或添加到到 的映射中numcli。