0

私はイベント B の初心者であり、セット PERSONNE にセット RESIDENT を含むセット CLIENT が含まれるマシンをモデル化しようとしています... ロダンのドキュメントを検索しましたが、何も見つかりませんでした.. . コンテキストは次のとおりです

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

あなたの仕様には、Event-B の初心者によくある問題があります。:)

3 つの据え置きセット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
于 2015-04-27T15:07:43.513 に答える