9784e28fe481e219471a75196b840baf5fc44e14
[repair.git] / Repair / RepairCompiler / MCC / test2.model
1 // sEXT2 - Simple FileSystem Example -  MODEL DEFINITION FILE
2
3 // rule 1 - adds the block number of the superblock to the superblock set
4 [], literal(true) => literal(0) in SuperBlock;
5
6 // rule 2 - adds the block number of the groupblock to the groupblock set
7 [], literal(true) => literal(1) in GroupBlock;
8
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; 
12
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; 
16
17 // rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
18 [], d.g.BlockBitmapBlock < d.s.NumberofBlocks => 
19 d.g.BlockBitmapBlock in BlockBitmapBlock; 
20
21 // rule 6 - adds the rootdirectoryinode number to the set
22 [], d.s.RootDirectoryInode < d.s.NumberofInodes =>
23 d.s.RootDirectoryInode in RootDirectoryInode; 
24
25 // rule 7 
26 delay [for j=literal(0) to d.s.NumberofInodes-literal(1)], 
27 !(j in? UsedInode) => j in FreeInode; 
28
29 // rule 8
30 delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)], 
31 !(j in? UsedBlock) => j in FreeBlock; 
32
33 // rule 9
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]
42  in DirectoryEntry;
43
44 // rule 10
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; 
52
53
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.
59
60 // rule 11 
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
67
68 // rule 12
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; 
74
75 // rule 13
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; 
80
81 // rule 14
82 // adds all non-zero inodenumbers of directory entries to the set
83 // FileInode
84 [forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes and
85 !(de.inodenumber = literal(0)) => de.inodenumber in FileInode; 
86
87 // rule 15
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; 
92
93 // rule 16
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; 
98
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; 
102
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; 
108
109 // rule 19
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;