獲取變量的首要/下一個狀態

Question

給定一些條件，我想檢查變量下一個狀態是否適用於某個命題。我無法創造出羅丹接受的東西。

我的確切情況是下面的不變。我想確保鎖定開啓時變量door不會改變。變量door或者是Open或Closed

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

如果PrimaryLock是On這意味着門狀態不會改變，不管未來會觸發什麼事件。

這是可能的使用事件b或我需要通過添加額外的變量來解決我的問題嗎？

Answer 1

目前，您可以指定關於狀態更改的屬性的唯一地方是事件本身。因此，您必須爲每個修改變量door的事件添加警衛PrimaryLock /= On。

如果你使用改進（你應該！:)，那麼這實際上並沒有那麼糟糕，因爲你指定了可能改變門的抽象事件，並且改進中的所有事件都必須遵循它們的規範。

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 

，並指定打開或關閉它作爲改進的事件。

我承認這將是一個很好的功能來表達所有事件的屬性。

Answer 2

您也可以使用Atelier B開發Event-B規格。 Rodin有一些變化，但原則保持不變。 對於您的問題，與工作室B，您可以按如下指定事件：

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

有，door和door$0代表值之前和事件之後。

您可以在規範的最抽象層次上有這樣的事件。然後，您將介紹一種改進方法，使用系統中可能會改變門的狀態的所有事件，並對這些事件進行改進door_change。

這個「技巧」允許指定關於系統中變量變化的屬性。不過，我不知道羅丹是否有這個功能。