0

我是 Event-B 的初学者，我正在尝试建模一台机器，其中集合 PERSONNE 包含集合 CLIENT，集合 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 次）......

4

1 回答 1

1

There is a problem in your specification that is very common for beginners in Event-B. :)

You have introduced three deferred sets PERSONNE, CLIENT and RESIDENT. But I think a client or a resident are persons, too. And all deferred sets are constants, so with this construction, you're not able to modify your set of clients or residents.

I think the basic problem is the keyword SETS. You do not have to specify all sets of your machine there. Think TYPES! You just introduce a new type (I think you need only PERSONNE here) and have a constant for all elements.

context contexteHumain
sets PERSONNE

So remove the sets CLIENT and RESIDENT. I would suggest to remove all axioms, too. Do you really have to assume that the set of possible persons is finite?

Adapt your invariants:

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

Remove inv7 and inv8. You probably want to add an invariant that the set of persons in your system is finite (in contrast to all possible persons in PERSONNE):

@inv9: finite(pers)

Accordingly, you would adapt your guards:

@gr1: futur_resident ∈ cli

resp.

@gr1: resident_actuel ∈ res
于 2015-04-27T15:07:43.513 回答