>>811
Alloyは形式的に記述した仕様の妥当性（矛盾はないか、条件は満たしてるか、想定外外のケースは起きないか）などを
確かめるためのツールであって、自然言語で書かれた仕様の解釈が妥当か確かめるツールではないよ。残念ながら
自然言語の仕様書の解釈を誤ってAlloyに入力したとしても、その解釈の誤り自体はAlloyは指摘してくれない