module filesystem

sig Object {}
sig Dir in Object {}
sig File in Object {}
sig FS {
        objects : set Object,
        parent : Object -> lone Dir,
        root : set Dir
}

fact tables {
        -- each filesystem must have one dir
        FS in root.Dir
        root in FS -> lone Dir
}

fact refs {
        -- parent is only defined for objects in the filesystem
        parent in objects -> Dir
        -- parent directories must be objects in the filesystem
        {x : FS, z : Dir, y : Object | x -> y -> z in parent} in objects -> Object
        -- root directories must be objects in the filesystem
        root in objects
}

pred inv {
        -- root has no parent
        all fs : FS | no (fs.root).(fs.parent)
        -- all objects are reachable from the root
        all fs : FS | fs.objects in (fs.root).*(~(fs.parent))
}