\* TLC configuration file for ACP_NB
\* Safety has been checked for 3 participants (without symmetries) 
\* and 4 participants (with symmetries)
\* Liveness has been checked for 3 participants
\* Incorrect safety and liveness properties are both detected
\* (with meaningful counterexamples) with 2 participants

\*SYMMETRY
\*  Perms

CONSTANTS
  participants = { p0, p1 }

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

SPECIFICATION
  SpecNB
  
PROPERTIES
  AC1 AC2 AC3_1 AC4_alt            \* safety
  AC3_2 AC5                        \* liveness

\*  DecisionReachedNoFault         \* invalid, to check that TLC does its job
\*  AbortImpliesNoVote             \* invalid, to check that TLC does its job
\*  StrongerAC3_1                  \* invalid, to check that TLC does its job
\*  AllCommit                      \* invalid, to check that TLC does its job
\*  AllAbort                       \* invalid, to check that TLC does its job