event-b - 获取变量的主要/下一个状态

Question

给定一些条件，我想检查变量下一个状态是否适用于某个命题。我无法创造出罗丹接受的东西。

我的确切情况是以下不变量。我想确保door当锁打开时变量永远不会改变。变量door是Open或者Closed

inv4: PrimaryLock = On ⇒ door :∣ door' = door

如果PrimaryLock是On这意味着无论接下来触发什么事件，门的状态都不会改变。

这可以使用 Event-b 还是我需要通过添加其他变量来解决我的问题？

score 1 · Accepted Answer

目前，您可以指定有关状态更改的属性的唯一位置是事件本身。因此，您必须为PrimaryLock /= On每个修改变量的事件添加保护door。

如果你使用细化（你应该！:)，那么这实际上并没有那么糟糕，因为你指定了可能改变门的抽象事件，并且细化中的所有事件都必须遵循它们的规范。

open_door  = WHEN PrimaryLock /= On THEN door := Open   END
close_door = WHEN PrimaryLock /= On THEN door := Closed END

不细化open_door或close_door隐式细化的细化中的新事件skip不允许改变门状态。因此，如果open_door和close_door是抽象规范中唯一改变变量的事件door，door则只能在未锁定的情况下在细化中进行修改。

你可以用更抽象的方式指定它

change_door_status = WHEN PrimaryLock /= On THEN door :: {Open,Closed} END

并将打开或关闭它的事件指定为细化。

我承认为所有事件表达此类属性将是一个不错的功能。

score 0 · Accepted Answer

您也可以使用 Atelier B 来开发 Event-B 规范。罗丹有一些变化，但原则保持不变。对于您的问题，使用 Atelier B，您可以指定一个事件，如下所示：

door_change = BEGIN
  door :( door : { Open, Closed } & 
    (PrimaryLock = On => doors = doors$0
  )
END

在那里，door并door$0代表事件之前和之后的价值观。

您可以在规范的最抽象级别上拥有这样的事件。然后，您引入系统中所有可能改变门状态的事件的细化，并使此类事件细化door_change。

这种“技巧”允许人们指定有关系统中变量变化的属性。不过，我不知道此功能在罗丹中是否可用。

2 回答 2