Платформа Родена Event-B, отношение Подмножества моделирования

Question

Я новичок в Event-B, и я пытаюсь смоделировать машину, где набор PERSONNE включает в себя набор CLIENT, который включает в себя набор RESIDENT... Я искал документацию Родена, но ничего не нашел.. Вот контекст

context contexteHumain

sets PERSONNE CLIENT RESIDENT

axioms
  @axm1; finite(PERSONNE)
  @axm2; finite(CLIENT)
  @axm3; finite(RESIDENT) // Definition of three possible sets

а вот и машина

machine machineFunKeyHotel sees contexteHumain

variables
    pers
    reserv
    cli
    resid
    chkin
    chkout

invariants
    @inv1: pers ⊆ PERSONNE
    @inv2: cli ⊆ CLIENT
    @inv3: resid ⊆ RESIDENT
// Définis les 3 variables d'ensemble de Personnes, Clients et Résidents
    @inv4: reserv ∈ BOOL
    @inv5: chkin ∈ BOOL
    @inv6: chkout ∈ BOOL
// Les paramètres booléens si la ⦂personne a réservé, check-in ou check-out.
    @inv7: CLIENT ⊆ PERSONNE
    @inv8: RESIDENT ⊆ CLIENT
// Et les relations entre les différnets ensembles d'humains·

events
  event INITIALISATION
  begin
    @act1: reserv ≔ FALSE
    @act2: chkin ≔ FALSE
    @act3: chkout ≔ FALSE
// Ces valeurs sont à faux, en effet, au début personne n'a ni réservé ni check-in
// Encore moins check out.
    @act4: resid ≔ ∅
    @act5: cli ≔ ∅
// Au début le nombre de client et de résidents sont zéro
    @act6: pers ≔ ∅ //???
// Définir un nombre de personne presqu'infini (Personnes sur terre estimé à
// 7 290 477 807 personnes le vendredi 3 avril 2015 à 9 h 07 min et 24 s (GTM +1)
  end

  event réserver
// Lorsqu'une personne quelconque a réservé ça implique quelle soit ajoutée
// à l'ensemble clients.
    any potentiel_client
    where
      @gr1: potentiel_client ∈ PERSONNE
      @gr2: reserv = TRUE
    then
      @act1: cli ≔ cli ∪ {potentiel_client}
  end

  event checkerin
// Lorsqu'un client a passé l'étape de check-in, cela implique qu'il est ajouté
// à l'ensemble résident
    any futur_resident
    where
      @gr1: futur_resident ∈ CLIENT
      @gr2: chkin = TRUE
    then
      @act1: resid ≔ resid ∪ {futur_resident}
  end

  event checkerout
// Lorsqu'un résident a procédé au check out cela implique qu'il est retiré
// et de l'ensemble client et de l'ensemble résident.
    any resident_actuel
    where
      @gr1: resident_actuel ∈ RESIDENT
      @gr2: chkout = TRUE
    then
      @act1: resid ≔ resid ∖ {resident_actuel}
      @act2: cli ≔ cli ∖ {resident_actuel}
  end
end

Я думаю, у меня есть идея, но я не могу решить, как решить различные ошибки, которые я получаю: типы CLIENT и PERSONNE не совпадают (3 раза) Типы RESIDENT и CLIENT не совпадают (2 раза)...

Answer 1

В вашей спецификации есть проблема, которая очень часто встречается у новичков в Event-B.:)

Вы ввели три отложенных набора PERSONNE, CLIENT а также RESIDENT, Но я думаю, что клиент или резидент тоже люди. И все отложенные наборы являются константами, поэтому с этой конструкцией вы не сможете изменять свой набор клиентов или резидентов.

Я думаю, что основной проблемой является ключевое слово SETS, Вам не нужно указывать все комплекты вашей машины там. Считать TYPES! Вы просто вводите новый тип (я думаю, что вам нужно только PERSONNE здесь) и есть константа для всех элементов.

context contexteHumain
sets PERSONNE

Так что снимайте наборы CLIENT а также RESIDENT, Я бы посоветовал удалить все аксиомы тоже. Вы действительно должны предполагать, что множество возможных людей конечно?

Адаптируйте ваши инварианты:

invariants
  @inv1: pers ⊆ PERSONNE
  @inv2: cli ⊆ pers
  @inv3: resid ⊆ cli

Удалить inv7 а также inv8, Возможно, вы захотите добавить инвариант, чтобы набор людей в вашей системе был конечным (в отличие от всех возможных людей в PERSONNE):

@inv9: finite(pers)

Соответственно, вы бы адаптировали своих охранников:

@gr1: futur_resident ∈ cli

соответственно

@gr1: resident_actuel ∈ res