From 8ba738028b175f4f40cc9642aa38adcc3ee62fa4 Mon Sep 17 00:00:00 2001
From: hardroadcrush <130765493+hardroadcrush@users.noreply.github.com>
Date: Tue, 31 Mar 2026 00:19:44 -0900
Subject: [PATCH] Update currentmodel-FS-1.html
I found the tutorial very hard to learn from.
I've made it more readable by
-Making references to signatures and attributes italic
-Making the language used more unambiguous
---
tutorials/online/currentmodel-FS-1.html | 34 +++++++++++++++----------
1 file changed, 21 insertions(+), 13 deletions(-)
diff --git a/tutorials/online/currentmodel-FS-1.html b/tutorials/online/currentmodel-FS-1.html
index e6eb439..70f6695 100644
--- a/tutorials/online/currentmodel-FS-1.html
+++ b/tutorials/online/currentmodel-FS-1.html
@@ -9,43 +9,51 @@
File System Model (I)
-// A file system object in the file system
+// A file system object type in the file system called FSObject.
+// It has an attribute called parent that contains either
+// zero or one Dir.
sig FSObject { parent: lone Dir }
-// A directory in the file system
+//Dir represents a directory in the file system
+//It has all the attributes of FSObject as well since it is
+//extended from it.
sig Dir extends FSObject { contents: set FSObject }
-// A file in the file system
+//File represents a file in the file system
+//It has all the attributes of FSObject as well since it is
+//extended from it.
sig File extends FSObject { }
-// A directory is the parent of its contents
+// Every directory is the parent of its contents
fact { all d: Dir, o: d.contents | o.parent = d }
-// All file system objects are either files or directories
+// All file system objects are either files or directories
fact { File + Dir = FSObject }
-// There exists a root
+// There exists one root directory
one sig Root extends Dir { } { no parent }
-// File system is connected
+// File system is connected
fact { FSObject in Root.*contents }
-// The contents path is acyclic
+// an assertion that every path in the contents subtree of
+// every directory is acyclic
assert acyclic { no d: Dir | d in d.^contents }
-// Now check it for a scope of 5
+// Now check the assertion for a maximum scope of
+// 5 instances of each signature
check acyclic for 5
-// File system has one root
+// assertion that the file system has one root
assert oneRoot { one d: Dir | no d.parent }
-// Now check it for a scope of 5
+// Now check it for a scope of 5
check oneRoot for 5
-// Every fs object is in at most one directory
+// Every file system object is in at most one directory
assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents }
-// Now check it for a scope of 5
+// Now check this assertion for a scope of 5
check oneLocation for 5