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 [], literal(true) => d.g.InodeBitmapBlock in InodeBitmapBlock;
  15
  16 // rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
  17 //[], d.g.BlockBitmapBlock < d.s.NumberofBlocks =>
  18 //d.g.BlockBitmapBlock in BlockBitmapBlock;
  19
  20 // rule 6 - adds the rootdirectoryinode number to the set
  21 //[], d.s.RootDirectoryInode < d.s.NumberofInodes =>
  22 //d.s.RootDirectoryInode in RootDirectoryInode;
  23
  24 // rule 7
  25 delay [for j=literal(0) to d.s.NumberofInodes-literal(1)],
  26 !(j in? UsedInode) => j in FreeInode;
  27
  28 // rule 8
  29 delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)],
  30 !(j in? UsedBlock) => j in FreeBlock;
  31
  32 // rule 9
  33 // for all directoryinodes, loop through there blockptr's and then add
  34 // all their directoryentries to DirectoryEntry set
  35 //[forall di in DirectoryInode, forall itb in InodeTableBlock,
  36 // for j=literal(0) to (d.s.blocksize/literal(128))-literal(1),
  37 // for k=literal(0) to literal(11)],
  38 // cast(InodeTable,d.b[itb]).itable[di].Blockptr[k] < d.s.NumberofBlocks =>
  39 // cast(DirectoryBlock,d.b[cast(InodeTable,d.b[itb]).itable[di].Blockptr[k]]).de[j]
  40 // in DirectoryEntry;
  41
  42 // rule 10
  43 // all non-zero blocks in an used inodes blockptr list should be
  44 // added to the contents relation
  45 //[forall i in UsedInode,
  46 // forall itb in InodeTableBlock,
  47 // for j=literal(0) to literal(11)],
  48 //     !(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
  49 //     <i,cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]> in contents;
  50
  51
  52 // rule 11 seems to be imperfect because it is adding directories and files
  53 // to the filedirectoryblock but these automatically get funneled into
  54 // fileblock (and hence the change below). Perhaps these should discriminate
  55 // because otherwise, there is no direct use of DirectoryBlock (subset
  56 // of FileDirectoryBlock) anywhere in the model definition at all.
  57
  58 // rule 11
  59 // for each inode in use, add non-zero, valid blocks mentioned in the
  60 // inode's blockptr list in the inodetableblock to fileblock
  61 //[forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)],
  62 //cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]<d.s.NumberofBlocks and
  63 //!(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
  64 //cast(InodeTable,d.b[itb]).itable[i].Blockptr[j] in FileBlock;
  65 // was FileDirectoryBlock
  66
  67 // rule 13
  68 // same as rule 12/19, but instead with used inodes.
  69 [forall j in Inode, forall ibb in InodeBitmapBlock], literal(true) => <j, cast(InodeBitmap,d.b[ibb]).inodebitmap[j]> in inodestatus;
  70
  71 // rule 14
  72 // adds all non-zero inodenumbers of directory entries to the set
  73 // FileInode
  74 //[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes and
  75 //!(de.inodenumber = literal(0)) => de.inodenumber in FileInode;
  76
  77 // rule 15
  78 // builds up relation 'inodeof' such that <x,y> means x is a
  79 // directory entry with inode numbered y
  80 //[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes =>
  81 //<de, de.inodenumber> in inodeof;
  82
  83 // rule 16
  84 // populating the referencecount relation with the referencecount
  85 // values for every usedinode
  86 //[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
  87 //<j,cast(InodeTable,d.b[itb]).itable[j].referencecount> in referencecount;
  88
  89 // rule 17 - populate the filesize relation with the sizes inodes' files
  90 //[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
  91 //<j,cast(InodeTable,d.b[itb]).itable[j].filesize> in filesize;
  92
  93 // rule - similar to rule 19, if the bit in the block bitmap is 0 the that
  94 // block is marked as free in the blockstatus relation
  95 //[forall j in Block, forall bbb in BlockBitmapBlock], literal(true) => <j,cast(BlockBitmap,d.b[bbb]).blockbitmap[j]> in blockstatus;
  96