Automatic Verification of Directory-Based Consistency Protocols with Graph Constraints