Supervisor Tree を Alloy で記述してみた

alloy

今ひとつ Alloy を理解できていないので、Erlang や Scala で使う Supervisor Tree の仕様を記述

まずは、集合を定義してみる。

abstract sig Actor {
  parent : lone Supervisor
}
sig Worker extends Actor {}
sig Supervisor extends Actor {
  child : Actor
}
  • Worker は、Actor である
  • Supervisor は Actor である
  • Actor は、親として高々1つの Supervisor を持つ
  • Supervisor は、子として0個以上の Actor を持つ

個人的に、1 Application : 1 Supervsior Tree だろうと思っているので、下記を追加する。

one sig RootSupervisor extends Supervisor {}

Actor は、高々一つの親を持つけれど、RootSupervisor は絶対に親を持たないので、下記の制約を追加する。

one sig RootSupervisor extends Supervisor {} {
  no parent
}

ここまでで、Supervisor Tree に登場する集合は、全て定義できた。ここに制約を追加していく。
現状だと、自分自身を親や子にできるので、下記の制約を追加する。

fact parent {
  no (^parent & iden)
}

fact child {
  no (^child & iden)
}

親と子の関係はペアとなるので、下記の制約を追加する。

fact pair {
  parent = ~child
}

RootSupervisor を除く全ての Actor は絶対に親が必要であるため、全ての Actor は RootSupervisor から辿れるという制約を追加する。

fact {
  Actor in RootSupervisor.*child
}

最後に確認用に空の動作を追加して実行する。

pred show () {}
run show

assert や check は勉強中なので、また今度。
最終的には、下記の通り。

module SupervisorTree

abstract sig Actor {
  parent : lone Supervisor
}
sig Worker extends Actor {}
sig Supervisor extends Actor {
  child : Actor
}
one sig RootSupervisor extends Supervisor {} {
  no parent
}

fact parent {
  no (^parent & iden)
}

fact child {
  no (^child & iden)
}

fact pair {
  parent = ~child
}

fact {
  Actor in RootSupervisor.*child
}

pred show () {}
run show

突っ込み大歓迎。