GNU/Linux ◆ xterm-256color ◆ bash 151 views

High-level steps are:

  1. Given a spec A, a (TLC) model M, and an error trace T

  2. Use TLC to check M with the “-generateSpecTE” command-line parameter set

  3. Append an operator OP to the generated SpecTE.tla: OP == PrintT(<<”lvl: “, TLCGet(“level”), vars>>) * vars is defined in A

  4. Change INIT and NEXT in SpecTE.cfg to check Init and Next in spec A

  5. Uncomment ACTION_CONSTRAINT in SpecTE.cfg

  6. Append CONSTRAINT OP to SpecTE.cfg

  7. Use TLC to check SpecTE