VoucherRedeem.cfg

CONSTANTS
  V = {v1, v2, v3}
  H = {holder1, holder2, holder3}
  C = {collector1, collector2, collector3}
INVARIANTS VTPTypeOK VTPConsistent
SPECIFICATION VTPSpec
\* Refinement does not hold
\*PROPERTY VSpec
CHECK_DEADLOCK FALSE