Updating a variable inside a filtering condition (like CHOOSE ) causes TLC exception.

[Nar Ganapathy]

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}                                                                                

                 /\ UNCHANGED <<  

                              ChunksToRepair, 

                              ChunksToMove, 

                              OrphanedChunks

                              >>

[Stephan Merz]

The culprit is the conjunct

                /\ { GCBlocksForFile(f) : f \in DeletedFiles}                                                                                

of BlockGC. First of all, this is not type correct (a "silly expression" in TLA+ jargon) because it constructs a set (of Booleans, given the definition of GCBlocksForFile) but is used as a Boolean. Second, TLC will not interpret the expressions

   var' = ...

inside the definition of GCBlocksForFile(f) as assignments but just as tests for equality, hence the error message that you see: the value of BlocksToFiles in the successor state is not yet defined.

It appears to me that you intended to write

   /\ \A f \in DeletedFiles : GCBlocksForFile(f)

in order to iterate the action for each element of DeletedFiles. However, this will again not work if DeletedFiles contains more than one element: TLC will interpret the formulas var' = ... as assignments for the first element of the set DeletedFiles and as equality tests for the following elements, and these tests will fail, making the action inapplicable.

You really want to define operators that take the set DeletedFiles and produce the corresponding values in the successor state, for example

BTF(fs) == [ b \in DOMAIN BlocksToFiles |-> IF BlocksToFiles[b] \in fs THEN NullFile 

                                            ELSE BlocksToFiles[b] ]

and use conjuncts such as

   /\ BlocksToFiles' = BTF(DeletedFiles)

in the definition of action BlockGC.

Hope this helps,

Stephan

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ea9d56ed-865d-4aa3-9adf-aa89726295ac%40googlegroups.com.

[Nar Ganapathy]

Thanks for the response. Yes, I tried /\ \A f \in DeletedFiles : GCBlocksForFile(f) and it worked yesterday and I thought that fixed it. However you are right in that they had only one file in the DeletedFiles set.

 

Does TLA+ does not allow me to iterate through a set and apply state variable changes ? I don’t quite understand a key concept of when a state variable can be changed. Is the that rule that var’ = f(var) is always TRUE the very first time and then afterwards its not true ?

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B3E0BCD1-F6EF-4679-BE23-99D21DD5D75B%40gmail.com.