source: vis_dev/vis-2.1/examples/coherence/coherence1.ctl @ 15

#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<*1*> = 1) -> AX((cc1.block_state=SHARED) * (cc1.block_add<0>=1))) + ((((cc1.block_state=SHARED) * (cc1.block_add<0>=1))) -> (direc.cache_Rlist1<*1*> = 1)));