1

いくつかの条件が与えられたとき、変数の次の状態が何らかの命題に当てはまることを確認したいと思います。私はロダンが認めたものを作ることができませんでした。

私の正確なケースは、次の不変条件です。doorロックがオンのときに変数が変更されないようにしたい。変数doorは、OpenまたはClosed

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

これPrimaryLockはOn、次にどのイベントがトリガーされても、ドアの状態が変わらないことを意味します。

これは Event-b を使用して可能ですか、それとも変数を追加して問題を解決する必要がありますか?

4

2 に答える 2

1

現在、状態の変化に関するプロパティを指定できる唯一の場所は、イベント自体です。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

そして、それを開閉するイベントを絞り込みとして指定します。

すべてのイベントに対してこのようなプロパティを表現できれば、すばらしい機能になることは認めます。

于 2015-12-11T14:34:49.407 に答える