1 // sEXT2 - Simple FileSystem Example - MODEL DEFINITION FILE
3 // rule 1 - adds the block number of the superblock to the superblock set
4 [], literal(true) => literal(0) in SuperBlock;
6 // rule 2 - adds the block number of the groupblock to the groupblock set
7 [], literal(true) => literal(1) in GroupBlock;
9 // rule 3 - adds the inodetableblock block number to the inodetableblock set
10 [], d.g.InodeTableBlock < d.s.NumberofBlocks =>
11 d.g.InodeTableBlock in InodeTableBlock;
13 // rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set
14 [], d.g.InodeBitmapBlock < d.s.NumberofBlocks =>
15 d.g.InodeBitmapBlock in InodeBitmapBlock;
17 // rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
18 [], d.g.BlockBitmapBlock < d.s.NumberofBlocks =>
19 d.g.BlockBitmapBlock in BlockBitmapBlock;
21 // rule 6 - adds the rootdirectoryinode number to the set
22 [], d.s.RootDirectoryInode < d.s.NumberofInodes =>
23 d.s.RootDirectoryInode in RootDirectoryInode;
26 delay [for j=literal(0) to d.s.NumberofInodes-literal(1)],
27 !(j in? UsedInode) => j in FreeInode;
30 delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)],
31 !(j in? UsedBlock) => j in FreeBlock;
34 // for all directoryinodes, loop through there blockptr's and then add
35 // all their directoryentries to DirectoryEntry set
36 [forall di in DirectoryInode,
37 forall itb in InodeTableBlock,
38 for j=literal(0) to (d.s.blocksize/literal(128))-literal(1),
39 for k=literal(0) to literal(11)],
40 cast(InodeTable,d.b[itb]).itable[di].Blockptr[k] < d.s.NumberofBlocks =>
41 cast(DirectoryBlock,d.b[cast(InodeTable,d.b[itb]).itable[di].Blockptr[k]]).de[j]
45 // all non-zero blocks in an used inodes blockptr list should be
46 // added to the contents relation
47 [forall i in UsedInode,
48 forall itb in InodeTableBlock,
49 for j=literal(0) to literal(11)],
50 !(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
51 <i,cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]> in contents;
54 // rule 11 seems to be imperfect because it is adding directories and files
55 // to the filedirectoryblock but these automatically get funneled into
56 // fileblock (and hence the change below). Perhaps these should discriminate
57 // because otherwise, there is no direct use of DirectoryBlock (subset
58 // of FileDirectoryBlock) anywhere in the model definition at all.
61 // for each inode in use, add non-zero, valid blocks mentioned in the
62 // inode's blockptr list in the inodetableblock to fileblock
63 [forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)],
64 cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]<d.s.NumberofBlocks and
65 !(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
66 cast(InodeTable,d.b[itb]).itable[i].Blockptr[j] in FileBlock; // was FileDirectoryBlock
69 // if the bit in the inodebitmap is 0 then that inode is marked as
70 // free in the inodestatus relation
71 [for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock],
72 cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(false) =>
73 <j,literal(Free)> in inodestatus;
76 // same as rule 12/19, but instead with used inodes.
77 [for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock],
78 cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(true) =>
79 <j,literal(Used)> in inodestatus;
82 // adds all non-zero inodenumbers of directory entries to the set
84 [forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes and
85 !(de.inodenumber = literal(0)) => de.inodenumber in FileInode;
88 // builds up relation 'inodeof' such that <x,y> means x is a
89 // directory entry with inode numbered y
90 [forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes =>
91 <de, de.inodenumber> in inodeof;
94 // populating the referencecount relation with the referencecount
95 // values for every usedinode
96 [forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
97 <j,cast(InodeTable,d.b[itb]).itable[j].referencecount> in referencecount;
99 // rule 17 - populate the filesize relation with the sizes inodes' files
100 [forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
101 <j,cast(InodeTable,d.b[itb]).itable[j].filesize> in filesize;
103 // rule - similar to rule 19, if the bit in the block bitmap is 0 the that
104 // block is marked as free in the blockstatus relation
105 [for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock],
106 cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(false) =>
107 <j,literal(Free)> in blockstatus;
110 // if the bit in the blockbitmap is 1 then that block is marked as
111 // used in the blockstatus relation
112 [for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock],
113 cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(true) =>
114 <j,literal(Used)> in blockstatus;