#The directory contains information about the cache content
#that is coherent with the information in the cache controller
# If the block is in state EXCLUSIVE in the cache controller, its corresponding
# bit is set in the Wlist of the directory

AG(((cc1.block_state = EXCLUSIVE)*(cc1.block_add<0> = 0)) ->  (direc.cache_Wlist1<*0*> = 1));