Lambdaカクテル

京都在住Webエンジニアの日記です

Alloyでオーク問題を解く

猥雑な話で怒られそうなので恐縮ですが、オークが女騎士に怪しい薬を盛るというパズルがあったので、最近興味を持っていたAlloyでモデル検査をしましょう。

gist.github.com

解を図示するとこうなります。

f:id:Windymelt:20190919000833p:plain

Alloy初めて触ったのですが面白いですね。ところが「薬を盛ったオークは1人のみ」という制約がうまく効かないのか、「Show next solution」を押していると・・・

f:id:Windymelt:20190919000910p:plain

これはひどい……

矢印を出すために「飲ませた」という関係を定義していますが、これはなくてもいいかもしれないですね。

DISCLAIMER: 筆者はパズル中の表現については無関係な立場を取るものとします。