Alloyの人間関係をビビッドにするライブラリを作った

関係が言語の基本構成部品になっているalloy、やっぱり身近な「関係」を使って解説しようということで「人間関係」を例にあげることが多い。だけどman3とwoman1の間のロマンスとか砂を噛むようで味気ないよね。というわけで与えた選択肢の中からオブジェクトに一意な名前をつけるライブラリを作ってみた。

Susumuひどいｗｗ

ソースコードは他の勉強中に書いたコードと一緒にlearning_alloyリポジトリに置いた: https://github.com/nishio/learning_alloy

この画像を作るのに使ったコードはこちら: https://github.com/nishio/learning_alloy/blob/master/demo_of_named_man.als

ライブラリはパラメータを取る多相的モジュールってのになっていて、引数に与えられたシグネチャの子としてたくさんのシグニチャを作って、それぞれに「最大1個しか存在してはいけない」という制約をつける仕組み。tool/ディレクトリにこれを作るために作ったAlloyのコードを生成するPythonスクリプトが置いてある。

追記

run {
  #Man = 3
  #Woman = 5
} for 10

という書き方でインスタンスの個数を制約しているけど、今は実例探しだからあんまり問題になってないだけで反例探しだと10個までのスコープ全部の中から述語を満たすものを探すのでコストが高い。typescopeを使った方が良いようだ。run {} for exactly 3 Man, exactly 5 Woman

追記

lone sig X, Y, Z extends Base {} とかできるのか。

追記

enum Base {X, Y, Z}とかあるんだ。このライブラリでは個別の名前がloneになっているけど、oneにしたい場合はenumで書くほうがスマート。