2

私は 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が、それはその行のセマンティクスに関する現在の理解ではありません。

4

1 に答える 1

4

モデルがプロパティを保証することを意味するために、構造の正確性に関するチュートリアルの発言を取り上げます。

  • ファイルシステムのルートには親がありません。
  • すべてのライブ オブジェクトは、コンテンツ リレーションを介してルートから到達可能です。
  • 親関係は内容関係の逆です。
  • ルートから到達可能なすべてのオブジェクトはライブです。
  • コンテンツと親関係は、ライブ オブジェクトにのみ保持されます。(ライブでないオブジェクトには、親もコンテンツもありません。)

表示されているインスタンスでは、Dir0 はライブではなく、コンテンツも親もありません。したがって、インスタンスはリストしたすべての制約に従い、ファイル システム (Dir3 をルートとするツリー) は実際に接続されていると思います。Dir0 は反例ではなく、ファイル システムの構造的な問題でもありません。これは、どのファイル システム ルートからも到達できないため、ライブではない単なるファイル システム オブジェクトです。真実？

制約により、各ファイル システムが接続されたグラフ (実際にはツリー) であることは保証されますが、ファイル システムが互いに接続されていることは保証されません (また、それらがばらばらであることも保証されません)。複数のファイル システムを要求するように run コマンドを変更すると、これが見やすくなります。

これらの制約が一般的なファイル システムの「構造上の正確性」を構成するかどうかについて、IETF 会議で議論を深めることができるかもしれません。ファイルシステムの例のII。

于 2013-02-18T20:09:26.247 に答える