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;