合金教程，斷開文件系統？

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中完成。