#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
# FAILS
AG(((cc1.cache_req = blk_rreq)*(direc.arbiter_state = ONE)*(cc1.blk_add<0>=0)*(direc.cache_Wlist2<*0*> = 1)) -> (cc2.block_state = EXCLUSIVE));