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