I approached this problem with the assumption that if I started with the right object model, adding constraints would be easy. I think this turned out to be true.
The InodeTable is a singleton, since there exists exactly one per file system. All Inodes are accessible by the InodeTable via an array, which is indexed by Inumber. I originally modelled InodeTable.get as binary relation mapping Inumbers to Inodes, but in practice it was much easier to write constraints using a more OO/visually sensical approach.
Inodes map to DataBlocks via the 'addr' relation. Inodes can map to any number of DataBlocks, and likewise for DataBlocks. I did not constrain files to contain unique DataBlocks, in large part because that seemed noncrucial and required larger visualizatinos than if Blocks were shared.
An important feature of this object model is that AddrBlock and DirBlock extends DataBlock. Any relation that maps to DataBlock inherently maps to elements that are either exclusively in DataBlock, or else also in either AddrBlock or DirBlock. Thus, redirected addresses in Inode are simply the relations that map to the subset of DataBlock, AddrBlock. Similarly, multiple redirections result from AddrBlock.addr mapping to elements in AddrBlock. Since DirBlock extends DataBlock, Inode.addr may point directly to DirBlock, in which case that Inode is a directory. By the way, I did not see any reason to model exact numbers of redirection and so on, at least not in the object model. Details like that strike me as minor constraints that only clutter the abstract picture.
Finally, DirBlocks contain a set of Filenames (the '+' implies that all Filenames map to some DirBlock). There is a one-to-one correspondence between Filenames, Inumbers, and Inodes.
Pathnames are modelled like LISP lists: the car returns the first element in the list, the cdr returns the list minus the first element, which might be the empty set. The 'recursive' nature of this structure when using .* lent itself to path traversal.
[see unix.pal]
explanation
module unix
one sig InodeTable { get : set Inumber }
sig Inumber { inode : one Inode }
sig Inode { addr : set DataBlock }
sig Filename { inumber : one Inumber }
sig DataBlock { }
sig AddrBlock extends DataBlock { addr : DataBlock }
sig DirBlock extends DataBlock { contains : set Filename }
// no floating pieces: all Inodes are pointed to by Inumbers, // all Inumbers are pointed to by InodeTable, and all DataBlocks // are pointed by Inodes or AddrBlocks.
fact { Inode = Inumber.inode }
fact { Inumber = InodeTable.get }
fact { DataBlock = Inode.addr + (Inode.addr&AddrBlock).^addr }
// All Inodes correspond to an Inumber (only need to set size // equivalence because Inumber.inode maps to exactly one Inode). // Also need to explicitly state one to one correspondence between // Filenames and Inodes.
fact { #Inumber = #Inode }
fact { #Inumber = #Filename }
fact { all disj f1,f2 : Filename | f1.inumber != f2.inumber }
// AddrBlock must point to exclusive DataBlocks eventually (hence the ^).
fact addrBlockPointsToDataBlock { all a : AddrBlock | one d : a.^addr |
d in DataBlock-AddrBlock-DirBlock }
// If point to DirBlock, not point to other things
fact { all i : Inode | all d : i.addr | d in DirBlock => #(i.addr) = 1 }
pred dirSystem() {
#InodeTable = 1
#Inode > 0
#DirBlock > 0
#AddrBlock > 0
}
run dirSystem for 6
pred simpleSystem() {
#Inode.addr = 2
some AddrBlock
some DataBlock-AddrBlock
#Inode = 1
DirBlock in none
}
run simpleSystem for 4
A simple Unix file system with one directory containing one file. Reading top to bottom:
The InodeTable points first to an Inumber/Inode that is a directory (the Filename should be
'root'). The Directory contains a single File, also pointed to by the InodeTable, which
has two Blocks of Data, plus two once-indirected DataBlocks, plus one twice-indirected DataBlocks.
sig Pathname { car : Filename, cdr : lone Pathname }
// no looping in Pathname // (or, all Filenames and Pathnames are unique in single Pathname)
fact { no p : Pathname | p in p.^cdr }
fact { no p : Pathname | p.car in (p.^cdr).car }
// All cars in Pathname are Inodes that point to DirBlocks, except for // last element in Pathname, which may be any DataBlock.
fact { all p : Pathname
| p.cdr !in none => p.car.inumber.inode.addr & DirBlock !in none
and p.cdr.car & p.car.inumber.inode.addr.contains != none}
// DirBlocks are mapped from at most one inode. (since a previous constraint // requires that no DataBlock float, and a second constraint requires that // AddrBlock not point to DirBlocks, then DirBlocks are mapped to exactly one inode.)
fact { all disj i1, i2 : Inode | i1.addr + i2.addr in DirBlock => i1.addr != i2.addr }
pred show() {
#DirBlock > 0
#AddrBlock > 0
#Pathname = 2
#Pathname.cdr > 0
#Inode > 0
}
run show for 4
A similar file system as in part a, this time with a path name specifying the file's
location and name. Notice that the car of the top Pathname points to and Inode that is
a directory and which contains the next filename in the Pathname.
fun getInodesFromPathname (p : Pathname) : set Inode {
((p.*cdr).car).inumber.inode
}
run getInodesFromPathname for 4 but exactly 4 Pathname, exactly 3 Filename
fact { some Pathname.cdr.cdr }
Start at the top of the diagram and read down. There are four Inodes in the pathname,
two directories and at the end a file.
The first assertion, that each pathname resolves to at most one inode, is necessarily true. The use of one requres exactly one Filename, one Inumber and one Inode.
The second assertion, that no two distinct pathnames resolve to the same inode, is less clear. First of all, I see no reason not to permit linking, but soft and hard. I can't remember which is which, but one of those link types would require that different pathnames result in the same file...at least I seem to remember that even the name can be different. At any rate, that assertion failed!
By extending DataBlock to contain AddrBlocks, which in turn point to more DataBlocks, indirect addressing fits into the previous structure without the need to change other constraints. Well, I had this in mind from the beginning, so I didn't actually need to change anything.
One thing I did forget about was the Root directory! The following code takes care of that:
// Root is a Filename with extra constraints. // Because it was special in a constraint way I made it // 'in' not 'extends'.
one sig Root in Filename {}
// Root is a directory
fact { all d : Root.inumber.inode.addr | d in DirBlock }
// Root begins all Pathnames
fact { all p : Pathname-Pathname.cdr | p.car = Root }
The first filename in all Pathnames is Root