#The directory contains information about the cache content
#that is coherent with the information in the cache controller
# If the block is in state SHARED in the cache controller, its corresponding
# bit is set in the Rlist of the directory
AG(((direc.cache_Rlist1<*0*> = 1) -> AX((cc1.block_state=SHARED) * (cc1.block_add<0>=0))) +
   ((((cc1.block_state=SHARED) * (cc1.block_add<0>=1))) -> (direc.cache_Rlist1<*0*> = 1)));