永遠の暫定版．間違ってたらコメント下さい．わからないで書いているところもあるので，ほぼ私のためのメモになっています…（言い訳）．

全体像

モジュールヘッダ

module hoge から書く．書いているモデルのモジュール名に当たると思われる．

シグネチャ

集合の定義．

例

 abstract sig Person {
   // something here
 }

 sig Man extends Person {
   // something here
 }

 sig Woman extends Person {
   // something here
 }

fact

fact は，必ず成立する（しなくてはならない）性質を記述するための文．
おそらく，反例を探すときに，fact に記述されたものに絞るのに使われるのだと思う．

• fact { F }
• fact 名前 { F }
• sig S { hogehoge }{ F }

のように記載する．

function

function は，実際の処理を記述するのではなく，hoge を引数として受け取り，fuga のような性質をみたす集合を返す，という感じで記述する．

書き方は，fun f[x1: e1, x2: e2,...] : e { E } とかく．

// Name と Addr は集合
sig Name, Addr {}
// Book は Name と Addr の直積の部分集合．つまり住所録，アドレス帳
sig Book {
  addr: Name -> Addr
}
// lookup は，アドレス帳と名前を受け取り，そのアドレス帳から名前に合致するアドレスの集合を返却する
fun lookup[ b: Book, n: Name ] : set Addr {
  b.addr[n]
}

predicate

引数を持つ述語．

pred p[x1: e1, ...,xn: en] { F } のように書く．

// Name = { (N0), (N1), ...}, Addr = { (A0), (A1), ...}
sig Name, Addr {}
// Book = { (N0, A0), (N1, A1), ...}
sig Book {
  addr: Name -> Addr
}
// アドレス帳に名前とアドレスの対応が含まれるか？
pred contains[b: Book, n:Name, d: Addr] {
  // 名前とアドレスとの対応がアドレス帳に含まれている，という述語
  n->d in b.addr
}
// どの名前に対してもアドレスが紐付いている．
fact everyNameMapped {
  // どのアドレス帳とどの名前に対しても，あるアドレスが存在して，名前とアドレスの紐付けがアドレス帳に存在する
  all b: Book, n: Name |
    some d: Addr | contains[b, n, a]
}

独自のドットジョイン

説明がしにくいので一旦例だけ．

// Person の元に対して，その grandpas を，両親の父親の集合として定義する
fun Person.grandpas : set Person {
  this.(mother + father).father
}

// ？？？説明プリーズ
pred Person.ownGrandpa {
  this in this.grandpas
}

assertion

モデルの定義や fact からある性質が従うかどうかを確認する記述．

assert a { F } のように書く．

sig Node {
  childresn: set Node
}

one sig Root extends Node {}

fact {
  Node in Root.*children
}

// 無限に伸びる木じゃないとこれは成り立たない．
// Alloy の場合，有限なオブジェクト内でしか調べないので必ず成り立たない．
assert someParent {
  all n: Node | some children.n
}

// 木のルート以外は何かの子
// これは成り立つ
assert someParent {
  all n: Node - Root | some children.n
}

check

assert に対して，それが成り立たない例の構成を実行するコマンド．

assert a { F } に対して， check a scope と記述する．具体的には，!F となる例（反例）を探す．
もちろん，fact M が記述されていれば，M && !F を満たす例（反例）を

abstract sig Person {}
sig Man extends Person{}
sig Woman extends Person{}
sig Grandpa extends Man {}

// a をなんらかの述語とする．
// 以下は有効
check a
// Person が 4 個の場合に調べる
check a for 4
// Person は 4 個だが Woman は 3 個の場合に調べる
check a for 4 but 3 Woman
// Man が 3 つ，Woman が 4 つの場合に調べる
check a for 3 Man, 4 Woman

// invalid
// 最上位のシグネチャ Person の個数が決まらない
check a for 3 Man
check a for 5 Woman, 2 Granpda

run

pred に対して，それが成り立つような例の構成を実行するコマンド．
思いもしなかった例を見つける手段？

pred p に対して，run p scope と記述する．

訂正

• 2021/4/10

A, B extends C が C = A + B かのような記載をしていましたので修正しました。
正しくは、C - (A + B) は空でないです。

試しに動かしてみた系の記事も同じ日に投稿予定．