合金教程，断开文件系统？

Question

我正在通过Alloy教程，刚刚开始this chapter。我的问题是启动该章的一句话：

现在，我们已经建立了一个确保我们的文件系统的结构正确性的模型......

当我运行建立这样的模型远远我仍然断开连接的文件系统，这似乎与这句话相矛盾。

这与合金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线可能需要连接，但是这不是我现在该行的语义的理解。

Answer 1

我把本教程的有关结构正确性此言意味着，该模型保证了性能：

• 文件系统根目录没有父。
• 通过内容关系可以从根到达每个活动对象。
• 父亲关系是内容关系的逆。
• 从根目录可到达的每个对象都是活的。
• 内容和父关系仅适用于活动对象。 （不活的对象没有父项，也没有内容）

在显示的实例中，请注意Dir0不是活的，没有内容，也没有父项。所以我认为该实例服从我列出的所有约束条件，并且文件系统（以Dir3为根的树）实际上已连接。 Dir0不是反例，也不是文件系统的结构性问题;它只是一个文件系统对象，无法从任何文件系统根目录访问，因此无法访问。真正？

请注意，尽管约束确实确保每个文件系统都是连接图形（实际上是一棵树），但它们不确保文件系统彼此连接（或者它们不相交）。如果您更改运行命令以询问多个文件系统，应该会更容易看到。

您可能会在IETF会议上就这些约束条件是否构成文件系统的“结构正确性”进行很好的讨论，但我认为在上下文中，这个短语只是意在指出什么是在文件系统示例的课程I和II中完成。