In the TLA+ spec snippet below, I am getting an error at the highlighted line (BlocksToFiles'). TLC gives this error
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
In evaluation, the identifier BlocksToFiles is either undefined or not an operator.
line 69, col 28 to line 69, col 40 of module BlockModel
DeletedFiles is just set of model values. BlocksToFiles is a function from Blocks to Files.
I can't quite figure out the error. I would really appreciate any tips or pointers. thanks
GCBlocksForFile(f) == /\ PrintVal("F", f)
/\ PrintVal("BlocksToFiles",
BlocksToFiles)
/\
BlocksToFiles' = [ b \in DOMAIN BlocksToFiles
|-> IF BlocksToFiles[b]
= f THEN NullFile ELSE BlocksToFiles[b]
]
/\ ChunksToDelete' = ChunksToDelete \cup
{ Range(BlocksToChunks[b1]) : b1 \in { b \in DOMAIN BlocksToFiles : BlocksToFiles[b] = f }} \*
add the chunks of the block to be deleted. This is the equivalent of the deleted index in zippy
/\ BlocksToChunks' = [b \in DOMAIN BlocksToFiles
|-> IF BlocksToFiles[b] = f THEN <<NullChunk,
NullChunk, NullChunk>> ELSE BlocksToChunks[b]] \*
Remove block to chunk mapping for b
/\ UnusedBlocks' = UnusedBlocks \cup {
b \in DOMAIN BlocksToFiles : BlocksToFiles[b] = f } \*
put block b as Unused
/\ UnusedFiles' = UnusedFiles \cup {f} \*
move f to UnusedFiles
/\ DeletedFiles' = DeletedFiles \ {f} \*
remove f from deletedFiles
/\ PrintVal("BlocksToFiles'",
BlocksToFiles')
/\ PrintVal("BlocksToChunks'",
BlocksToChunks')
/\ PrintVal("UnusedBlocks'",
UnusedBlocks')
/\ PrintVal("DeletedFiles'",
UnusedBlocks')
BlockGC == /\ DeletedFiles # {}
/\ PrintVal("OrphanBlockGC",
DeletedFiles)
/\ { GCBlocksForFile(f) : f \in DeletedFiles}