0

合金の Web サイトで、署名がセットを定義することを読みました。この定義を考えると、私は以下の合金コードを理解しようとしていました:

enum dooroptype { unlocked, locked, opened}
enum enginetype {on,off}
enum motortype { ismoving, still}
enum key_location { in_car, faralone}

abstract sig state{
  inside,far, near : set Person,
  car_action : motortype,
  engine : enginetype,
  key_position : (Person + key_location),
  door : dooroptype
}

署名が実際にセットを定義する場合、セットが単項関係であるのに、署名定義に非常に多くのパラメーターがあるのはなぜですか? 私が間違っているとすれば、この定義をどのように解釈するのでしょうか。

4

2 に答える 2

3

私は合金で最初の一歩を踏み出していますが、答えようとします. これは、上記のコードにあるものです。

  1. dooroptype = セット (単項関係) で正確に 3 つのアトム。
  2. enginetype = set (単項関係) で正確に 2 つのアトム。
  3. motortype = 正確に 2 つのアトムを持つセット (単項関係)。
  4. key_location = 正確に 2 つのアトムで設定 (単項関係)。
  5. state = set (単項関係) 0 個以上のアトム。
  6. inside、far、near = として定義される二項関係state -> set Person
  7. car_action = 次のように定義された二項関係state -> one motortype
  8. エンジン = 次のように定義された二項関係state -> one enginetype
  9. key_position = 2 つの二項関係の和集合state -> Person(ただし、各状態が最大 1 回しか出現しないように制約する多重度があるため、状態を aまたは a のstate -> key_locationいずれかに関連付けることはできますが、両方には関連付けることはできません)Personkey_location
  10. ドア = として定義される二項関係state -> dooroptype

要するに、上で定義したものはすべてリレーションであり、一部は単項であり、一部は二項です。二項関係inside, far and nearはset多重度で定義されますが、他のすべての関係は多重度 1 で定義されます。

つまり、署名はセットであり、関係は署名内で定義されますが、グローバルに表示されます。

于 2012-11-12T10:09:33.813 に答える
2

2 つの小さな修正:

  1. 技術的に言えば、enum enginetype {on,off} は

    sig enginetype {}
one sig on, off extends engine type {}

そのため、3 つのセットを宣言し、そのうちの 2 つ (on と off) はシングルトンです。

  1. のフィールド key_position の宣言

    abstract sig state{
  key_position : (Person + key_location)
  }

実際、2 つの関係 (状態 -> 人および状態 -> key_location) の和集合と見なすことができますが、多重度の制約は、Aviad の定式化が示唆する 2 つの値ではなく、任意の状態 s に対して s.key_position の値が 1 つだけ存在することです。 .

于 2012-11-14T15:13:44.467 に答える