\* TLC configuration file for ACP_NB_WRONG
\* The fundamental consistency property AC1 does not hold

CONSTANTS
  participants = { p0, p1 }

  waiting = waiting
  notsent = notsent
  undecided = undecided
  commit = commit
  abort = abort
  yes = yes
  timeout = timeout
  no = no

SPECIFICATION
  SpecNB
  
PROPERTIES
  AC1 \* invalid, TLC found that!