1

私には2つのクラスがAあり、それらBのクラスの追加データとの関係がありRます。

したがって、AとBはを介して相互に関連付けられていRます。

sig A {}
sig B {}

sig R {
    a : A,
    b : B,
    data : Bool
}

ここで、Boolは次のように定義されます。

sig Bool {}
sig True, False extends Bool {}

今、私はAこのように拡張します：

sig A{
    allb : some B
}

これには、これとそれBの間に関係があり、データがタイプであるすべてのインスタンスが含まれます。ABTrue

次の論理ステートメントをAlloyファクトとして表現したいと思います。

上記のテキストの正式なバージョン
（ソース：dropproxy.com）

ここでTrue == 1、とは、とのすべてのインスタンスをそれぞれセットし、含むとFalse != 1仮定Aします。RAR

私がこれまでに試したことは、fun trueR(a : A)すべてRの'を返す必要があるR.a = a and r.data = Trueaとfact allbIsRTrue、それぞれに対して。によって返される'のA allb合計である必要があることを示すaを定義することです。R.btrueR

ただし、ここで行き詰まり、参照内のセットを合計するための適切な構成が見つからず、試行するとsum構文エラーが発生します。

正式な制約をAlloyファクトとして指定するにはどうすればよいですか？

4

1 に答える 1

3

集合の内包性を使いたいと思います。Alloyでは、これは集合の内包的包摂の構文です

{x: X | f(x)}

上記の式は、が成立 する一連のX'に評価されます。f(x)

あなたの例では、あなたのために事実を表現するために、次のallBようなものを書くことができます

fact fAllB {
    all a: A | 
        a.allB = {b: B | 
            some r: R | r.ra = a and r.rb = b and r.data = True}
}

英語では、この事実は「すべてaの集合Aに対して、a.allBはすべての集合であり、それらを正確に「接続」するものBが存在し、そのためにである。rabr.dataTrue

モデルの残りの部分に加えた次の変更に注意してください。

  • あなたはおそらくどちらでもないBoolboolsを望まないので、私はsigを抽象化しましたTrueFalse

  • とsigsをシングルトンsig（つまり、True）にしました。おそらく、それぞれのアトムを1つだけにしたいからです。Falseone sig

  • 名前のエイリアシングと潜在的な混乱を避けるために、リレーションaの名前を変更しました。brarb

これが、この例で使用したモデルの残りの部分です

abstract sig Bool {}
one sig True, False extends Bool {}

sig A {
  allB: set B
} 
sig B {}
sig R {
  ra : A,
  rb : B,
  data : Bool
}
于 2012-10-19T16:33:22.880 に答える