노트
아직 올려 둔 예제가 그리 많지 않다. 사이트 작업을 이어 가면서 더 써 나갈 생각이다. 그동안은 웹 곳곳에서 찾은 좋은 예제 몇 가지를 소개한다!
TLA+ 예제 저장소: 공식 저장소로, 대부분 추상적인 알고리즘과 프로토콜을 다룬다.
TLA+로 보는 토끼와 거북이: 연결 리스트에서 사이클을 찾는, 바로 그 알고리즘 문제를 정형적으로 모델링했다.
메시지 큐: 읽는 쪽이 구독하는 토픽을 갖춘 pubsub 구현.
스레드 유한 큐: 가득 찬 큐에 쓰려는 쓰기 스레드를 잠시 재우는 유한 큐에서 데드락(deadlock)을 찾는다.
적대적 모델링: 스펙(spec)을 “기계”와 “세계” 구성 요소로 나누는 짧은 예제로, 여기서 세계는 기계의 적대자 역할을 한다.
배치 업로더: 내가 실무에서 처음 작성한 스펙이다!
결제 핸들러: 개념 개요의 송금 예제와 비슷한데, 현실에서 벌어졌다는 점만 다르다.
대규모 프로덕션급 스펙 세 개를 심도 있게 논의하는 정형 실용 모델링 입문도 참고하라.