読者です 読者をやめる 読者になる 読者になる

謎言語使いの徒然

適当に気になった技術や言語を流すブログ。

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 であると。
その状態で、「私が騎士なら妻も騎士だ」という言葉を旦那が発して、「私が騎士なら妻も騎士だ」という言葉そのものが正しい場合は旦那も妻も騎士であるという制約条件を与えて図示すると。

後ろの

{}{/*ここ*/}

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

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