Получение простого / следующего состояния переменной

Учитывая некоторое условие, я хочу проверить, что переменное следующее состояние выполняется для некоторого предложения. Я не смог создать то, что Роден принял.

Мой точный случай - следующий инвариант. Я хочу убедиться, что переменная door никогда не меняется, когда включена блокировка. Переменная door либо Open или же Closed

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

Если PrimaryLock является On это означает, что состояние двери не изменится, независимо от того, какое событие будет вызвано следующим.

Возможно ли это с помощью Event-b или мне нужно решить мою проблему, добавив дополнительные переменные?

Источник

2 ответа

Решение

В настоящее время единственное место, где вы можете указать свойства об изменениях состояния, - это сами события. Таким образом, вы должны добавить охрану 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

и укажите события, которые открывают или закрывают его как уточнения.

Я признаю, что было бы неплохо выразить такие свойства для всех событий.

Источник

Вы также можете использовать Atelier B для разработки спецификаций Event-B. Есть некоторые вариации в отношении Родена, но принципы остаются теми же. Для вашей проблемы, с Atelier B, вы можете указать событие следующим образом:

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

Там, door а также door$0 стоять за значения до и после события.

Вы можете иметь такое событие на самом абстрактном уровне спецификации. Затем вы вводите уточнение со всеми событиями вашей системы, которые могут изменить состояние двери, и сделать такие события уточненными. door_change,

Этот "трюк" позволяет указать свойства, касающиеся изменений переменных в системе. Однако я не знаю, доступна ли эта функция в Rodin.

Источник
Другие вопросы по тегам