2

我正在学习 Alloy 教程，并且刚刚开始这一章。我的问题是本章开头的那句话：

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

当我运行到目前为止构建的模型时，我仍然会发现文件系统断开连接，这似乎与这句话相矛盾。

断开连接的文件系统

这是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 不是反例，也不是文件系统的结构问题；它只是一个文件系统对象，无法从任何文件系统根目录访问，因此不存在。真的？

请注意，虽然约束确实确保每个 FileSystem 是一个连接图（实际上是一棵树），但它们并不能确保文件系统相互连接（也不能确保它们是不相交的）。如果您将运行命令更改为请求多个文件系统，这应该更容易看到。

您可能会在 IETF 会议上就这些约束是否构成一般文件系统的“结构正确性”进行良好的酒吧讨论，但我认为在上下文中，该短语只是为了指向第一课中所做的事情和文件系统示例之二。

于 2013-02-18T20:09:26.247 回答