CONSTANTS
  Entities = {e1, e2}
  Participants = {p1, p2}
  Doc = Doc
  Vec = Vec
  Graph = Graph
  Fts = Fts
  MaxSteps = 6
  Nil = Nil

SPECIFICATION Spec

CHECK_DEADLOCK FALSE

INVARIANTS
  TypeOk
  MetadataVectorConsistency
  HybridResultValid
  CommittedAtomicity
  AbortedAtomicity
  TxnStateValid

SYMMETRY Symmetry