다음 단계

축하한다! 핵심 과정의 끝에 도달했다. 이제 TLA+의 핵심 개념을 모두 접했고, TLA+로 설계에서 버그를 찾는 법도 익혔다.

그렇긴 해도 아직 배움이 다 끝난 것은 아니다. TLA+에는 문법과 의미론 말고도 훨씬 많은 것이 있다. 모델 최적화(model optimization)도, 디자인 패턴도, 개발 프로세스의 일부로 TLA+를 쓰는 법도, 커맨드 라인에서 실행하는 법도 아직 이야기하지 않았다. 게다가 지금까지 쓴 예제는 전부 장난감 문제였다. 실제 세계의 스펙(spec)을 모델링하면 어떤 모습일까?

다시 말해, 어떻게 해야 TLA+를 잘 쓰게 될까?

우선, 이 사이트의 나머지 부분이 그 과정을 도와줄 것이다. 주제별 심화 섹션은 설계 시 고려 사항, 일반 팁, 도구를 더 잘 쓰는 법 등 전부 TLA+의 고급 활용에 관한 내용이다. 그리고 예제 섹션은 공부해 볼 연산자(operator)와 스펙을 모아 둔 곳이다.

그 밖에도 웹에는 자료가 얼마든지 있다! 링크는 기타 자료 페이지에서 확인할 수 있다.

하지만 무엇보다 중요한 것은 연습이다. 실력을 늘리려면 스펙을 써야 한다. 한동안 다뤄 봐서 잘 아는 시스템을 모델링하는 것부터 시작하기를 강력히 권한다. 그 시스템의 아키텍처나 특정 기능 하나에 대한 고수준 스펙을 써 보라. 빠짐없이 다뤄야 한다는 걱정은 접어 두고, 스스로 해낼 수 있다고 생각하는 것에만 집중하라.

이 단계에서 나오는 스펙 에러는 실제 에러를 가리킨다기보다 상대적으로 경험이 부족한 탓일 가능성이 더 크다(반드시 그렇다는 것은 아니지만). 잘 아는 시스템으로 연습하면 좋은 이유가 바로 이것이다. 어떤 시스템 가정을 놓쳤는지, 어떤 TLA+ 실수를 저질렀는지 알아보기가 더 쉽다. 이를 피드백 루프의 일부로 삼아 실력을 더 키워 나가라.

(하지만 그게 진짜로, 실제로 존재하는 버그일 가능성을 배제하지는 마라. 그런 일은 생각보다 자주 일어난다. 다만 제일 먼저 그렇게 넘겨짚지는 마라.)

백지에서 시작하는 새 시스템의 스펙을 쓰거나, 고장 났다고 이미 알려진 시스템을 디버깅하는 일에 곧장 뛰어들어도 괜찮다. 결국 가장 좋은 방법은 무엇이든 여러분을 가장 의욕 나게 하는 방법이다.

TLA+를 즐겁게 배웠기를 바란다!