ACP_SB_TLC.cfg

\* TLC configuration file for ACP_SB
\* Safety has been checked for 4 participants (without symmetries) 
\* and 6 participants (with symmetries)
\* Liveness has been checked for 4 participants
\* Intermediate properties have 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, p2 }

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

SPECIFICATION
  Spec
  
PROPERTIES
\*  AC1 AC2 AC3_1 AC4_alt            \* safety
\*  AC3_2                            \* liveness

\*  FaultyStable VoteStable StrongerAC2 StrongerAC3_1 NoRecovery \* intermediate properties

\*  DecisionReachedNoFault         \* invalid, to check that TLC does its job
\*  AbortImpliesNoVote             \* invalid, to check that TLC does its job
\*  AC5                            \* invalid, to check that TLC does its job

CHECK_DEADLOCK FALSE