Repair/RepairCompiler/MCC/specs/filesystem/test3.model

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