File System Model (I)

module models/examples/tutorial/filesystem

// A file system object in the file system
sig FSObject {
  parent: lone Dir
}

// A directory in the file system
sig Dir extends FSObject {
  contents: set FSObject
}

// A directory is the parent of its contents
fact defineContents {
  all d: Dir, o: d.contents | o.parent = d
}

// A file in the file system
sig File extends FSObject {}

// All file system objects are either files or directories
fact fileDirPartition {
  File + Dir = FSObject
}

// There exists a root 
one sig Root extends Dir {
}{
  no parent
}

// File system is connected
fact fileSystemConnected {
  FSObject in Root.*contents
}

// The contents path is acyclic
assert acyclic {
  no d: Dir | d in d.^contents
}

check acyclic for 5

// File system has one root
assert oneRoot {
  one d: Dir | no d.parent
}

check oneRoot for 5

// Every fs object is in at most one directory
assert oneLocation {
  all o: FSObject | lone d: Dir | o in d.contents
}

check oneLocation for 5

The "main tutorial text" frame will provide you with links to go to the next version of the model, when the time is right. If you wish to browse the different versions of the model on your own, you may do so with the links below:

(there are no previous versions of this model)

next model file system example version II.

restart the tutorial from the beginning.