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 @@
-// 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