Checking in specs
[repair.git] / Repair / RepairCompiler / MCC / specs / filesystem / test3.space
1 // sEXT2 - Simple File System Example
2 // Space Definition Language File
3
4 set Block(Block) :
5     UsedBlock | 
6     FreeBlock;
7
8 set FreeBlock(Block);
9
10 set Inode(Inode) :
11     UsedInode | 
12     FreeInode;
13
14 set FreeInode(Inode);
15
16 set UsedInode(Inode) :
17     FileInode | 
18     DirectoryInode ;
19
20 set FileInode(Inode);
21
22 set DirectoryInode(Inode) : RootDirectoryInode;
23
24 set RootDirectoryInode(Inode);
25
26 set UsedBlock(Block) :
27     SuperBlock | 
28     GroupBlock | 
29     FileDirectoryBlock | 
30     InodeTableBlock | 
31     InodeBitmapBlock | 
32     BlockBitmapBlock;
33
34 set FileDirectoryBlock(Block) : 
35     DirectoryBlock | 
36     FileBlock;
37
38 set SuperBlock(Superblock);
39
40 set GroupBlock(Groupblock);
41
42 set FileBlock(Block);
43
44 set DirectoryBlock(Block);
45
46 set InodeTableBlock(InodeTable);
47
48 set InodeBitmapBlock(InodeBitmap);
49
50 set BlockBitmapBlock(BlockBitmap);
51
52 set DirectoryEntry(DirectoryEntry);
53
54 // relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
55
56 inodeof: DirectoryEntry -> UsedInode (many->1);
57
58 contents: UsedInode -> FileDirectoryBlock (1->many);
59
60 inodestatus: Inode -> int (many->1);
61
62 blockstatus: Block -> int (many->1);
63
64 referencecount: Inode -> int (many->1);
65
66 filesize: Inode -> int (many->1);