私は Alloy チュートリアルを進めていて、この章を始めたところです。私の質問は、章を開始するフレーズです。
これで、ファイル システムの構造上の正確性を保証するモデルを構築できました...
これまでに構築したモデルを実行すると、まだファイル システムが切断されています。これは、このフレーズと矛盾しているようです。
これは、数日前に Web サイトからダウンロードした Alloy 4.2、ビルド日付 2012-9-25 のものです。私は何か間違ったことをしていますか、それとも意図的なものですか? 私の理解では、このような切断を防ぐモデルには何も表示されません。しかし、私の理解はまだ少しあいまいです。
関連するモデルを以下にコピーします。
// File system objects
abstract sig FSObject { }
sig File, Dir extends FSObject { }
// A File System
sig FileSystem {
live: set FSObject,
root: Dir & live,
parent: (live - root) ->one (Dir & live),
contents: Dir -> FSObject
}{
// live objects are reachable from the root
live in root.*contents
// parent is the inverse of contents
parent = ~contents
}
おそらく接続が必要な行を確認できましたlive: set FSObject
が、それはその行のセマンティクスに関する現在の理解ではありません。