source: vis_dev/vis-2.1/examples/coherence/README @ 11

Here is a list of properties to check:
1) Liveness: If a  processor requests a  read then it will eventually be 
serviced.

2) Safety: If a cache has exclusive access to a block, then the other cache
 has no access to that block 

3) Safety: If the block is in state SHARED in the cache controller, its corresponding
 bit is set in the Rlist of the directory.

4) Safety: If the block is in state EXCLUSIVE in the cache controller, its corresponding
 bit is set in the Wlist of the directory