AlloyAnalizer の基礎構文を見たところで

どう応用していいのか分からなかったので、次のサンプルを探してみる。

http://www.slideshare.net/konn/alloy-analyzer-9379488

enum Boolean { true, false }
enum KnightOrCrank { knight, crank }

abstract sig Talk { bool: one Boolean }

abstract sig Human {
  talk: lone Talk,
  type: one KnightOrCrank
} {
  some talk => (type = knight <=> talk.bool = true )
}

one sig Husband extends Human {} {
  IF_I_AM_KNIGHT_WIFE_ARE_KNIGHT in talk
}

one sig Wife extends Human {} { no talk }

one sig IF_I_AM_KNIGHT_WIFE_ARE_KNIGHT extends Talk {} {
  bool = true <=> (Husband.type = knight => Wife.type = knight )
}

pred show {}
run show

なるほど、属性継承か。
また、talk に関して、制約条件を設定して、種類が knight であるならば、talk の真偽は true であると。
その状態で、「私が騎士なら妻も騎士だ」という言葉を旦那が発して、「私が騎士なら妻も騎士だ」という言葉そのものが正しい場合は旦那も妻も騎士であるという制約条件を与えて図示すると。

後ろの

{}{/*ここ*/}

は制約条件を指定できるのか。
ここまで来ると、実用できそうな気配がある。というか、紹介しているプレゼンターはいい例を紹介していると思う。前回の勉強元とは大違いだｗ

残りの例も走らせて理解しよう。