Learn TLA+ 원페이지 요약

Learn TLA+ Learn TLA+

코드 버그와 달리 설계 결함에는 “정말 열심히 생각해 보라”는 처방뿐이었다. TLA+는 설계를 직접 테스트하게 해 주는 정형 명세 언어이고, 이 무료 가이드는 핵심 과정·주제별 심화·예제 세 부분으로 그것을 가르친다.

• 결함의 두 출처: 코드 버그(코드가 설계와 어긋남 — off-by-one, 널 역참조)와 설계 결함. 코드 버그를 찾는 기법은 많지만 설계 버그에는 기법이 없었다.
• TLA+: 설계를 직접 테스트하는 정형 명세 언어. 레슬리 램포트가 개발했고 AWS·Microsoft·CrowdStrike 같은 기업들이 지지해 왔다.
• 대체가 아니라 보강: 엔지니어링 역량을 대체하지 않고 보강해, 시스템을 더 빠르고 자신 있게 설계하게 해 준다.
• 핵심 과정(Core): 기본 연산자(operator)에서 고급 주제까지 언어 전체를 다루는 선형적 입문. 순서대로 읽도록 설계됐다.
• 주제별 심화(Topics): 선택 사항인 고급 자료. 레슨마다 다수(전부는 아님)의 사용자에게 유용하고, 대체로 서로 독립이며 의존이 있으면 명시된다.
• 예제(Examples): TLA+를 스펙에 적용한 사례 — 스펙을 쓰는 법과 이해하는 법을 함께 보여 준다.
• 가이드의 상태: 아직 작업 중이다. 업데이트는 새 소식, 진행 중인 작업은 새 소식의 로드맵, 질문·우려는 GitHub 저장소 hwayne/learntla-v2로 받는다. 옛 버전은 old.learntla.com.
• 저자 힐렐(Hillel): TLA+ 재단 일원이자 『Practical TLA+』 저자. 자기 책이 유료인 것이 마음에 들지 않아 이 가이드를 썼다. 블로그·주간 뉴스레터를 운영하고 전문 컨설턴트로 워크숍을 진행한다(<plug> 가짜 태그를 두른 셀프 홍보 농담).

함정 핵심 과정은 순서대로 읽는다 — 초보자는 개념 개요부터 시작하고, 익숙한 사람은 새 내용이 나올 때까지 훑는다. 주제별 심화는 골라 읽어도 되며 모든 레슨이 모든 사용자에게 필요하지는 않다. 가이드가 미완성이므로 최신 변경은 새 소식과 로드맵에서 확인한다.

완역 읽기 → Learn TLA+

자주 묻는 질문 FAQ

TLA+가 무엇이고 누가 만들었는지, 어떻게 테스트하는지(TLC 모델 체킹), 어디에 강하고 약한지, 테스트·다른 정형 도구와 어떻게 다른지를 문답으로 정리한다.

• TLA+: 명세(specification), 즉 시스템 설계를 쓰고 검사하는 언어. 코드를 쓰기 전에 명세를 직접 테스트해 버그를 찾는다.
• 만든 사람: Leslie Lamport. 비잔틴 장애 허용, Paxos, LaTeX(“Lamport’s TeX”)도 만들었다.
• PlusCal: TLA+로 컴파일되는 DSL. 대부분의 엔지니어에게 순수 TLA+보다 시작하기 쉽다. 핵심 과정은 PlusCal로 시작해 끝에 TLA+를 완전히 가르치고, 주제별 심화·예제는 양쪽 버전을 제공한다.
• 정형 기법(formal methods): 정형 명세(“올바름”의 엄밀한 수학적 정의)를 쓰고 정형 검증(코드가 그 정의를 만족함을 보임)으로 확인하는 CS 분야. 실례는 저자가 운영하는 Let’s Prove Leftpad.
• 왜 설계를 검증하나: 범용 코드의 정형 검증은 정말 어렵다. TLA+는 훨씬 단순한 추상 설계만 검증해, 능력 일부를 내주고 쓰기 쉬움을 얻는다.
• TLA의 뜻: 본문 농담은 “Three Letter Acronym”, 진짜 뜻은 Temporal Logic of Actions(액션의 시간 논리). TLA+는 TLA라는 핵심을 중심으로 설계됐다.
• TLC · 모델 체킹: 주력 도구. 스펙의 가능한 모든 행동을 요구사항에 비춰 검사하며 단위 테스트보다 훨씬 철저하다. 프로세스 3개 × 스텝 4개 시스템이면 인터리빙 34,650가지, 서로 다른 상태 415,800개를 전부 본다.
• 한계: 테스트 대상은 설계다. 설계에서 코드를 생성하거나 코드와 대조하는 기능이 내장돼 있지 않다(50줄 설계가 코드 수천 줄이 될 수 있다. 동기화 기법은 따로 있다). 설계가 좋은지·실용적인지·구현 가능한지는 모르고 요구사항 만족 여부만 알려 준다.
• 강점: 동시적·분산 시스템의 모델링과 버그 찾기. 프로그램·서비스·사람 행위자가 얽힌 시스템(예: AWS Step Function)도 하나의 설계로 묶어 검사한다.
• 약점 5가지: 수치 코드(정수만, 소수·부동소수점 불가), 문자열 조작(문자 시퀀스로 가능하나 어색), 확률적 속성(“90% 이상”), 도달 가능성 속성(“X가 일어날 가능성이 항상 있다”), 실시간 속성(“Y 후 5초 안에 X”). 도구 쪽으로는 대화형 탐색·시각화 공식 기능이 아직 없다.
• 수학 배경: 새로 필요한 개념은 “X implies Y”와 “forall/some x in set” 한정자뿐이고, 핵심 과정이 점진적으로 설명한다.
• 테스트와의 관계: 단위 테스트·Cucumber·TDD·PBT는 코드 작성 실수를 잡고, TLA+는 설계가 원하는 대로 동작하는지 본다. 설계 검사는 구현 중 실수를 못 막지만, 구현보다 빨리 만들고 더 철저히 테스트할 수 있다. 테스트보다 “낫지”는 않다.
• 다른 도구: SPARK·Idris·Dafny·Frama-C·F*는 코드를 정형 검증하는 도구다. Alloy·Spin·Event-B·mCRL2는 같은 영역(추상 설계 검증)의 명세 언어로, 저자는 비교에 양쪽 전문가가 쓴 별도 페이지가 필요하다고 본다. P는 써 보지 않아 비교하지 않고, CTL*는 농담으로 넘긴다.
• 성공 사례: Espark Learning(엔지니어 10명)은 분산 설치 프로그램 버그를 찾아 몇 주의 개발과 연간 수십만의 매출을 지켰다(저자가 TLA+를 시작한 계기). AWS는 S3·DynamoDB 일부를 모델링해 모든 테스트와 코드 리뷰 두 번을 빠져나간 35스텝 버그를 찾았고, CrowdStrike는 닷새 워크숍으로 여러 장애 사례를 찾았다. Azure·MongoDB·Confluent·Elastic·Cockroach Labs도 썼다.
• 설계 검사의 경제성: “서비스가 다운돼도 같은 결제를 두 번 제출하지 않는다”를 코드로 철저히 테스트하려면 대공사지만, TLA+로는 스물 몇 줄이면 된다.

함정 TLA+는 설계만 검사하므로 코드 테스트를 대체하지 않는다. 아직 테스트를 하지 않는 팀이라면 테스트가 먼저다(저자는 이 이유로 잠재 고객을 거절한 적이 있다). 좋은 설계인지는 도구가 아니라 엔지니어가 판단한다 — “어떤 도구도 좋은 엔지니어가 될 의무를 면제해 주지 않는다.”

완역 읽기 → 자주 묻는 질문

새 소식 What’s New

사이트의 날짜별 변경 이력 6건과 앞으로의 로드맵을 나열한 공지 페이지다. 개념 설명은 없다.

• 2023-08-02: 주제 경계 없는 모델 다루기·모델 체킹 최적화 추가.
• 2023-01-13: 주제 메시지 큐 모델링 추가.
• 2022-11-11: GitHub 이슈 여러 건 수정, 새 연산자 예제(분할) 추가.
• 2022-07-25: 연습 문제 디렉티브(exercise directive) 추가 — 핵심 과정에 연습 문제를 넣기 시작할 수 있게 됐다.
• 2022-07-08: 표준 모듈 레퍼런스 추가.
• 2022-06-30: 베타 공개.
• 로드맵 · 핵심 과정: 연습 문제, 이해하기 어려워하는 부분 고치기, 다이어그램 추가.
• 로드맵 · 주제별 심화: 정제, ADT 모델링, 커뮤니티 모듈, 레거시 시스템 모델링, 기계와 세계의 차이, 스펙과 코드베이스 동기화, 하이퍼속성, :: 문법.
• 로드맵 · 예제 / 레퍼런스 / 기타: 예제는 “Many” 한 단어. 레퍼런스는 문제 해결 페이지, LaTeX-ASCII 대응표, TLA+·PlusCal 치트시트. 기타는 오프라인 PDF, C 문법 PlusCal 패널, 팝업 각주.
• 이름만 등장하는 용어: ADT, 하이퍼속성, :: 문법, 커뮤니티 모듈, 기계와 세계의 차이 — 로드맵 항목명일 뿐 설명은 없다.

함정 로드맵은 예정 목록일 뿐이며 각 항목의 완료 여부는 이 페이지가 말하지 않는다. 2022-11-11 항목의 링크 텍스트는 “새 연산자 예제”지만 가리키는 곳은 예제 “분할”이다.

완역 읽기 → 새 소식

개념 개요 Conceptual Overview

동시성 설계 버그는 드문 이벤트 순서에서만 터져 찾기도 고치기도 어렵다. 스펙(시스템)과 속성(요구사항)을 주면 TLC가 제약된 모델 안의 모든 행동을 탐색해 속성을 깨는 행동을 찾아 준다 — 책 전체의 개념 틀이 이 장에 있다.

• 동기 예제(경쟁 조건): 송금 코드 guard → withdraw → deposit. “동시에 여러 송금 가능”과 “송금 스텝이 비원자적”이라는 두 변경이 함께 있을 때만 경쟁 조건이 생긴다. 앨리스 잔액 6달러에 송금 X(3)·Y(4)가 동시에 guard를 통과하면 둘 다 인출돼 잔액이 -1이 된다.
• 동시성 버그가 어려운 이유: 대부분의 실행은 정상이고 특정 순서에서만 버그가 난다. 락 같은 세 번째 기능을 넣어 문제가 사라져도, 설계를 탐색하지 않고는 해결했는지 더 드물게 만들었는지 알 수 없다.
• TLA+의 목적: 설계 문제를 프로그램으로 탐색한다. 요구사항이 깨지면 설계를 바꾸고, 깨지지 않으면 옳다는 확신이 커진다.
• 개념 틀: 명세(스펙) · 속성 · 모델 체커(+모델)의 세 부분.
• 명세(specification): 시스템과 그 시스템이 할 수 있는 일의 기술. 예: 계좌 집합, 계좌별 잔액, 아무 계좌 간 아무 금액 송금, 잔액 확인 후 차감·가산, 비원자적·동시 송금.
• 행동(behavior): 가능한 서로 다른 실행. 스펙은 행동들의 집합을 가진다.
• 속성(property): 시스템 요구사항. 모든 행동이 모든 속성을 만족해야 올바르며, 위반 행동 하나면 충분하다.
• 불변식(invariant): 모든 행동의 모든 상태에서 참이어야 하는 속성. 예: “어떤 계좌도 초과 인출될 수 없다”. 라이브니스·액션 속성은 더 고급으로 뒤 장에서 다룬다.
• 모델 체커: 가능한 모든 행동을 생성해 모든 속성을 검사하고, 위반이 있으면 재현 경로인 에러 트레이스를 돌려준다. 툴박스에 번들된 TLC가 가장 인기 있으며, 따로 말이 없으면 “모델 체커”는 TLC다.
• 모델(model): 행동은 무한하므로 제약을 건다(예: 계좌 3개·계좌당 최대 10달러, 송금 2건·송금당 최대 10달러). 이 런타임 매개변수와 기타 설정 전체가 모델이다.
• 작은 범위 가설: 모델 통과가 정확성을 보장하지는 않지만, 경험적으로 대부분의 오류는 아주 작은 범위에서 나타난다(워커 3개로 되면 아마 25개로도 된다).
• 정의 ==: 정의에는 ==를 쓴다.
• 집합(set): 중복·순서 없는 값의 모음. 배열·키-값 맵은 시퀀스(sequence)·구조체(structure)에 해당하지만 명세에서는 집합이 훨씬 근본적이다.
• 함수 집합 [People -> Money]: 사람에게 금액을 배정하는 가능한 모든 방식의 집합.
• 변수는 여러 초기값 중 하나: acct \in [People -> Money]는 100개 값 중 하나이며, TLC는 100개 초기값 각각에서 출발하는 모든 행동을 탐색한다.
• 한정자(quantifier) \A: NoOverdrafts는 모든 계좌가 >= 0이면 참 — 파이썬 all([acct[p] >= 0 for p in People])에 해당한다.
• 프로세스(process): wire 프로세스가 여러 개 동시에 돈다. NumTransfers == 2면 2개, 10·100·1000개도 가능하다(한계는 인내심과 RAM).
• 레이블(label): 각 스텝은 별개의 레이블에 속한다. 무엇이 원자적으로 일어나고 어디에 다른 프로세스가 끼어들 수 있는지를 레이블이 정하므로 경쟁 조건을 표현할 수 있다.
• 매개변수화: 하드코딩한 값을 CONSTANTS People, Money, NumTransfers로 바꾸면 불변식은 같고 값만 다른 모델을 여러 개 만든다 — 송금 1건이면 통과, 2건이면 실패함을 확인할 수 있다.
• 아직 안 다룬 개념: 시간 속성, 공정성, 스터터 불변성(뒤 장).

variables
  acct \in [People -> Money];

define
  NoOverdrafts ==
    \A p \in People:
      acct[p] >= 0
end define;

  Check:
    if acct[from] >= amnt then
      Withdraw:
        acct[from] := acct[from] - amnt;
      Deposit:
        acct[to] := acct[to] + amnt;
    end if;

함정 이 wire 스펙은 NoOverdrafts를 불변식으로 지정하면 실패한다 — Check와 Withdraw가 다른 레이블이라 그 사이에 다른 송금이 끼어들기 때문이다. 모델 통과는 정확성 증명이 아니며(더 큰 매개변수에서만 드러나는 오류가 있을 수 있다), 행동이 무한하므로 모델에 반드시 제약을 걸어야 한다.

완역 읽기 → 개념 개요

핵심 과정 Core

완전한 문외한을 초보 실무자로 이끄는 자기완결적 “책”이다. PlusCal부터 가르치고, 순수 TLA+의 새 내용은 나중에 한 장으로 다룬다.

• 성격: 언어의 핵심 자료를 담은 독립된 책. TLA+에 이미 익숙하면 주제별 심화가 더 유용할 수 있다.
• 학습 순서: ① 기본 연산(두 수 더하기, 시퀀스 이어 붙이기) → ② 결정적·비동시 알고리즘 명세(“리스트에 중복이 있는지 확인”)와 불변식 검사 → ③ 비결정적 알고리즘(무작위성, 실패 가능성) → ④ 동시적 시스템(큐 하나를 공유하는 읽기·쓰기 주체) → ⑤ 시간 속성(“언젠가는 모든 서버가 온라인이 된다”) → ⑥ TLA+ 우선 방식의 스펙.
• 필수 범위: 시간 속성까지(포함)가 TLA+를 온전히 쓰는 데 필요하고, 그 이후는 힘을 더 보태는 내용이다.
• TLA+를 쓰는 두 방식: 모든 것을 TLA+로 하는 순수 TLA+, 또는 TLA+를 일종의 “어셈블리 언어”로 삼아 기본 로직은 TLA+로 쓰고 상태 전이는 전부 DSL에서 처리하는 방식.
• PlusCal: 두 번째 방식을 위한 공식 DSL. 이 가이드는 저자 선호로 PlusCal부터 시작한다.
• PlusCal 먼저인 이유 1: 명세는 극도로 밀도 높고 서로 얽힌 주제라, 일부 측면을 떼어 쓸모 있게 가르친 뒤 쌓아 가면 인지 부하가 준다. 순수 TLA+부터면 하나를 해내려 해도 모든 것을 한꺼번에 배워야 한다.
• PlusCal 먼저인 이유 2: PlusCal을 알면 순수 TLA+ 학습이 훨씬 쉬워, 새 내용 전부를 TLA+ 장 하나로 다룰 수 있다.
• 예제: 현재 가이드의 예제는 빈약하고, 더 흥미로운 예제와 웹에서 모은 링크는 예제 섹션에 있다.

함정 모두가 PlusCal 먼저 방식을 더 쉽다고 느끼지는 않으며, 그래도 괜찮다. TLA+부터 가르치는 대안은 창시자가 만든 두 가지다 — 『Specifying Systems』(시스템 모델링의 포괄적 입문서지만 스펙 검사 방법은 덜 다룸)와 비디오 강좌(저자는 보지 않았지만 지인 몇몇이 정말 좋아한다고 전한다). 더 큰 목록은 기타 자료에 있다.

완역 읽기 → 핵심 과정

환경 설정 Setup

툴박스를 설치해 개념 개요의 wire 스펙을 만들고, PlusCal을 변환한 뒤 TLC 모델을 돌려 NoOverdrafts 불변식이 깨지는 에러 트레이스를 직접 본다. 이후 모든 장에서 쓰는 스크래치 파일과 >>> 표기도 여기서 준비한다.

• 툴박스(Toolbox): 저자가 교육용으로 먼저 쓰게 하는 TLA+ IDE. 초보자에게 어려운 부분을 추상화해 준다. v1.8.0 릴리스를 내려받으며 Java가 필요하다.
• 새 스펙: File > Open Spec > Add New Spec.
• 모듈 문법: MODULE 이름 줄은 대시 4개 이상으로 감싸고, 모듈은 등호 4개 이상(====)으로 끝내며, 이름은 파일 이름과 대소문자까지 같아야 한다. 저자는 이를 "역사적 이유"라고 농담한다.
• 모듈 바깥: 모듈 이름 위와 ==== 아래는 무시되므로 메모 자리로 쓴다.
• PlusCal 변환: File > Translate PlusCal Algorithm, 단축키 ctrl+T(Mac은 cmd+T). 이 과정은 PlusCal로 가르친다.
• 모델 실행: TLC Model Checker > New Model → "What is the behavior spec"을 "Temporal Formula" + "Spec"으로, "Invariants" 상자에서 Add로 NoOverdrafts 입력 → 실행(F11).
• 에러 트레이스(error trace): 불변식이 깨지기까지의 정확한 스텝을 툴박스 오른쪽에 보여 준다. 읽는 법은 불변식 작성하기 장에서 다룬다.
• 스크래치 파일(scratch file): 스펙 전체를 돌리지 않고 연산자 출력만 시험하는 별도 스펙. 일반 모델과 다른 점은 둘 — behavior spec을 "no behavior spec"으로 두고, "Evaluate Constant Expression" 상자에 Eval을 넣으면 결과가 "Value" 상자에 뜬다.
• >>> 표기: >>> 식 다음 줄의 결과는 Eval == 식으로 얻은 출력이라는 가이드 전반의 관례다(>>> 1+1 → 2).

---- MODULE scratch ----
EXTENDS Integers, TLC, Sequences

Eval == 0
====

함정 behavior spec이 "Temporal Formula"/"Spec"으로 잡히지 않으면 ====가 한 벌뿐인지, 변환된 TLA+가 그 위에 있는지 확인한 뒤 두 필드를 직접 설정한다. 파일 맨 위 MODULE 줄과 맨 아래 ==== 줄은 각각 하나만 있어야 하고, 파일을 Wire.tla로 저장했다면 모듈 이름도 바꿔야 한다. 저자는 스크래치 파일을 하나 만들어 두기를 권한다.

완역 읽기 → 환경 설정

연산자와 값 Operators and Values

TLA+의 두 기본 재료인 연산자(== 정의·IF-THEN-ELSE·LET)와 값(문자열·불리언·정수·시퀀스·집합)을 익힌다. 24시간 시계 예제로 "값의 집합"을 만들고, CHOOSE로 알고리즘 대신 정의에 가깝게 스펙을 쓰는 법을 배운다.

• 연산자(operator): 프로그래밍의 함수에 해당한다. Op(a, b) == expr(등호 두 개). 인자 수가 고정이라 기본값·오버로딩·선택 인자가 없다. 인자 없는 연산자는 괄호를 생략하며 사실상 상수다. 고차·재귀 연산자와 람다는 연산자 더 알아보기 장에서 다룬다.
• 식(expression): 연산자의 우변. 식을 짜는 키워드는 LET, case 문(드묾), IF-THEN-ELSE 셋이다. 식은 항상 값이 있어야 하므로 ELSE는 필수다.
• 값 타입: TLA+는 수학에 뿌리를 둬 타입이 없지만(untyped) TLC는 원시 4종(문자열·불리언·정수·모델 값)과 복합 4종(집합·시퀀스·구조체·함수)을 구분한다. 연산자는 타입별로 나뉘고 겹치는 것은 =·#(같지 않다)뿐이다. 타입이 다른 값끼리 비교하면 에러다.
• 정수·문자열: 산술은 EXTENDS Integers가 필요하다. 문자열은 큰따옴표만 쓰고 연산은 =·#뿐이라 불투명한 식별자로 쓴다(조작이 필요하면 시퀀스로 저장). 부동소수점은 없다 — 보통 추상화로 없애고, 꼭 필요하면 TLA+가 맞지 않는 도구다.
• 불리언: TRUE·FALSE, /\(and), \/(or), ~(not).
• 함의(implication) A => B: A가 참이고 B가 거짓일 때만 FALSE. ~A \/ B, 대우 ~B => ~A와 같다. 제어 흐름엔 쓸모없지만 스펙 작업에선 극히 중요하다. A <=> B는 둘 다 참이거나 둘 다 거짓(A = B와 같음).
• 글머리표 표기: /\·\/를 줄머리에 세워 논리식을 구조화한다. 언어에서 공백이 의미를 갖는 유일한 곳이라 들여쓰기가 바뀌면 뜻이 바뀐다. 첫 항 앞의 /\는 선택이다.
• 시퀀스(sequence): <<a, b, c>>, 조회는 seq[n], 인덱스는 1부터(1..Len(seq)). Sequences 모듈의 Append·\o(연결)·Head·Tail·Len·SubSeq. 튜플은 고정 길이 시퀀스의 다른 이름이다. EXTENDS는 한 줄에 쉼표로 쓴다(EXTENDS Integers, Sequences).
• 집합(set): 순서·중복 없는 모음 {…}. 중첩은 되지만 타입은 못 섞는다({1, "a"} 무효). \in·\notin·\subseteq(부분집합 또는 같음)·\union(\cup)·\intersect(\cap)·\(차집합), 원소 수는 FiniteSets의 Cardinality.
• 값의 집합: BOOLEAN = {TRUE, FALSE}, a..b(a > b면 {}), 데카르트 곱 \X(튜플의 집합, 결합 법칙 불성립), SUBSET S(멱집합). 문자열만 예외다(STRING은 무한 집합).
• 맵·필터: {f(x): x \in S} / {x \in S: P(x)} — 콜론을 "where"로 읽으면 구분된다. 시퀀스의 치역(range)도 맵으로 구한다.
• CHOOSE x \in S: P(x): 조건을 만족하는 값을 고른다. 없으면 TLC 에러, 여럿이면 결과는 결정적이다(TLC는 조건에 맞는 가장 작은 값을 고른다). 값을 알고리즘으로 "구성"하는 대신 정의로 "선택"하게 해 준다.
• LET … IN: 지역 하위 연산자 정의. 매개변수를 받을 수 있고, 여러 개를 두어 앞선 정의를 참조하며 단계별로 쌓는다.
• 시계 예제: AddTimes(<<2, 0, 1>>, <<1, 2, 80>>)가 불가능한 <<3, 2, 81>>을 내놓으면서 "유효한 시계 값의 집합" ClockType(원소 86400개)이 필요해진다. 프로그래밍식 ToClock2(90000)은 <<25, 0, 0>> 같은 엉터리 값을 조용히 내지만, CHOOSE판 ToClock(86401)은 TLC 에러로 엣지 케이스를 드러내고 % 86400으로 보강된다.

ToSeconds(time) == time[1]*3600 + time[2]*60 + time[3]
ClockType == (0..23) \X (0..59) \X (0..59)
Squares == {x*x: x \in 1..4}
Evens == {x \in 1..4: x % 2 = 0 }
Range(seq) == {seq[i]: i \in 1..Len(seq)}

ToClock(seconds) ==
  LET seconds_per_day == 86400
  IN CHOOSE x \in ClockType: ToSeconds(x) = seconds % seconds_per_day

함정 연산자 정의에 = 하나를 쓰거나 비교에 ==를 쓰면 파서 에러가 나고, EXTENDS를 두 줄로 써도 에러다. CHOOSE 실패("no element of S satisfied P")는 식이 틀렸거나, 있어야 할 값이 없는 실제 시스템 결함이다 — 저자는 99%가 미처 고려하지 못한 엣지 케이스라고 본다. 빈 값 검사는 set = {}, seq = <<>>. 부분집합 검사에 S \in SUBSET T는 매우 비효율적이니 S \subseteq T를 쓰고, SUBSET ClockType(2^86400개)은 만들지 않는다.

완역 읽기 → 연산자와 값

스펙 작성하기 Writing Specifications

TLA+ 입문용 언어 PlusCal의 문법과 레이블 규칙을 배워 중복 검사기 알고리즘을 쓰고, 시작 상태를 집합으로 선언해 입력 1만 개를 한 번에 검사한다.

• 액션의 시간 논리: TLA+ = Temporal Logic of Actions. 액션(action)은 시스템 상태 변화를 기술한 것이다. 범용적이라 복잡하고 배우기 어렵다.
• PlusCal: 2009년 Leslie Lamport가 만든 DSL. 프로그래밍 언어에 가까운 문법이 TLA+ 액션으로 컴파일된다. 날것의 TLA+보다 덜 강력해 못 쓰는 스펙도 있지만 많은 스펙에서 더 단순하다. 저자 경험상 PlusCal부터가 수월해 입문 파트를 PlusCal로 진행한다(수학 성향이면 TLA+ 장으로 건너뛰어도 된다).
• 알고리즘 블록: 주석 (* *) 안에서 --algorithm 이름으로 시작해야 한다(아니면 일반 주석). 이름은 모듈 이름과 무관하다. variables(어떤 TLA+ 값이든 가능) 뒤 본문은 begin … end algorithm.
• := vs =: :=는 기존 변수 갱신 전용. 초기값과 with 임시 할당은 =, 본문 안의 =는 비교다.
• 변환(translate): cmd-T/ctrl-T. \* BEGIN TRANSLATION ~ \* END TRANSLATION 사이에 생성된 TLA+가 실제로 모델 체킹된다. 우클릭의 "Translate PlusCal Automatically"로 자동 변환할 수 있다(순수 TLA+ 스펙에선 에러).
• 레이블(label): 시스템의 한 스텝에 일어날 수 있는 모든 것. 레이블 하나는 원자적(atomic)이고 시간이 흐르지 않으며, 레이블과 레이블 사이에 시간이 흐른다. 레이블이 곧 TLA의 액션이고, 배치로 시스템이 얼마나 동시적인지 명세한다(100개 합산 수십 ns vs HTTP 요청·응답 수십 ms — 합산을 while로 쪼개면 그 사이에 요청이 끼어들 수 있다).
• 레이블 규칙: 모든 문장은 어떤 레이블에 속한다(알고리즘은 레이블로 시작). 변수는 레이블당 한 번만 갱신한다 — 시퀀스 두 칸도 위반이며, 같은 변수의 여러 부분은 동시 할당 ||로 갱신한다.
• skip · assert · goto: skip은 아무것도 안 한다. assert expr는 거짓이면 TLC가 즉시 실패한다("레이블 안은 한꺼번에" 원칙의 예외, EXTENDS TLC 필요). goto L은 L로 점프하며 바로 뒤에 레이블이 와야 한다.
• if/elsif/else: 분기 안에 레이블을 둘 수 있고 분기 간 균형은 필요 없다. 단 어느 분기에든 레이블이 있으면 블록 뒤에 레이블이 와야 한다.
• 레이블은 중첩되지 않는다: B에 들어가는 순간 A를 벗어난다. "B는 A에서만 도달 가능하다"가 올바른 멘탈 모델이다.
• macro · with: macro는 begin 위에 두는 텍스트 치환 규칙이라 넘긴 변수 자체가 갱신된다. with는 레이블 중간의 임시 할당(=). 둘 다 레이블을 담을 수 없다.
• while: 유일한 루프. 앞에 반드시 레이블이 온다. 비원자적이라 매 반복 후 루프 레이블로 돌아가며, 그사이 다른 프로세스가 실행될 수 있다.
• 작성 흐름: 고수준 목표를 연산자로(IsUnique(seq)) → 알고리즘 작성 → 둘이 일치하는지 검증(다음 장).
• TLC 결과 화면: 지름(diameter, 가장 긴 행동의 길이), 발견 상태 수(중복 포함), 서로 다른(distinct) 상태 수, 큐, 해시 충돌 확률(실무상 무시), 레이블별 실행 횟수(0이면 스펙 버그 의심). 이후 스펙 목록 아래엔 "상태 / 서로 다른 상태" 수치를 적는다.
• 행동(behavior)과 다중 시작 상태: 행동은 하나의 완전한 실행으로, 시작 상태마다 하나씩 생긴다. \in으로 변수가 집합의 어떤 원소로 시작한다고 선언하면 TLC가 모든 시작 상태를 검사한다. 상태 공간은 곱으로 커질 수 있지만 상태가 수렴하면 서로 다른 상태는 훨씬 적다.
• 러닝 예제 duplicates: seq = <<1, 2, 3, 2>> 하나면 7 states / 6 distinct, 입력 두 개면 행동 두 개, S == 1..10으로 입력 10,000개면 70000 states / 60000 distinct.

Iterate:
  while index <= Len(seq) do
    if seq[index] \notin seen then
      seen := seen \union {seq[index]};
    else
      is_unique := FALSE;
    end if;
    index := index + 1;

S == 1..10
  variable seq \in S \X S \X S \X S;

함정 assert가 실패하면 에러 트레이스가 원인 스텝을 보여 주지 않으므로 저자는 불변식을 권한다. 변환을 잊지 말 것(자동 변환 옵션). 커버리지는 보장이 아니다 — -187에서만 터지는 버그도 있을 수 있고, TLA+는 엔지니어링 판단을 보강할 뿐 대체하지 못한다. 시퀀스 길이가 4로 고정된 구멍은 구조화된 데이터 장에서 메우며, 이 장은 아직 정답을 검증하는 속성을 쓰지 않았다.

완역 읽기 → 스펙 작성하기

불변식 작성하기 Writing an Invariant

에러 없이 도는 스펙도 틀릴 수 있다. 중복 검사기에 타입 불변식과 정확성 불변식을 붙이고 에러 트레이스·pc·=>·\A/\E를 익혀, "알고리즘 + 정확성 불변식 + 둘을 대조하는 모델"을 갖춘 완전한 스펙을 만든다.

• 불변식(invariant): 초기값이나 현재 위치와 상관없이 모든 상태에서 참이어야 하는 것. 모델에 추가하면 TLC가 가능한 모든 상태에서 검사하고, 통과하면 불변식이 없을 때와 똑같아 보이며 실패할 때만 무언가를 보여 준다.
• 타입 불변식(type invariant): 가장 흔한 불변식. TLA+의 "타입"은 값의 임의 집합일 뿐이라 정수보다 정밀하게 지정한다(index \in 1..Len(seq)+1, seen \subseteq S).
• define 블록: 변수 선언과 알고리즘 본체 사이에 두는 순수 TLA+ 연산자 모음. PlusCal 변수를 참조할 수 있다.
• 에러 트레이스 읽기: 위 상자는 위반된 불변식, 아래 상자는 초기 상태(<Initial Predicate>)부터의 스텝과 각 액션 후 변수 값이다. 바뀐 값은 빨간색이고 마지막 스텝이 실패한 스텝이다. seq처럼 집합에서 시작한 변수는 고정된 한 값으로 나온다.
• pc 변수: 변환기가 레이블을 추적하려고 추가하는 변수("새는 추상화"). 값은 다음에 평가할 레이블 이름 문자열로, 시작은 "Iterate", 완료 후 "Done".
• 함의 A => B: IF A THEN B ELSE TRUE와 같다. 불변식을 특정 조건에서만 적용할 때 쓴다(예: 끝났을 때만 검사).
• 한정자(quantifier): \A x \in S: P(x)(모든 원소), \E x \in S: P(x)(적어도 하나). 빈 집합에서 \A는 항상 참, \E는 항상 거짓 — forall이 참인데 exists가 거짓인 유일한 경우다.
• 다중 바인딩: \E m, n \in 2..num(m과 n은 같은 값일 수 있다), 서로 다른 집합에서 \A x \in S, y \in T: P(x, y).
• 시퀀스에 한정자: 시퀀스는 집합이 아니라서 인덱스 집합 1..Len(seq)에 건다. 원치 않는 조합은 i # j => …로 걸러낸다.
• 정확성 불변식 만들기: is_unique = TRUE를 넣어 일부러 실패시킨 트레이스로 읽는 법을 익힌다. IF is_unique THEN IsUnique(seq) ELSE ~IsUnique(seq)는 is_unique = IsUnique(seq)로 줄고, is_unique가 TRUE로 시작하므로 pc = "Done" =>를 붙인다.
• IsUnique 다듬기: 1차 Cardinality(seen) = Len(s)는 통과하지만 저자는 엉터리로 본다 — 실제 행동인 seen에 묶여 있고, 정의가 아닌 요령이며, 확장되지 않는다. 2차 \A i, j \in 1..Len(s): s[i] # s[j]는 i = j인 쌍 때문에 고유한 시퀀스도 실패한다(스크래치에서 CHOOSE로 <<1, 1>> 확인). i # j =>를 붙이면 통과한다(70000 / 60000).
• 관용구: 알고리즘 + 정확성 불변식 + 모델은 이진 탐색·위상 정렬·SAT 솔버 같은 CS 알고리즘 모델링에 쓰이고, 최적화가 구현을 틀리게 만들지 않는지도 검사할 수 있다.

TypeInvariant ==
  /\ is_unique \in BOOLEAN
  /\ seen \subseteq S
  /\ index \in 1..Len(seq)+1

IsCorrect == pc = "Done" => is_unique = IsUnique(seq)

IsUnique(s) ==
  \A i, j \in 1..Len(s):
    i # j => s[i] # s[j]

함정 assert 실패 트레이스는 단언이 실패하기 직전 스텝에서 끝난다(불변식 실패와 다르다). =>도 글머리표 들여쓰기 규칙을 따라 /\ A, /\ B 다음 줄에 글머리표보다 안쪽으로 들여 쓴 => C는 A /\ (B => C)로 읽힌다 — 헷갈리면 괄호를 쓴다. =>를 \E와 섞지 마라: \E i, j: i # j => seq[i] = seq[j]는 i = j만 골라도 참이 되므로 i # j /\ seq[i] = seq[j]로 쓴다. 한정자 실습은 자기 스펙 대신 스크래치 파일에서 하길 권한다.

완역 읽기 → 불변식 작성하기

스펙 매개변수화 Parameterizing Specs

하드코딩한 값을 CONSTANT로 빼서 모델 실행마다 고르고, ASSUME으로 무의미한 값을 막으며, 모델 값·대칭 집합으로 센티널을 안전하게 표현하고 상태 공간을 줄인다.

• 상수(constant): 모델 실행마다 설정하는 값(커맨드라인 플래그에 비유). CONSTANT S, 여러 개는 CONSTANT S, Length. TLA+의 "상수"는 "절대 변하지 않는 값"이 아니며, 그런 값은 인자 0개 연산자일 뿐이다. 값을 안 정한 채 돌리면 툴박스가 알려 주고 모델 설정 화면에서 넣는다.
• 세 가지 할당: 일반 할당(ordinary assignment), 모델 값, 모델 값의 집합.
• 일반 할당: 유효한 TLA+ 식이면 무엇이든 된다. 저자 표기 S <- 1..10. 반복 개발용 작은 모델과 최종 테스트용 큰 모델을 따로 둘 수 있다.
• ASSUME: 올바른 상수를 넣었는지 검사한다. 연산자·상수엔 의존할 수 있지만 변수엔 못 한다. 모델 실행 전에 검사되며 실패하면 Error: Assumption … is false. 상수가 무엇이어야 하는지 알려 주는 문서 역할도 한다.
• 모델 값(model value): 연산이 없고 동등성만 검사되며 오직 자기 자신과만 같은 값(숫자·문자열·튜플·다른 모델 값과 모두 다름). NULL·NotYetAccessed 같은 센티널에 쓰고, 일반 할당 안에서도 쓸 수 있다(Set <- {1, 2, X}).
• 모델 값의 집합: 보통 집합처럼 따옴표 없이 입력한다(S <- [model value] {s1, s2, s3, s4, s5}). 동시성 모델링에서 매우 유용해진다.
• 대칭 집합(symmetry set): 모델 값의 집합에 켜는 TLC 최적화. 원소를 서로 바꿔 치기만 한 상태를 같은 상태로 본다 — 모델 값이 동등성만 지원하기에 성립한다(<<s1, s2, s2>>와 <<s2, s3, s3>>는 같지만, 정수 <<1, 2, 2>>와 <<2, 3, 3>>는 s[1] + s[2]가 달라 대칭이 아니다).
• 결과: 저자 추정으로 S를 1..100으로 넓히면 상태가 70,000개에서 5억 개 이상으로 는다 → 평소엔 작은 값으로 빠른 피드백, 뻔한 문제를 털어낸 뒤 큰 값. S <- {}나 {1, 2}는 무의미하므로 ASSUME Cardinality(S) >= 4. 모델 값 집합 {s1, …, s5}는 4,375개 상태(1..5와 같음), 대칭 집합이면 715개.

CONSTANT S
ASSUME Cardinality(S) >= 4

CONSTANT DEBUG
ASSUME DEBUG \in BOOLEAN

Inputs ==
IF DEBUG
THEN {<<1, 2, 3, 4>>}
ELSE S \X S \X S \X S

함정 널 가능 값을 "null" 문자열과 비교하면 값이 정수일 때 타입이 다른 비교라 TLC 에러가 나고, -1 같은 센티널은 다른 수치 계산에 실수로 섞일 위험이 있다 — 모델 값 NULL이면 숫자일 때 IF last_access_time = NULL이 그냥 거짓이 된다. 대칭 집합이 항상 빠르지는 않다: 대칭 계산 오버헤드 때문에 저자 컴퓨터에선 원소 8개 대칭 집합이 일반 모델 집합보다 2분 더 걸렸다. 상수엔 제약 가정을 붙이고 DEBUG 같은 헬퍼 상수를 두려워하지 마라(이 책 예제는 단순함을 위해 평소보다 많이 하드코딩한다).

완역 읽기 → 스펙 매개변수화

구조화된 데이터 Structured Data

구조체와 시퀀스는 문법적 설탕이고 TLA+의 진짜 컬렉션은 집합과 함수 둘뿐이다. 함수 집합 [S -> T]로 타입 불변식을 쓰고, 중복 검사기의 입력 길이까지 상수로 빼 상태 스위핑으로 상한(Size) 이하의 모든 길이를 검사한다.

• 구조체(struct): 문자열 키 해시맵. [a |-> 1, b |-> {}], 인덱싱은 struct["a"] 또는 struct.a. 조직화된 데이터 묶음(예: 계좌·금액·입출금 구분의 BankTransaction)을 표현한다.
• 구조체 집합: [acct: Accounts, amnt: 1..10, type: {…}] = 각 필드가 해당 집합에 속하는 모든 구조체. 타입 불변식에 쓴다.
• DOMAIN: 구조체의 모든 키 집합(구조체엔 Len이 없다). 시퀀스에선 1..Len(seq)처럼 보이지만 실제로는 Len이 DOMAIN으로 정의된다.
• 함수(function): 프로그래밍의 함수(그건 연산자에 가깝다)가 아니라 한 집합의 값을 다른 집합으로 대응시키는 수학적 사상. [x \in S |-> expr], 출발 집합 S가 정의역(domain) = DOMAIN F. 시퀀스는 정의역이 1..n인 함수, 구조체는 정의역이 문자열 집합인 함수이며, 정의역은 어떤 집합이든 된다.
• 다인자 함수: [p \in S \X S |-> …], [x \in S, y \in S |-> …], [x, y \in S |-> …]. 호출은 Prod[3, 5]처럼 꺾쇠괄호를 생략할 수 있고, 내부적으로 튜플이라 DOMAIN F = S \X T.
• 펼친 형태(expanded form): 스크래치 파일의 함수 출력 형식. x :> y는 x를 y로 보내는 단일 값 함수, f @@ g는 두 함수 병합(키가 겹치면 왼쪽 값 유지). 둘 다 EXTENDS TLC가 필요하다(>>> 1 :> "a" @@ 2 :> "b" → <<"a", "b">>).
• 함수는 값이다: 계산에는 연산자가 훨씬 낫다. 함수는 변수에 담고 다른 값처럼 조작하는 용도로 중요하다.
• 함수 집합(function set) [S -> T]: 정의역이 S이고 모든 값이 T(공역, codomain)에 속하는 모든 함수. 원소 수는 T 원소 수의 (S 원소 수)제곱. 공역에 맵·필터를 결합할 수 있다({set \in SUBSET CPUs: Cardinality(set) <= 2}).
• 원소 수 어림: 계좌 3개면 BankTransactionType = 3·10·2 = 60개, 작업 2·CPU 3이면 [Tasks -> SUBSET CPUs] = 64개, [1..n -> BOOLEAN] = 2^n개.
• 함수 집합 예: 서버 상태 [Server -> {"online", "booting", "offline"}], 방향 그래프 [Node \X Node -> BOOLEAN](대칭 조건으로 걸러 무방향 그래프), 자원 할당 [Resource -> User]·미할당 허용 [Resource -> User \union {NULL}](NULL은 모델 값).
• 정의로 계산하기: Python zip은 두 DOMAIN의 교집합으로 반복·재귀 없이 쓴다. Sort는 CHOOSE sorted \in [DOMAIN seq -> Range(seq)]로 정의하는데, IsSorted만 요구하면 <<>>를 돌려줘도 통과하므로 원소 개수 일치(CountMatching) 조건을 더한다. CPU 할당 불변식 OnlyOneTaskPerCpu는 \A 함의식으로도, 할당 집합이 서로소라는 형태로도 쓸 수 있다.
• 상태 스위핑(state sweeping): 초기 상태 변수 하나로 다른 변수들의 매개변수(입력 시퀀스 길이, 버퍼 최대 크기 등)를 제어하는 기법. 필수는 아니지만 훨씬 쉬워 두뇌를 명세 자체에 쓰게 해 준다.
• 중복 검사기 마지막 회: [1..3 -> S] = S \X S \X S이므로 seq \in [1..5 -> S]로 바꾸고(800000 / 700000) → 길이를 상수 Size로 → n \in 1..Size로 길이 5 이하를 전부 검사한다(876540 / 765430).

struct == [a |-> 1, b |-> {}]
BankTransactionType == [acct: Accounts, amnt: 1..10, type: {"deposit", "withdraw"}]
RangeStruct(struct) == {struct[key]: key \in DOMAIN struct}

CONSTANT S, Size
ASSUME Size > 0
variable
  n \in 1..Size;
  seq \in [1..n -> S];

함정 구조체 키에 따옴표를 붙인 ["key" |-> val]은 파서 에러, 구조체 집합의 [key: "val"]은 모델 체킹 시점 에러다 — [key: {"val"}]가 맞다. 함수 집합은 ->, 함수는 |->이며 저자는 누구나 한 번은 헷갈린다고 본다. 복잡한 타입일수록 집합 원소 수를 주기적으로 어림하고, 원하는 속성의 값을 직접 구성하기보다 집합에서 CHOOSE로 골라내라.

완역 읽기 → 구조화된 데이터

비결정성 Nondeterminism

with x \in set(값 선택)과 either … or(분기 선택)로 무작위성·사용자 입력·센서값·실패 경로를 모델링하고, 구현 세부를 고수준 스텝으로 추상화한다. "도달하지 않는다"는 불변식을 일부러 깨뜨려 TLC로 해를 찾는 법도 익힌다.

• 결정적 vs 비결정적: 지금까지는 시작 상태가 여럿이어도 시작 상태마다 행동(behavior)이 고정됐다. 비결정성은 한 스텝에서 여러 가지 일 중 하나를 할 수 있다는 뜻이다.
• 비결정성의 원천 4가지: 무작위성, 대화형 시스템(사용자가 무엇을 어떤 순서로 할지 모름), 센서(범위는 알지만 값은 모름), 독립적으로 움직이는 여러 부분(실행 순서를 모름 = 동시성, 다음 장).
• with x \in set: = 대신 \in을 쓰면 집합의 아무 원소나 고른다. TLC는 모든 값을 시도해 원소 수만큼 새 행동을 만든다. 한 with 안에 x \in BOOLEAN과 z = TRUE처럼 비결정·결정 할당을 섞을 수 있다.
• 집합 변수에서 꺼내기: with thread \in sleeping처럼 변수에 든 집합에서도 고른다. 집합이 비면 with가 블록되어 데드락으로 이어질 수 있다.
• either / or: 비결정적 제어 흐름. TLC는 분기마다 갈래를 만든다. 분기 안에 레이블을 둘 수 있어 상태 기계 구현에 특히 유용하다.
• 추상화 수단: 명세가 프로그래밍 언어와 크게 갈라지는 첫 지점이다. 실패 경로("새드 패스")를 세부 없이 "성공 또는 에러"로 줄인다. 흔한 패턴이 either … or skip(성공 분기 + 아무것도 안 하는 실패 분기)이다.
• 에러 종류: 복구 로직이 에러 종류에 따라 다르면 신경 쓰는 만큼만 with reason \in {...}로 표현한다.
• 외부 행위: 들어오는 요청을 특정하지 않고 레코드 집합 RequestType을 정의해 요청마다 거기서 꺼낸다. 예상 밖 분기는 assert FALSE로 스펙 오류를 잡는다.
• 불변식을 탐색 도구로: 목표에 "도달하지 않는다"는 불변식(Invariant == sum # Target)을 넣으면, 도달 가능할 때 TLC가 실패하며 그 경로를 에러 트레이스로 보여 준다.
• 상태 수 비율: 비결정성은 (본 상태 / 고유 상태)와 (본 상태 / 초기 상태) 비율을 크게 올린다. 순서만 다른 경로가 같은 상태로 합쳐지고(5+3 = 3+5), 시작 상태마다 행동이 여럿이 되기 때문이다.
• 계산기 예제: while i < NumInputs 루프에서 with x \in Digits(0..9)로 더하는 v1은 NumInputs <- 5에서 1043 states / 187 distinct, either로 덧셈·뺄셈·곱셈 3분기를 넣은 v2는 71333 / 16551이다. v3는 Target <- 417로 돌려 트레이스 sum 0 → 1 → 10 → 60 → 420 → 417을 얻는다. 저자가 Target을 0~1000까지 바꿔 가며 돌린 결과, 5번 입력으로 도달 못 하는 가장 작은 수는 851이었다.

with roll \in 1..6 do
  sum := sum + roll;
end with;

macro request_resource(r) begin
  either
    reserved := reserved \union {r};
  or
    \* Request failed
    skip;
  end either;
end macro;

함정 빈 집합에서 with로 고르면 블록되어 데드락 위험이 있다. while TRUE에 누적 변수를 두면 상태 공간이 무한해 모델 체커가 끝나지 않으므로, 입력 횟수를 모델 상수(NumInputs)로 한정하고 입력 도메인을 0..9처럼 좁혀라. 실패 원인을 전부 명세하는 것은 큰 비용이다 — 워크플로의 작은 부분이면 either … or skip으로 추상화하고 큰 그림에 집중한다.

완역 읽기 → 비결정성

동시성 Concurrency

PlusCal의 동시성 단위인 프로세스(단일·집합, self, 지역 변수)와 await·데드락·프로시저를 reader/writer 큐 예제로 익히고, 스레드 카운터 예제로 경쟁 조건 → 락 → 불변식 확장을 거쳐 "불변식만으로는 부족하다"는 결론에 이른다.

• 동시성: 여러 독립 행위자가 스펙 안에서 상호작용하는 것. 흔하고 추론하기 어려워 정형 기법의 핵심 셀링 포인트다.
• 프로세스: 동시성의 기본 단위(OS 프로세스·스레드·다른 머신의 프로그램·사람까지). process name = val … end process. 모든 프로세스 값은 비교 가능한 같은 타입이어야 하고(예외: 모델 값), 서로 다른 프로세스는 레이블 이름을 공유할 수 없다.
• 순서 비결정: 프로세스 간 순서를 정하지 않으면 TLC가 모든 순서를 탐색한다. 비원자적 while은 반복 하나하나가 별개 액션이라 조합이 늘어난다.
• 빈 큐 읽기 = 명세 결함: 빈 시퀀스에 Head를 적용하면 TLC가 "unexpected exception"을 보고한다. 대안은 건너뛰기·reader 블록·기본값·시스템 일부로서의 에러이며, 예제는 if로 무시한다.
• pc 함수: 다중 프로세스에서 변환기는 pc를 프로세스 값 → 레이블 문자열 함수로 바꾼다(reader의 레이블은 pc[0]).
• 지역 변수: process … variables i = 0; begin, 시작값 여러 개(i \in 1..3)도 가능. define 연산자가 참조할 수 없어 실무에선 드물고, 루프 반복·모델 경계 같은 장부 기록용으로 쓴다.
• 프로세스 집합: process name \in set은 원소마다 프로세스 하나. reader와 writer를 여럿 두려면 겹치지 않는 같은 타입이 필요해 모델 값 집합 두 개가 가장 쉽다. writer 3 + reader 1이면 액션 순서가 4! = 24, 하나 더면 120으로 폭발한다.
• goto: goto ReadFromQueue;는 레이블을 while TRUE에 넣는 것과 같다.
• self: 프로세스 집합에서 자기 값을 돌려준다(매크로 안에서도 가능). 단독 정의 프로세스엔 없으므로 process P \in {val}로 우회한다.
• await: 레이블 안의 모든 await가 참일 때만 레이블이 실행된다. 빈 집합 with도 블록한다. 갱신된 변수를 직접 쓰면 갱신값 기준이지만 define 연산자를 거치면 아니므로, 갱신한 변수를 await에 쓰지 않는다.
• 데드락: 어떤 프로세스도 진행할 수 없으면 TLC가 에러로 보고한다(모델 설정에서 끌 수 있음). 모든 프로세스가 끝나면 변환기가 넣은 Terminating 액션 덕에 데드락이 아니다.
• 프로시저(선택 학습): 레이블을 담을 수 있는 매크로 유사물. 호출 스택 때문에 EXTENDS Sequences가 필수다. return은 값 없이 제어만 돌려주고, 빠지면 TLC 에러다. call Name(...) 뒤엔 goto·레이블·(프로시저 안이면) return이 와야 하며, 매크로 뒤·프로세스 앞에 정의한다.
• 경쟁 조건과 락: 비원자적 갱신을 레이블 분할(tmp := counter → counter := tmp + 1)로 모델링하고, await lock = NULL; lock := self;로 락을 건다.
• 타입 불변식: 값마다 대략적 집합으로 느슨하게. 지역 변수 tmp를 참조하면 \* END TRANSLATION 뒤, ==== 앞에 둔다.
• 불변식의 한계: "카운터는 증가만 한다", "락을 훔치지 않는다"는 잘못된 상태가 아니라 잘못된 전이다. AllDone => …은 끝나지 않으면 자명하게 통과한다 → "언젠가는 올바른 결과"가 필요하다(다음 장).
• 예제 흐름: reader_writer는 writer 1개(3 states / 2 distinct)에서 시작해 빈 큐 실패 → if(7/5) → self 적재(69/38) → writer await(33/20)를 거치고, reader까지 await하면 데드락으로 실패한다. threads는 원자적 증가 6/4로 통과, tmp 경유 비원자 갱신은 둘 다 0을 읽어 실패, 락 추가로 19/17 통과.

process writer \in Writers
begin
  AddToQueue:
    await queue = <<>>;
    queue := Append(queue, self);
end process;

TypeInvariant ==
  /\ counter \in 0..NumThreads
  /\ tmp \in [Threads -> 0..NumThreads]
  /\ lock \in Threads \union {NULL}

함정 NULL은 -1로도 되지만 숫자로 오용되지 않게 모델 값을 강력히 권한다. ReleaseLock에는 assert lock = self를 넣는 것이 좋다. 불변식이 없어도 정기적으로 모델 체킹해 애매한 경우를 일찍 잡고, 실행 전에 에러·스텝 수·프로세스 순서를 예측하는 연습을 하면 경쟁 조건에 대한 직관이 빨리 자란다.

완역 읽기 → 동시성

시간 속성 Temporal Properties

불변식은 특별한 개념이 아니라 시간 속성의 한 종류일 뿐이다. []·<>·~>와 공정성(fair, fair+)으로 행동 전체에 대한 안전성·라이브니스 속성을 쓰고 TLC로 검사한다.

• 시간 속성(temporal property): 시간에 걸친 논리 명제로, 모든 속성을 아우르는 범주다. TLC가 불변식을 따로 제공하는 이유는 실용성과 효율이다.
• 안전성 vs 라이브니스: 안전성(safety)은 "나쁜 일이 일어나지 않는다", 라이브니스(liveness)는 "좋은 일이 일어난다"(예: 모든 트랜잭션은 완료되거나 롤백된다). 모든 불변식은 안전성 속성이지만 역은 아니다 — "특정 서버 하나가 행동 내내 온라인"은 단일 상태만 보고는 판단할 수 없다.
• []P (항상): 모든 상태에서 P가 참. 맨 바깥의 []P는 불변식과 같다. 박스 없이 P를 속성으로 넣으면 첫 상태만 검사한다. []P \/ []Q, []P => []Q, 한정자 안의 []도 쓸 수 있다.
• ~[]P: 모든 행동에 P가 거짓인 상태가 적어도 하나 있다는 뜻이며, 라이브니스 속성이다.
• 스터터 스텝(stutter step): 아무것도 바뀌지 않는 새 상태. 어떤 행동이든 무한히 스터터할 수 있다(= 크래시). 불변식은 스터터로 깨지지 않지만 라이브니스는 깨진다. TLA+는 최악의 시나리오 언어라서, 명시하지 않으면 최악의 순간에 크래시한다고 가정한다.
• 약한 공정성(fair process): 프로세스가 항상 진행 가능하면 언젠가 진행한다(영원히 멈출 수 없다).
• 강한 공정성(fair+, 액션 단위 AwaitLock:+): 간헐적으로라도 항상 다시 진행 가능해지면 언젠가 진행한다 — 락 경쟁에서 한 스레드의 기아를 막는다. 공정성은 선택이다: 로그오프할 수 있는 사용자 프로세스처럼 액션이 보장되지 않는 것은 공정하게 만들지 않는다.
• <>P (언젠가는): ~[]~P와 같다. 모든 행동의 적어도 한 상태에서 P가 참.
• <>[]P와 []<>P: 언젠가부터 영원히 P(수렴) / 항상 언젠가는 다시 P. 시계에서 []<>(time = midnight)는 참, <>[](time = midnight)는 거짓이다.
• P ~> Q (leads-to): =>의 시간적 대응물. P가 참이 될 때마다 Q가 지금 또는 미래에 참이 된다.
• 예제에서 배우는 것: ① 서버 오케스트레이터의 Safety(\E s \in Servers: [](s \in online), 늘 온라인인 서버가 하나는 있다)는 모든 상태에 온라인 서버가 있는데도 실패한다 — s1이 빠졌다 돌아온 뒤 s2가 빠지니 끝까지 온라인인 서버는 없다. 상태 하나가 아니라 행동 전체를 봐야 보이는 버그다. ② Liveness(~[](online = Servers))는 첫 상태에서 영원히 스터터할 수 있어 실패하고, fair process로 바꾸면 통과한다. ③ 스레드들이 락을 다투면 약한 공정성으로는 한 스레드가 계속 락을 가로챌 수 있어 \A t \in Threads: <>(lock = t)가 실패한다 — 여기엔 fair+가 필요하다. ④ 초기값을 counter = 1로 잘못 둔 버그는 <>로는 놓친다(목표값을 한 번 지나가기 때문). <>[]로 “결국 그 값에 머문다”고 써야 잡힌다.

Safety == \E s \in Servers: [](s \in online)
Liveness == ~[](online = Servers)

Liveness ==
  \A t \in TaskType:
    t \in inbound
      ~> \E w \in Workers:
        t \in worker_pool[w]

함정 시간 속성은 툴박스의 "Invariants"가 아니라 "Temporal Properties"에 넣는다. 라이브니스 검사는 훨씬 느리므로 안전성용 큰 상수 모델과 라이브니스용 작은 상수 모델을 따로 두고, 라이브니스에는 대칭 집합을 쓸 수 없다. TLC는 어느 속성이 깨졌는지 말하지 않고 "Temporal Properties are Violated"만 출력하며 에러 트레이스도 최단이 아니다. 약하게 공정한 프로세스도 스핀락에는 빠질 수 있다. 라이브니스는 불변식보다 드물지만(시스템당 두어 개), 저자는 시스템이 실제로 해야 할 일을 정의하므로 결정적으로 중요하다고 본다.

완역 읽기 → 시간 속성

연산자 더 알아보기 More Operators

지금까지의 문법으로는 번거로운 빈틈(대표 예: 시퀀스 합 SumSeq)을 메우는 고급 연산자를 모은 장이다. 재귀 연산자, 고차 연산자와 LAMBDA, 사용자 정의 이항 연산자, 함수 연산자, CASE를 다룬다.

• 동기: sum.tla의 IsCorrect == pc = "Done" => sum = SumSeq(seq)를 검사하려면 SumSeq가 필요한데, 앞의 문법만으로는 가능하지만 매우 번거롭다. 이 불편 때문에 2008년 TLA+에 재귀 연산자가 추가되었다.
• 재귀 연산자(RECURSIVE): RECURSIVE SumSeq(_)처럼 미리 선언하며 _의 개수가 인자 수다(Op(_, _)). 선언을 LET 안에 넣어 헬퍼 연산자를 만들 수도 있다.
• 종료 검사 없음: 재귀가 끝나는지 문법으로 검사하지 않는다. 끝나지 않으면 TLC가 스택 오버플로 에러를 낸다.
• 집합 재귀와 CHOOSE: CHOOSE x \in set: TRUE로 원소를 골라 재귀한다. 선택이 유일하지 않으면 TLC는 가장 작은 값을 고르므로 SetToSeq({6, 8, 1, 2, -1, 5})는 <<-1, 1, 2, 5, 6, 8>>가 된다. 순서가 결과에 영향을 주면 유일한 선택 술어를 명시한다.
• 고차 연산자와 LAMBDA: 연산자를 인자로 받는다(SeqMap(Op(_), seq)). LAMBDA는 익명 연산자로, SeqMap(LAMBDA x: x + 1, <<1, 2, 3>>)은 <<2, 3, 4>>다. 재귀 연산자와 고차 연산자는 함께 쓸 수 없다.
• 이항 연산자: Sequences가 s \o t == …로 정의하듯 직접 정의할 수 있지만 기호는 고정 목록(\o, +, \prec 등)에서만 고른다. 저자는 스펙이 헷갈려진다며 대체로 쓰지 않지만 set ++ x == set \union {x}, set -- x == set \ {x}는 자주 쓴다.
• 함수 연산자: Double[x \in 1..10] == x * 2는 Double == [x \in 1..10 |-> x * 2]의 문법 설탕이며 주 용도는 재귀 함수(Factorial[x \in 0..10] == IF x = 0 THEN 1 ELSE x * Factorial[x - 1])다.
• CASE: CASE 조건 -> 값 [] … [] OTHER -> 값. 아무것도 일치하지 않고 OTHER도 없으면 에러, 여럿이 일치하면 구현 정의(TLC는 첫 번째)다.

RECURSIVE SumSeq(_)

SumSeq(s) == IF s = <<>> THEN 0 ELSE
  Head(s) + SumSeq(Tail(s))

Fizzbuzz(x) ==
  CASE (x % 3 = 0) /\ (x % 5 = 0) -> "Fizzbuzz"
    [] (x % 3 = 0)                -> "Fizz"
    [] (x % 5 = 0)                -> "Buzz"
    [] OTHER                      -> x

함정 끝나지 않는 재귀는 스택 오버플로로만 드러난다. CHOOSE … : TRUE 기반 집합 재귀는 항상 최솟값부터 고르므로 교환법칙이 성립하지 않는 계산에선 선택 술어를 명시하라. 재귀 연산자와 고차 연산자는 결합할 수 없고, CASE에 OTHER가 없으면 불일치 시 에러가 난다.

완역 읽기 → 연산자 더 알아보기

액션 속성 Action Properties

액션 속성은 상태가 아니라 전이(스텝)에 거는 안전성 속성이다. 프라임(x')과 박스 액션 공식 [][A]_v로 쓰고, TLC에서는 불변식이 아니라 PROPERTY로 검사한다.

• 액션 속성: 시스템이 어떻게 변할 수 있는지에 대한 제약. 불변식을 빼면 가장 큰 부류의 안전성 속성이며 시간 속성으로 검사된다.
• 프라임 x': 스텝이 끝날 때의 x 값 = 다음 스텝이 시작하는 값. 작은따옴표가 이 역할을 하므로 문자열은 큰따옴표여야 한다.
• 액션: 프라임이 들어 있는 연산자.
• 스터터 스텝 문제: 스터터 스텝은 언제 어디에나 끼울 수 있으므로 [](x' = x + 1)은 자명하게 거짓이다. 원한 속성은 x' > x \/ UNCHANGED x다.
• [A]_v: A \/ UNCHANGED v의 문법 설탕. [](x' = x + 1 \/ UNCHANGED x) = [][x' = x + 1]_x.
• 박스 액션 공식(box action formula): [][A]_v 꼴. TLC는 이 형태의 액션 속성만 검사할 수 있고, 다음 장에서 특별한 역할을 한다.
• _x의 효과: [][counter' > counter]_counter는 전개하면 counter' >= counter와 같은 뜻이 되지만, 여기에 기대지 말고 그대로 있어도 된다면 명시한다.
• 헬퍼 액션: 액션 속성 안에서 쓸 수 있다(BecomesNull(x) == x' = NULL).
• 한정자와 액션 속성: TLC는 최상위 액션 속성만 검사한다. 한정자 안에 박스를 넣으면 [] followed by action not of form [A]_v. 에러가 난다. \A x: []P(x) ≡ [](\A x: P(x))이므로 한정자를 액션 안으로 옮긴다.
• 트레이스 탐색기: 프라임 식을 쓰면 다음 스텝에서의 값을 보여 준다.
• 사용 비중: 저자의 스펙에는 불변식 > 액션 속성 > 라이브니스 속성 순으로 많다. 모든 스펙에 라이브니스가 최소 하나 필요하니 그쪽이 더 "중요"하다고 볼 수 있고, 액션 속성은 선택이지만 저자는 그 유연성 때문에 아주 좋아한다.
• 예제에서 배우는 것: threads 스펙에서 IncCounter를 counter := tmp + IF tmp = 0 THEN 1 ELSE -1;로 바꾸면 CounterOnlyIncreases가 counter = 1 → counter = 0 전이에서 실패한다 — counter = 0 상태 자체는 유효하고, 잘못된 것은 감소하는 전이다. 현재 counter 값만 봐서는 감소를 알아챌 수 없고, 전이를 봐야 한다. GetLock의 await lock = NULL;을 지우면 LockCantBeStolen이 실패한다. counters 스펙에서는 박스를 한정자 안에 넣은 버전(\A c \in Counters: [][values[c]' >= values[c]]_values[c])을 TLC가 검사하지 못한다. []와 \A는 교환 가능하므로 한정자를 박스 안으로 끌어들인 버전([][\A c \in Counters: values[c]' >= values[c]]_values)으로 바꾸면 검사된다.

LockCantBeStolen ==
  [][lock # NULL => lock' = NULL]_lock
LockNullBeforeAcquired ==
  [][lock' # NULL => lock = NULL]_lock

CounterOnlyIncreases ==
  [][
    \A c \in Counters:
      values[c]' >= values[c]
    ]_values

함정 액션 속성은 불변식이 아니라 PROPERTY로 넣는다. []만 붙인 액션은 스터터 스텝 때문에 자명하게 거짓이 되므로 [A]_v가 필수다. 한정자 안의 액션 속성은 헷갈리는 에러를 내니 []와 \A를 교환해 최상위 박스 액션 공식으로 만든다.

완역 읽기 → 액션 속성

TLA+ TLA+

PlusCal이 생성하는 TLA+를 거꾸로 읽으며 순수 TLA+의 구조(Init/Next/Spec, 액션, UNCHANGED, EXCEPT, 동시성, 공정성)를 익히고, 순수 TLA+가 PlusCal보다 나은 지점을 정리한다.

• PlusCal은 발판: 먼저 배우면 논리·모델 체킹에 집중하고 시간 논리를 뒤로 미룰 수 있다. 생성된 코드는 유효한 TLA+이므로 그것을 읽어 TLA+를 배운다.
• 스펙의 뼈대: VARIABLES 선언 + 연산자 Init, Next, Spec. Spec은 늘 "실행할 시간 속성"으로 넣던 것이자 TLA+ 명세의 핵심이다.
• 할당이 아니라 비교: PlusCal hr := 1은 TLA+ hr' = 1이다. Next는 불리언 연산자로, 다음 상태의 값을 정확히 기술하면 참이다. x = 5는 이번 상태, x' = 5는 다음 상태에 대한 비교다.
• 액션(action): 프라임 변수를 포함한 불리언 연산자 — Temporal Logic of Actions의 그 액션이다("plus"는 ZF 집합론 추가).
• Spec == Init /\ [][Next]_vars: 시간 연산자 밖의 것은 초기 상태에서 검사하므로, 초기 상태에서 Init이 참이고 모든 스텝에서 Next \/ UNCHANGED vars가 참일 때만 참이다. Next는 다음 상태 관계(next-state relation), 곧 스펙의 청사진이다.
• TLA+는 모든 행동 집합을 기술한다: Next == x' >= x도 유효한 스펙이고 1 → 9 → 17 → 17.1 → 84도 유효한 행동이지만, TLC는 이런 스펙을 생성할 수 없다.
• 모든 변수를 기술해야 한다: next 액션이 변수 하나라도 빠뜨리면 "Successor state is not completely specified by the next-state action" 에러. 관용 표기는 UNCHANGED x, 여럿이면 UNCHANGED <<x, y, z>>.
• with·either의 변환: with x = 1 → LET x == 1 IN(그래서 with 안에 레이블을 둘 수 없다), with x \in 1..2 → \E x \in 1..2:, either → \/ 분기 나열.
• EXCEPT: s[1]' = FALSE는 나머지 원소를 정하지 않아 에러다. s' = [s EXCEPT ![1] = FALSE]로 쓴다(! = 셀렉터). 여러 키 동시 갱신, 원래 값 @, 중첩 ![1].x가 되며 PlusCal에서도 counter[i] := @ + 1;이 가능하다.
• 동시성 모델링: 레이블마다 액션 하나. 액션은 pc[self]가 그 레이블일 때만 활성화(enabled)되고 pc를 다음 레이블로 바꿔 순차성을 흉내 낸다. 동시성은 "그저" \E self \in Threads: thread(self)이고, 종료 후를 위한 Terminating이 붙는다. await lock = NULL은 /\ lock = NULL이 된다. 직접 쓸 때는 Trans(state, from, to) 같은 헬퍼 액션으로 깔끔하게 한다.
• ENABLED A와 <<A>>_v: 이번 스텝에 A가 참일 수 있음 / A가 참이고 v가 바뀜([A]_v는 A가 참이거나 v가 안 바뀜).
• 공정성의 정의: 약한 공정성 WF_v(A)는 ENABLED가 "언젠가부터 항상" 참이면, 강한 공정성 SF_v(A)는 "항상 언젠가는" 참이면 A가 언젠가 일어난다는 뜻이다. 공정성은 Spec에 덧붙는 추가 제약으로 무한 스터터 등을 배제한다. \A self \in Threads : SF_vars(thread(self))는 모든 스레드가, \E면 최소 한 스레드만 공정하다. PlusCal은 레이블에만, TLA+는 레이블 안 하위 액션에도 공정성을 걸 수 있다.
• 예제: hourclock(13 states / 12 distinct)에서 <<12, 1>>은 Next를 만족하고 <<12, 13>>은 아니다. status 예제는 SF_status(Succeed) + WF_status(Retry)를 Spec == Init /\ [][Next]_status /\ Fairness에 붙여, 몇 번 실패하든 결국 <>(status = "done")임을 보인다.
• 왜 TLA+인가: 학습 곡선은 가파르지만 천장이 높다 — 헬퍼 액션, 섬세한 공정성, 리팩터링한 스펙의 동일 행동 검증, 중단 가능한 알고리즘(PlusCal은 either … or goto Start 중복 필요), 같은 값의 프로세스 여럿, 정제 속성. PlusCal만 써도 괜찮지만 그 한계와 부딪히는 시점은 알아 둔다.

Next == IF hr = 12
           THEN /\ hr' = 1
           ELSE /\ hr' = hr + 1

Spec == Init /\ [][Next]_vars

WF_v(A) == <>[](ENABLED <<A>>_v) => []<><<A>>_v
SF_v(A) == []<>(ENABLED <<A>>_v) => []<><<A>>_v

함정 next 액션은 모든 변수를 기술해야 하므로 안 바뀌는 변수는 UNCHANGED로 적는다. 함수 원소만 프라임으로 갱신하면 나머지 원소가 무엇이든 되어 에러가 나니 EXCEPT를 쓴다. with 안에 레이블을 둘 수 없는 이유는 LET 변환 때문이다.

완역 읽기 → TLA+

모듈 Modules

모듈을 가져오는 두 방식을 다룬다. EXTENDS는 모든 것을 파일 네임스페이스에 통째로 붓고, INSTANCE는 여기에 네임스페이스, 상수 대입(WITH), 부분 매개변수화를 더한다.

• 마지막에 다루는 이유: 스펙은 대부분 300줄 남짓 이하라 파일 하나로 충분하다. 그래도 LinkedLists 같은 추상 라이브러리를 만들거나 불변식을 별도 파일에 두고 싶을 때 쓴다.
• 파일 위치: 공유 모듈은 스펙과 같은 폴더에 둔다. 툴박스 설정(TLA+ Preferences > TLA+ Library Path Functions)으로 공유 디렉터리를 지정하면 모든 스펙에서 쓸 수 있다.
• EXTENDS: 지금까지 써 온 방식. 모든 것이 같은 네임스페이스에 들어가며(예: Append), 전부 한 줄에 적어야 한다. LOCAL을 붙인 연산자(LOCAL Op == "definition")는 임포트되지 않는다.
• INSTANCE 기본형: INSTANCE Sequences는 EXTENDS처럼 붓지만 여러 줄로 나눌 수 있다. LOCAL INSTANCE는 임포트한 연산자가 다른 스펙으로 전이적으로 딸려 가지 않게 한다(Sequences.tla가 Naturals를 이렇게 임포트한다).
• 네임스페이스: Foo == INSTANCE Sequences로 이름을 붙이고 Foo!Append(seq, 1)처럼 I!operator로 조회한다. LET 안에서도 임포트할 수 있고, 다른 이름으로 여러 번 임포트할 수도 있다(상수가 있는 모듈에서 의미가 생긴다).
• 매개변수화된 모듈: 상수를 가진 모듈은 WITH X <- 0, Y <- 0으로 상수를 대입해 임포트한다. 모든 연산자가 사실상 다시 쓰여 Origin!Add(x, y) == <<0 + x, 0 + y>>가 된다.
• 같은 이름 상수의 기본 대입: 임포트하는 쪽에 같은 이름의 상수(예: DEBUG)가 있으면 기본으로 그것이 들어가므로 WITH DEBUG <- DEBUG는 생략해도 같다. WITH에 값을 주면 오버라이드된다.
• 부분 매개변수화: XAxis(X) == INSTANCE Point WITH Y <- 0처럼 일부만 대입하고 나머지는 인스턴스 매개변수로 남긴다. XAxis(2)!Add(x, y) == <<2 + x, 0 + y>>.

---- MODULE Point ----
LOCAL INSTANCE Integers
CONSTANTS X, Y
ASSUME X \in Int /\ Y \in Int

Repr == <<X, Y>>
Add(x, y) == <<X + x, Y + y>>
====

Origin == INSTANCE Point WITH X <- 0, Y <- 0
XAxis(X) == INSTANCE Point WITH Y <- 0

함정 EXTENDS는 한 줄에 다 적어야 하므로 줄을 나누려면 INSTANCE를 쓴다. 네임스페이스 없이 모든 것을 부으면 모두가 괴로우니 Foo == INSTANCE …로 이름을 붙여라. 같은 이름의 상수는 자동으로 대입되므로 의도와 다르면 WITH로 오버라이드한다.

완역 읽기 → 모듈

다음 단계 Next Steps

핵심 과정의 마무리 페이지다. TLA+의 핵심 개념과 설계 버그를 찾는 법을 익힌 독자에게, TLA+를 "잘" 쓰게 되는 길 — 주제별 심화, 예제, 기타 자료, 무엇보다 직접 스펙을 쓰는 연습 — 을 안내한다.

• 아직 다루지 않은 것: 모델 최적화, 디자인 패턴, 개발 프로세스의 일부로 TLA+를 쓰는 법, 커맨드 라인 실행. 지금까지의 예제는 전부 장난감 문제였고, 실제 세계의 스펙이 어떤 모습인지라는 질문이 남는다.
• 주제별 심화: 설계 시 고려 사항, 일반 팁, 도구를 더 잘 쓰는 법 등 고급 활용 전반(주제별 심화).
• 예제: 공부용 연산자와 스펙 모음(예제).
• 사이트 현황: 원문 작성 시점에 두 섹션은 아직 "희망 사항"에 가까웠다 — 주제는 약 15개 계획 중 6개만 작성됐고, 예제 페이지는 대부분 인터넷의 다른 예제로 가는 링크다. 업데이트는 새 소식에서 확인한다.
• 기타 자료: 웹의 자료 링크는 기타 자료에 모여 있다.
• 연습이 가장 중요: 저자는 한동안 다뤄 봐서 잘 아는 시스템부터 모델링하라고 강하게 권한다. 아키텍처나 기능 하나에 대한 고수준 스펙을 쓰고, 포괄성은 걱정하지 말고 해낼 수 있다고 생각하는 것에 집중한다.
• 초보 단계의 에러 해석: 이 단계의 스펙 에러는 실제 버그의 징후라기보다 경험 부족 탓일 가능성이 더 크다. 잘 아는 시스템이면 놓친 시스템 가정이나 TLA+ 실수를 알아보기 쉬우니 이를 피드백 루프로 삼는다. 실제 버그일 가능성도 생각보다 자주 있으니 배제하지는 말되, 첫 가정으로 넘겨짚지도 않는다.
• 다른 출발점도 괜찮다: 백지에서 시작하는 새 시스템(greenfield)의 스펙이나 고장 난 것으로 알려진 시스템의 디버깅으로 곧장 뛰어들어도 된다. 저자는 결국 가장 의욕이 나는 방법이 최선이라고 본다.

함정 처음부터 포괄적인 스펙을 쓰려 하지 말 것. 초기 스펙 에러를 곧바로 실제 버그로 단정하지도, 그 가능성을 배제하지도 말 것 — 잘 아는 시스템으로 연습해야 에러 원인(놓친 가정 vs TLA+ 실수)을 가려내기 쉽다.

완역 읽기 → 다음 단계

주제별 심화 소개 Topics

TLA+를 더 효과적으로 쓰기 위한 기법과 에세이를 모은 파트의 목차다. 저자는 TLA+를 처음 접한다면 이 파트보다 핵심 과정이 더 유용할 수 있다고 안내한다.

• 집필 현황: 주제 대부분이 아직 작성되지 않았다. 계획 중인 주제는 새 소식 › 로드맵에 있다.
• 일반: 일반 팁 · 툴박스 사용하기 · 툴박스 너머 · 보조 변수 · 정제 · 경계 없는 모델 다루기 · 모델 체킹 최적화.
• "…를 모델링하는 법"(How to Model…): 메시지 큐 · 유한 상태 기계.

완역 읽기 → 주제별 심화

일반 팁 General Tips

더 나은 스펙을 위한 자잘한 요령 모음이다. TLA+·PlusCal 공통, PlusCal 전용, TLA+ 전용 세 묶음으로 나뉜다.

• ASSUME: 모든 CONSTANT에 기대 값을 알리는 ASSUME을 붙인다. 모델 값이면 어떤 집합의 원소가 아니라고 말하면 대개 충분하고, 데이터 타입은 그 타입의 빈 값과 비교한다. 타입이 다르면 TLC가 ASSUME에서 크래시하는데, 제대로 실패하는 것과 같은 역할이다.
• 태그드 유니언: TLC는 문자열과 정수가 섞인 집합을 다루지 못하므로 type·val 필드를 가진 구조체로 감싼다.
• 구조체의 함수 분해: state \in [Worker -> WorkerState]는 변수가 한 스텝에 한 번만 갱신되므로 필드를 따로 바꿀 수 없다. 필드마다 변수(worker_queue, worker_online)를 두면 따로 갱신된다. 대가는 지저분한 UNCHANGED와 구현 모습과의 거리. 저자는 구조체를 메시지 본문 같은 불변 값에 주로 쓴다.
• 안전성 모델과 라이브니스 모델 분리: 라이브니스 검사는 훨씬 느리고 대칭 집합을 쓸 수 없으므로 더 작은 상수의 전용 모델을 둔다.
• 모듈의 여분 공간: ---- MODULE name ---- 위와 ==== 아래는 무시된다. 아래는 스크래치, 위는 문제 도메인·요구 사항 메모 자리다.
• THEOREM: 속성을 "표면상" 선언한다. 모델 체커에는 영향이 없는 문서화 용도다.
• TypeInvariant와 ModelInvariant: 타입 불변식은 모든 변수의 가능한 값만 검사하고, 정당한 값(두 집합이 서로소 등)은 별도 정확성 불변식으로 뺀다. 모델 불변식은 상태 공간이 유한한지 확인한다(스펙이 만족하게 쓰거나 상태 제약(state constraint)으로 추가).
• PlusCal 매크로: 문을 재사용하는 주된 수단.
• while 루프는 해롭다: 한 바퀴마다 새 상태가 생겨 동시성과 상태 공간 폭발을 키운다. 계산은 seq := [i \in 1..Len(seq) |-> seq[i] * 2];처럼 한 스텝에 재할당한다. 상태 스위핑은 함수 장에서 다룬다.
• UNCHANGED 관리: 변수를 튜플로 묶고 묶음 단위로 UNCHANGED를 쓴다.
• 헬퍼 액션: 다음 상태 관계를 여러 액션으로 나눠도 된다. pc 갱신용 Trans(agent, a, b)가 대표 예.
• @: EXCEPT 안에서 이전 값. f' = [f EXCEPT ![1][2].a = @ + 1]
• 액션 매개변수화: \E를 Next(맨 아래 층)로 옮기고 액션에는 값을 넘긴다. 같은 w를 Add(w)·Remove(w)·Log(w)에서 재사용할 수 있다.
• 액션 속성으로 리팩터링: 옛 액션과 새 액션이 같은지 액션 속성(RefactorProp)으로 검증한다. 확장이라면 = 대신 =>.

CONSTANT Threads, NULL
ASSUME Threads # {}
ASSUME NULL \notin Threads

worker_state == <<worker_queue, worker_online>>
topic_state == <<topic_subscribers, topic_id>>

SomeAction ==
  /\ x' = x + 1
  /\ UNCHANGED <<worker_state, topic_state>>

함정 변수는 한 스텝에 한 번만 갱신되므로 구조체의 함수로 된 변수는 필드를 따로 바꿀 수 없다. THEOREM은 모델 체커가 검사하지 않는다. while 루프로 계산하면 불필요한 상태가 생긴다.

완역 읽기 → 일반 팁

툴박스 사용하기 Using the Toolbox

TLA+ 툴박스(Toolbox)의 파워 유저 기능 참조다. 에러 트레이스 패널, 트레이스 탐색기, 모델 설정, 편집기 기능을 쓸 수 있게 된다.

• 에러 트레이스 읽기: 드롭다운 하나 = 스텝 하나, 빨간 값 = 그 스텝에서 바뀐 변수. 함수 변수는 펼쳐서 바뀐 키를 본다.
• 패널 버튼 4개: 트레이스를 TLA+ 구조체로 복사(JSON은 개발 중) · 변수 필터(보조 변수, 바뀌지 않은 변수 숨김) · 모든 스텝 펼치기/접기 · 액션 줄 클릭 시 스펙의 해당 액션으로 이동하는 토글.
• 클릭 조작: 변수 Alt-클릭 = 숨김, 액션 더블클릭 = 스펙 코드로, Ctrl-더블클릭 = PlusCal 레이블로, 우클릭 = 그 상태를 초기 상태로 같은 모델 재실행.
• 트레이스 탐색기(Trace Explorer): 추가한 식을 트레이스의 모든 상태에서 평가한다(Explore, 복귀는 Restore). 탐색기 연산자 재사용, 프라임 값(prod' = x' * y'), 액션 전체 테스트(다음 상태를 정확히 기술하면 참)가 된다. 명령줄에서는 ALIAS가 비슷한 이점을 준다.
• 상태 제약: 만족하지 않는 상태를 TLC가 버린다. 단 버리기 전에 불변식은 검사하며, 막는 것은 그 상태로부터의 탐색뿐이다. 켜져 있으면 라이브니스를 검사할 수 없다.
• 액션 제약(action constraint): 액션판 상태 제약. x' > x면 x가 증가하는 전이만 탐색한다.
• 정의 오버라이드: 연산자를 교체한다. Int <- 1..10으로 "아무 정수"를 유한 집합으로 제한.
• 워커 스레드: 기본값 = 코어 수. 1개면 실행 간 결정적이라 print 디버깅에 좋다.
• 메모리 비율: 초과하면 상태를 디스크에 써서 크게 느려진다. 시작 전에 전부 사전 할당하므로 작은 모델에선 할당이 실행보다 길 수 있다.
• 뷰(VIEW): "흑마법". 기본은 모든 변수(<<x, y>>)로 상태를 구별하지만 VIEW x면 x만 본다. 잘 쓰면 최적화, 잘못 쓰면 스펙이 완전히 망가진다.
• 깊이 우선: 위반이 행동 깊은 곳에 있을 때. 최대 깊이를 정해 경계 없는 모델 일부도 검사한다.
• 시뮬레이션 모드: 최대 길이까지 무작위 트레이스 생성, 라이브니스 미검사, 스스로 끝나지 않는다.
• 프로파일링: Action Enablement(한 번도 활성화되지 않는 액션 = 스펙 버그 탐지) / On(연산자별 호출 빈도·비용 — 최적화용).
• 상태 그래프 시각화(graphviz 필요, 작은 상태 공간용) · TLC 커맨드 라인 매개변수 전달 · 편집기 ctrl+space 자동 완성, F3 정의로 이동, "translate pluscal automatically".

Init == x = 0
Next == x' = x + 1
Inv == x < 10
Spec == Init /\ [][Next]_x

함정 위 스펙은 INVARIANT Inv로 보통 실패한다. 상태 제약 x < 5를 두면 상태 6개로 통과하지만 x < 10이면 불변식이 먼저 검사되어 여전히 실패한다 — 상태 제약은 불변식 검사를 막지 못한다. 자동 변환 옵션은 PlusCal이 아닌 스펙에서 에러를 낸다.

완역 읽기 → 툴박스 사용하기

툴박스 너머 Beyond the Toolbox

툴박스 없이 tla2tools.jar 하나로 명령줄에서 PlusCal 변환과 TLC 모델 체킹을 돌린다. 핵심은 .cfg 설정 파일 형식과 몇 가지 TLC 플래그다(툴박스 대안으로 VSCode 확장도 언급된다).

• tla2tools.jar: GitHub 릴리스나 툴박스 설치 디렉터리에 있다. 하위 도구는 TLC · PlusCal 변환기 · Tla2Tex(LaTeX PDF) · SANY(파서)이며, 이 장은 앞의 둘만 다룬다.
• 변환: pcal.trans는 제자리 변환 + 백업 file.old + file.cfg 생성(있으면 덮어씀). -nocfg로 cfg 생성을 막지만 file.old는 못 막는다.
• 실행: -config를 생략하면 specfile.cfg를 찾는다.
• 설정 파일: 툴박스가 감춰 주던 전용 DSL. SPECIFICATION은 필수이며 관례상 Spec이지만 설정마다 다른 변형을 지정할 수 있다. INVARIANT/PROPERTY는 쉼표로 나열하되 이름 붙은 연산자만 된다(툴박스는 식을 MC.tla로 우회한다).
• CONSTANT: 단순 값이나 그 집합만(함수·식 불가). 모델 값은 name = name, 모델 값 집합 {c1, c2, c3}의 원소는 문자열이 아니라 식별자. 음수 불가(cfg는 임포트를 못 쓴다).
• CONSTRAINT / ACTION-CONSTRAINT / VIEW: 툴박스와 동일. CHECK_DEADLOCK FALSE로 데드락 검사를 끈다.
• ALIAS: 명령줄판 트레이스 탐색기. 트레이스가 별칭 구조체의 필드(예: nextx |-> x')를 보여 주지만 기본 에러 트레이스 출력을 대체하므로 빠진 변수는 사라진다.
• 플래그: -help(-h 아님) · -continue(모든 위반 출력) · -dump file(도달 상태 전부) · -dump dot file(graphviz, 확장자는 직접, dot,colorize·dot,actionlabels) · -metadir dir · -workers num/auto · -noGenerateSpecTE · -fpmem num(기본 0.25).

java -cp tla2tools.jar pcal.trans file.tla
java -jar tla2tools.jar -config configfile.cfg specfile.tla

SPECIFICATION Spec

INVARIANT Inv1, Inv2
PROPERTY Prop1

CONSTANT
  Const1 = {"a", "b", "c"}
  Const2 = Const2
  Const3 = {c1, c2, c3}

함정 -workers를 안 주면 CLI는 워커 1개로 돈다 — auto를 쓴다. pcal.trans는 기존 cfg를 덮어쓴다. -continue를 툴박스에서 플래그로 넘기면 툴박스가 버그로 여긴다.

완역 읽기 → 툴박스 너머

보조 변수 Auxiliary Variables

속성만으로 표현할 수 없는 것(예: 속성을 "잊기")을, 시스템의 일부가 아닌 추가 변수로 스펙을 보강해 표현·검사한다. 히스토리·에러·경계·예언 변수 4종을 다룬다.

• 속성의 한계: "Q가 참이 될 때까지 P, 그 뒤로는 상관없음"을 ~P => Q로 쓰면 이미 잊었어야 할 불변식이 실패한다.
• 보조 변수(auxiliary variable): Q_was_true를 추가해 P => Q \/ Q_was_true로 쓴다. 우아하진 않지만 효과가 있다. 다른 분야에선 ghost/helper 변수라 부른다.
• 히스토리 변수: 이미 일어난 일. 한 번 설정된 뒤 바뀌지 않음은 액션 속성으로 확인한다. 시스템에서 사라진 과거 정보(요청 시점 DB 값 aux_client_request_value)도 보존한다.
• 에러 변수: 의미론을 바꾸지 않고 에러 트레이스를 풍부하게 한다. either 분기마다 aux_branch := "Path1"을 대입하거나 이력 로그 aux_log' = Append(aux_log, w)를 남긴다.
• 경계 변수: 상태 공간을 유한하게 한다(reader_writer의 최대 N개 메시지). 저자는 작은 오류 주입에 쓴다 — aux_drops_left로 메시지 유실 횟수 제한.
• 예언 변수(prophecy variable): 미래에 일어날 일을 미리 정한다 = 비결정성을 앞으로 당긴다. 드물고 주로 정제용. 계산기 예: 반복마다 10갈래로 분기하던 with x \in Digits 대신 aux_proph_digits \in [1..NumInputs -> Digits]로 시작하면 초기 상태는 많아지고 각 초기 상태의 행동은 1개가 된다.
• "기계" 변수 vs 보조 변수: 시스템의 일부인 변수와 아닌 변수를 명확히 구분한다.

Prop == P => Q \/ Q_was_true

Next ==
  /\ \* regular spec
  /\ IF Q' THEN Q_was_true' ELSE UNCHANGED Q_was_true

either
  queue := Append(queue, msg);
or
  await aux_drops_left > 0;
  aux_drops_left := aux_drops_left - 1;
end either;

함정 트레이스를 읽기 쉽게 하려고 레이블을 남발하면 동시성이 추가되어 잘해야 상태 공간 폭발, 최악엔 의미론이 바뀐다 — 보조 변수로 대체한다. 경험칙: 스펙의 행동이 히스토리 변수에 의존하면 안 되며, 의존한다면 진짜 변수로 격상한다. 상태에서 값을 계산해 보기만 하려면 ALIAS면 된다.

완역 읽기 → 보조 변수

정제 Refinement

아직 작성되지 않은 자리표시 페이지다. 저자는 그동안 자기 블로그 글의 정제(refinement) 입문을 보라고 안내한다.

• 정제: 이 페이지에는 제목만 있고 정의·설명·문법이 없다.
• 현황: 저자에 따르면 다룰 내용은 블로그 글에 모두 있고, 사이트 스타일에 맞게 고치는 일만 남았다.
• 책 안의 언급: 예언 변수의 주 용도(보조 변수), 자세한 시스템을 고수준 스펙과 정제로 다루는 길(모델 체킹 최적화)로 등장한다.

완역 읽기 → 정제

경계 없는 모델 다루기 Handling Unbound Models

서로 다른 상태가 무한해 모델 체킹이 끝나지 않는 모델을 알아채고(모델 불변식), 경계를 두는 법(스펙 수정·상태 제약·TLCGet("level"))을 익힌다.

• 경계 없는 모델(unbound model): 모델 체커는 모든 서로 다른 상태를 찾으므로 그 수가 무한하면 끝나지 않는다. 발생원은 ① 정수를 계속 증가 ② 시퀀스에 계속 추가. 최상위 값만이 아니라 [a: Int, b: BOOL]의 a처럼 내부 값도 해당한다.
• 탐지 신호: 예상보다 상태가 훨씬 많거나 지름(diameter)이 예상보다 빨리 는다. 경계 있는 모델은 대부분 지름이 천천히 는다.
• 모델 불변식(model invariant): 모든 변수를 유한 집합으로 제한하는 타입 불변식 같은 것 — 가장 쉬운 탐지법. ModelInvariant => TypeInvariant이고, 경계 없는 모델은 반드시 이것을 깬다(경계 있는 모델도 괜히 깰 수는 있다).
• 경계 두기: 경계 없는 모델은 대부분 스펙 에러다. 어딘가 검사를 빠뜨려 모델 체커가 파고든 것이므로 버그·스펙 수정으로 대개 경계가 돌아온다.
• 상태 제약 ModelConstraint: 모델 불변식과 같은 식이지만 위반 상태를 에러 대신 거부한다. 상태 공간은 무한해도 유한한 부분만 탐색한다.
• TLCGet: TLC 모듈의 연산자로 생성 상태 수·현재 트레이스 길이 같은 런타임 통계를 준다. TLCGet("level")로 스텝 수를 제한하는 것이 저자가 가장 좋아하는 방법이다.

(*--algorithm seriously_dont_run_this
variable x = 0
begin
  while TRUE do
    x := x + 1;
  end while;
end algorithm; *)

CONSTANT MaxX

TypeInvariant == x \in Int
ModelInvariant == x \in 0..MaxX

ModelConstraint == TLCGet("level") < 9

함정 시간 속성도 검사한다면 상태 제약을 쓰지 마라 — 행동을 잘라 내므로 라이브니스를 평가할 행동 전체가 없다. 변수가 많으면 변수별 경계를 예측하기 어려우므로, 처음에는 변수를 그대로 두고 TLCGet("level")로 스텝 수만 제한하는 편이 훨씬 쉽다.

완역 읽기 → 경계 없는 모델 다루기

모델 체킹 최적화 Optimizing Model Checking

TLC 실행 시간은 주로 생성해야 할 상태 수가 좌우한다. 상수·대칭·동시성·비결정성·세부 수준을 줄여 상태 공간부터 줄이고, 그다음 상태당 비용을 손본다. 저자는 "과학이라기보다 예술"인 기본 휴리스틱 모음이라고 말한다.

• 시작 전 점검: 모델에 경계가 있는가 / 런타임 매개변수(툴박스 = RAM 25% + 코어당 워커, CLI = RAM 25% + 워커 1개) / 하드웨어(라이브니스 검사는 단일 스레드라 단일 코어 성능도 중요).
• 두 요인: 상태당 생성 시간(개선 5~10%)보다 상태 수(개선 흔히 10배)가 지배적이다.
• 상태 공간 추정: SUBSET S = 2^|S|, S \X T·[s: S, t: T] = |S|·|T|, [S -> T] = |T|^|S|. 곱으로 쌓인다([A \X B -> SUBSET C]는 재앙의 근원). 동시성은 인터리빙으로 폭증한다(배정 3배 → 상태 9배).
• 더 작은 상수: 첫 수단. 대부분의 버그는 작은 상태 공간에서도 나타난다. 작은 설정으로 반복하고 통과할 때만 큰 모델을 돌린다.
• 대칭 집합: n원소 모델 값 집합이면 대략 n!분의 1. CLI에서는 Symmetry 정의 + 설정에 SYMMETRY Symmetry.
• 안전성/라이브니스 모델 분리 · 로더 프로세스 제거(초기값만 세팅하는 프로세스 대신 가능한 최종 값 중 하나로 시작).
• 레이블 합치기: 원자성의 입도(grain of atomicity)를 의식적으로 고른다 — 너무 굵으면 진짜 에러를 가리고, 너무 잘면 오래 걸린다.
• 의도하지 않은 비결정성 줄이기: 순서가 상관없으면 CHOOSE로 한 순서를 고정한다. 시퀀스 대신 백: 중복만 필요하면 EmptyBag 등.
• 뷰: 상태 동일성에 쓸 튜플을 지정해 보조 변수를 무시한다(툴박스 View 옵션, CLI는 VIEW view).
• 세부 줄이기: 가장 중요한 휴리스틱 — "모델이 자세할수록 상태가 많아진다". 0..100 대신 0..3, 가능하면 BOOLEAN. 자세한 시스템은 고수준 스펙 + 정제로.
• 프로파일러: 호출 횟수·비용, 액션별 새/고유 상태 수(변환된 TLA+ 기준). 걸러내지 말고 구성하라: 큰 집합을 필터링하지 말고 작은 집합을 직접 생성한다.
• 그 밖의 팁: 자기 자신을 두 번 부르는 이중 재귀 함수 정의는 피한다. 느린 연산자는 Java로 오버라이드할 수 있다 — TLC도 SortSeq를 Java 삽입 정렬로 바꿔 쓰고, CommunityModules에 예제가 있다. 최적화한 뒤에는 리팩터 속성으로 상태 공간이 바뀌지 않았는지 확인한다. 작은 모델에 RAM을 과하게 주면 JVM 사전 할당 때문에 오히려 느려질 수 있다 — 보통은 큰 문제가 아니지만, 500GB 넘는 대형 머신에서는 20초짜리 스펙이 몇 분 걸린 경우도 있었다. 상태 공간 일부만 보고 싶으면 FastInit/FastNext/FastSpec으로 좁힌 스펙을 따로 만든다. 대안 모델 체커 Apalache는 언어 전체를 지원하지 않고 타입 시스템을 쓰며, 일부 스펙에서는 더 빠르다고 한다.
• 러닝 예제 수치(MaxNum = 7, 워커 3): 기본 28,351,303 상태 / 8,241,961 고유 → 깊이 제약 872,224 · 대칭 4,728,962 · 로더 제거 10,794,312 · 레이블 합치기 2,353,282 · CHOOSE 고정 2,052,493.

Constraint == TLCGet("level") < 11
Symmetry == Permutations(Workers)

    await to_process[self] # {};
    with x = CHOOSE x \in to_process[self]: TRUE do

함정 액션 합치기는 동시성 버그를 숨길 수 있다. CHOOSE x \in set: TRUE는 드문 허용 사례다(CHOOSE는 결정적이라 많은 사람이 예상하지 못한다). 뷰는 유효 상태도 쉽게 지운다 — 지역 변수 local을 빠뜨린 뷰는 기본보다 적은 1,018,176 상태만 찾았다.

완역 읽기 → 모델 체킹 최적화

메시지 큐 모델링 Modelling Message Queues

분산 시스템에서 가장 흔한 패턴인 메시지 큐를 메시지 구조체의 시퀀스로 표현하는 레시피다. 가변/불변 읽기, 메시지 타입 설계, 리더별·라이터별 다중 큐를 다룬다.

• 전제: Reader·Writer 프로세스 집합이 완벽한 FIFO 큐 하나를 공유한다. 쓰기는 queue := Append(queue, msg)(TLA+는 queue' = ...).
• 가변 큐(쉬운 방법): 파괴적으로 갱신한다. 현재 Head(queue) · 삭제 queue' = Tail(queue) · 크기 Len(queue) · 빔 queue = <<>>. 단순하지만 "같은 메시지는 두 번 들어가지 않는다" 같은 히스토리 의존 속성은 히스토리 큐 없이는 쓸 수 없다.
• 불변 큐(어려운 방법): 추가만 하고 인덱스 i로 읽는다. queue[i] · i' = i + 1 · Len(queue) - i + 1 · Len(queue) = i + 1. 히스토리 전체가 남는다. 저자는 추가 계획이 없는 큐(여러 시작 상태로 초기화)에 쓴다.
• 메시지 타입: 구조체의 집합. id 필드로 내용이 같은 메시지를 구별한다(MaxId 상수 필수). 종류가 여럿이면 msg 필드 + data 구조체로 나누고 MessageType을 하위 타입의 합집합으로 만든다.
• 여러 리더 큐: queues \in [Reader -> QueueType], 각 리더는 queues[self]에서 읽는다. 전원에 쓰기 = queues를 함수로 재정의, 일부에만 = SUBSET + @@.
• 최대 한 번 전달(at-most-once delivery): 유효한 수신자의 부분집합에만 전달하는 것으로 모델링한다.
• 여러 라이터 큐: 비결정적으로 읽는다. PlusCal은 with w \in Writer, TLA+는 \E w \in Writer + [queue EXCEPT ![w] = Tail(@)].

\* Seq comes from EXTENDS Sequences
QueueType == Seq(MessageType)
MessageType == [id: Nat, from: Writer, data: DataType]

\E readers \in SUBSET Reader:
  queues' = [r \in readers |-> Append(queues[r], msg)] @@ queues

함정 불변 큐는 경계 없는 모델이 되기 쉽다. 읽지 않은 메시지 수의 최댓값을 제한해도 오래된 메시지를 계속 읽는 한 큐는 끝없이 자란다. id 필드를 쓰면 MaxId 상수를 반드시 둔다.

완역 읽기 → 메시지 큐 모델링

유한 상태 기계 Finite State Machines

저자는 정형 기법을 큰 규모로 키울 방법으로 알려진 것이 상태 기계뿐이라고 본다. 램프 예제로 평범한 상태 기계를 PlusCal과 TLA+로 쓰고, 재귀 In 연산자로 계층적 상태 기계를 모델링한다.

• 비결정적 전이: 한 상태에서 갈 수 있는 전이가 여럿일 수 있다. 램프(BothOff·WallOff·LampOff·On, 전이 8개)는 스위치가 한 번에 하나씩만 바뀌므로 BothOff와 On 사이에 전이가 없다.
• PlusCal 패턴: either/or 분기마다 await state = X; state := Y;. 조건이 거짓인 분기는 막히고 나머지는 선택 가능해 비결정성이 유지된다. 레이블 Action + goto Action;으로 반복하고, transition(from, set_to) 매크로로 줄인다.
• TLA+ 패턴(저자 선호): Trans(a, b)에 state = a와 state' = b를 두고 Next는 Trans들의 \/다. 두 판 모두 상태 9개 / 고유 상태 4개.
• 계층적 상태 기계(HSM, Harel 스테이트차트): 상태 안에 상태를 두며, 자식은 부모의 모든 전이를 할 수 있다. 이 장의 제약: 전이는 리프 상태에서 끝나고, 부모는 하나이며, 순환이 없다.
• 재귀 In(s, p): Trans의 조건을 In(state, from)으로 바꾸면 조상에서 시작하는 전이가 모든 자손에 적용된다. 재귀 연산자 앞에는 RECURSIVE 선언.
• 계층 표현 2가지: 하향식(상태 → 자식 집합, @@로 나머지를 {})은 정의역이 보장되지만 같은 자식을 두 번 줄 수 있고, 상향식(상태 → 부모)은 부모가 둘일 수 없지만 In 검사가 번거롭다.
• ASSUME으로 구조 검사: 부모가 둘인 상태가 없음, InTD와 InBU가 모든 쌍에서 동치임을 확인. AlwaysInLeaf = TopDown[state] = {}.
• 웹 앱 UI 예: LogIn 아래 Main·Settings·Reports, Reports 아래 Report1·Report2. Trans("LogIn", "LogOut")은 로그인 아래 모든 상태에서 적용된다. 상태 16개 / 고유 상태 5개.

Trans(a, b) ==
  /\ state = a
  /\ state' = b

Spec == Init /\ [][Next]_state

RECURSIVE InTD(_, _)
InTD(s, p) ==
  \/ s = p
  \/ \E c \in TopDown[p]:
    InTD(s, c)

함정 PlusCal은 전이마다 분기를 하나씩 적어야 해서 길어진다 — 매크로를 쓰거나 TLA+로 옮긴다. 하향식에서 같은 자식이 두 번 들어가는 실수는 ASSUME으로 막고, 두 표현을 모두 구현해 ASSUME으로 동치를 교차 검증한다.

완역 읽기 → 유한 상태 기계

예제 Examples

예제 파트의 입구다. 사이트 안 예제는 아직 두 개(연산자 예제 「분할」, PlusCal 스펙 예제 「고루틴」)뿐이라, 웹에 있는 외부 TLA+ 예제 11개와 참고 자료 1개를 함께 소개한다.

• 사이트 안 예제의 두 갈래: 연산자(Operators) → 「분할」, PlusCal 스펙(PlusCal Specs) → 「고루틴」.
• 외부 예제 11개: TLA+ 예제 저장소(공식, 대부분 추상적인 알고리즘·프로토콜) · 메시지 전달 버그 모델링 · 토끼와 거북이(연결 리스트 사이클 찾기를 정형적으로 모델링) · 메시지 큐(읽는 쪽이 토픽을 구독하는 pubsub) · 스레드 유한 큐(가득 찬 큐에 쓰려는 스레드를 재우는 유한 큐에서 데드락 찾기) · 적대적 모델링(스펙을 "기계"와 "세계"로 나누고 세계가 기계의 적대자 역할) · Xen VChan · 배치 업로더(저자가 실무에서 처음 쓴 스펙) · 프로세스 핸들러 · 결제 핸들러(개념 개요 송금 예제의 현실판) · Raft 합의 알고리즘.
• 참고 자료: Introduction to Formal Pragmatic Modeling(정형 실용 모델링 입문) — 대규모 프로덕션급 스펙 3개를 깊이 논의한다.

팁 새 문법은 없는 목차 페이지다. 저자는 사이트 작업을 이어 가며 예제를 늘리겠다고 밝히고, 그동안은 외부 예제를 보라고 안내한다.

완역 읽기 → 예제

분할 Partitions

집합의 모든 분할을 돌려주는 연산자 Partitions(set)를 기존 문법만 조합해 만든다. 핵심 발상: "각 값이 몇 번째 집합에 속하는가"를 나타내는 함수를 "인덱스 → 값 집합" 시퀀스로 뒤집고, 집합으로 바꾼 뒤 공집합을 뺀다.

• 문제: 분할 = Part(각각 SUBSET S의 원소)들의 집합. 서로 다른 두 Part의 교집합은 공집합이고, 전체의 UNION은 S다. Partitions(3)은 분할 5개다. 저자는 숫자 대신 값의 집합을 받도록 일반화한다.
• 시퀀스로 보기: { {a,c}, {b} } 대신 << {a, c}, {b} >>로 상상하면, 같은 정보를 a :> 1 @@ b :> 2 @@ c :> 1로도 쓸 수 있다.
• 함수 집합 = 분할 인코딩: 그 인코딩은 함수 집합 [{a, b, c} -> 1..3]의 원소일 뿐이다. "값 → 인덱스" 맵을 "인덱스 → 값 집합"으로 뒤집는 G(f)를 LET 안에 정의한 것이 PartitionsV1이다.
• 집합 맵 + Range: 시퀀스를 집합으로 되돌리면 <<{1, 2}, {}>>가 {{1, 2}, {}}가 되므로 차집합 \ {{}}로 공집합을 뺀다.
• 비용: <<{1, 2}, {}>>와 <<{}, {1, 2}>>는 같은 분할이라 중복이 많다. [1..n -> 1..n]은 n^n개 — 1..4면 함수 256개 대 분할 15개로 10배 넘는 오버헤드다. 분할 개수는 벨 수(Bell number)를 따른다. 각주: n^n을 테트레이션이라 부르기도 한다.

PartitionsV1(set) ==
  LET F == [set -> 1..Cardinality(set)]
    G(f) == [i \in 1..Cardinality(set) |-> {x \in set: f[x] = i}]
  IN
    {G(f): f \in F}

Range(f) == {f[x] : x \in DOMAIN f}

Partitions(set) ==
    {Range(P) \ {{}}: P \in PartitionsV1(set)}

함정 PartitionsV1({"a", "b"})는 공집합이 끼고 순서만 다른 시퀀스 4개를 내므로 Range와 \ {{}}를 빼먹지 말 것(코드는 EXTENDS Integers, TLC, Sequences, FiniteSets). 중복 생성은 비효율적이지만 저자는 괜찮다고 본다 — 분할은 대개 스펙의 서로 다른 구성으로 쓰이고, 그때 256원소 집합 계산 비용은 상태 공간이 15배 커지는 비용에 묻힌다.

완역 읽기 → 분할

고루틴 Goroutines

Chris Siebenmann이 보고한, 데드락 나는 Go 코드 약 20줄(버퍼 있는 limitCh 토큰 + 버퍼 없는 found 채널)을 PlusCal로 옮겨 TLC 기본 데드락 검사로 버그를 재현하고, 수정안 3개를 각각 검증한다. 설계가 아니라 코드를 직접 검증하는 사례다.

• 속성 없이 데드락만: 정형 명세 = 시스템 기술 + 속성 기술이지만, 데드락만 찾을 때는 속성을 생략해도 된다(TLC가 기본으로 검사). 타입 불변식 같은 온전성 검사는 좋은 습관이지만 필수는 아니다.
• 왜 PlusCal: Go 코드가 매우 순차적이다. 대가로 버퍼 없는 채널에서 "임피던스 불일치"가 생기지만 전체로는 이득. 어려운 부분은 go, defer, 채널의 성질 셋.
• defer: 지연 코드를 프로세스 끝의 별도 레이블로 옮긴다(더 정확히 하려면 프로시저).
• go: PlusCal은 프로세스를 미리 다 정의해야 하므로, 각 프로세스가 initialized[self]를 await하게 두고 메인이 플래그를 TRUE로 세우면 시작한다. go(routine) 매크로로 Go 문법에 맞춘다.
• 버퍼 있는 채널: 내용물은 숫자 하나, 최대 용량은 buffered 변수. 가득 차면 송신이, 비면 수신이 블록 → await + 증감 매크로.
• 버퍼 없는 채널: 송신자와 수신자가 모두 있어야 진행한다. 채널 값 = 수신자를 기다리는 송신자 집합(select 때문에 상태를 송신자 쪽에 둔다). send_unbuffered 프로시저는 두 스텝 — 집합에 자신을 넣고(DeclareSend), 수신자가 빼 줄 때까지 대기(Send). receive_channel 매크로는 버퍼 있는 채널이면 카운터를 줄이고, 아니면 with로 송신자 하나를 비결정적으로 골라 뺀다.
• 결과: 모델 NumRoutines <- 3, NumTokens <- 2에서 TLC가 7상태 데드락 트레이스를 찾는다 — 고루틴 1·2가 found에서 대기, 메인은 고루틴 3에 줄 토큰이 없어 블록되는 순환 대기다. Chris의 수정안 셋(고루틴이 직접 토큰을 가져가기 · found 송신 전에 토큰 반납 · for 루프 전체를 별도 고루틴 process for_loop = -1로)은 모두 모델 체킹을 통과한다.

procedure send_unbuffered(chan) begin
  DeclareSend:
    channels[chan] := channels[chan] \union {self};
  Send:
    await self \notin channels[chan];
    return;
end procedure

함정 with는 집합이 비면 블록하므로 그 앞의 await channels[chan] # {}는 명확성을 위한 중복이다. Get 루프는 range 수신(채널이 닫힐 때까지)을 부정확하게 표현하지만 스펙이 채널 닫기에 의존하지 않아 생략했다. Go 20줄에 스펙 약 75줄이 들었고 절반 이상은 재사용 가능한 채널 로직이다 — 저자는 프로덕션 전에 데드락을 잡으면 순이익이라고 본다.

완역 읽기 → 고루틴

용어집 Glossary

가이드 전반의 핵심 용어를 한두 문장으로 정의한 참조 페이지다(일부 항목은 미완성).

• 액션(Action): 상태가 어떻게 진화하는지 기술하는 술어. 프라임 연산자가 든 불리언 식(x' = x). 여러 액션이 동시에 참일 수 있다. 활성화된(Enabled): 이번 스텝에 일어날 수 있는 액션.
• 행동(Behavior): 상태의 시퀀스, 곧 "타임라인". 스텝(Step): 시계가 한 번 째깍하며 상태 일부를 바꾸는 것 — 행동은 스텝의 시퀀스다. 스터터 스텝(Stutter Step): 아무것도 바꾸지 않는 전이. 모든 스펙은 스터터 불변이다.
• 공정성(Fairness): 언젠가 진전한다는 보장. 약한 = 영구히 활성화돼 있으면 언젠가 일어난다. 강한 = 영구히 비활성화돼 있지만 않으면 언젠가 일어난다.
• 속성(Property): 시스템에 대해 참이기를 바라는 것 = 안전성 + 라이브니스. 안전성(Safety): 나쁜 일이 일어나지 않는다(대부분 불변식). 불변식(Invariant): 모든 상태에서 참 — 모두 안전성 속성. 라이브니스(Liveness): 좋은 일이 반드시 일어난다 — 모두 시간 속성. 시간 속성(Temporal Property): 둘 이상의 상태에 걸치는 속성.
• 함수(Function): 정의역이 고정된 수학적 함수. 연산자(Operator): 프로그래밍 함수에 해당하며, 프라임 변수가 있으면 액션이다. 술어(Predicate): 불리언 식.
• 명세/스펙(Specification): 시스템의 엄밀한 수학적 기술. 모델(Model): 스펙 + 주입한 매개변수 + 요구하는 불변식. 상태 공간(State space): 가능한 모든 행동으로 도달 가능한 모든 상태.
• 모델 체킹(Model checking): 가능한 행동을 전부 생성해 속성 위반을 찾는 전수 테스트. TLC: TLA+ 모델 체커(이 사이트는 "모델 체커"와 같은 뜻으로 쓴다). 정리 증명기(Theorem Prover): 속성을 수학적으로 증명 — TLA+용은 TLAPS.
• 정형 기법(Formal Methods): 엄밀하고 검증된 코드를 쓰는 분야. 정형 명세 언어: 시스템을 기술해 오류를 찾는 언어. TLA+: 동시적 시스템을 모델링하는 "액션의 시간 논리". PlusCal: TLA+ 알고리즘을 쓰는 DSL. TLA+ Toolbox: 공식 IDE.

함정 포함 관계를 헷갈리지 말 것: 불변식 ⊂ 안전성(역은 성립 안 함), 라이브니스 ⊂ 시간 속성. 공정성으로 막지 않으면 행동은 영원히 스터터링할 수 있다. TLAPS는 모델 체킹보다 훨씬 어려워 이 가이드에서 다루지 않는다.

완역 읽기 → 용어집

표준 모듈 Standard Modules

TLC에서 쓸 수 있는 표준 모듈의 연산자를 한 줄 설명과 예로 정리한 레퍼런스다(Reals·RealTime 제외).

• Naturals: + - * ^ % < > <= >=, Nat, a..b, a \div b(내림 나눗셈). Integers: 여기에 Int와 -a.
• Sequences(PlusCal 프로시저에 필요): <<a, b, c>>, Seq(set), Len, Head, Tail, \o(연결), Append, SubSeq(seq, m, n)(양 끝 포함), SelectSeq(seq, Op(_))(필터).
• FiniteSets: IsFiniteSet, Cardinality. Bags(다중집합 = 항목 → 양의 정수 개수 함수): IsABag, SetToBag, BagToSet, BagIn, EmptyBag, (+), (-), BagUnion, \sqsubseteq, SubBag, BagOfAll, BagCardinality, CopiesIn.
• TLC(PlusCal assert에 필요): a :> b, f @@ g, Permutations, SortSeq, ToString, JavaTime, Print/PrintT, Any, Assert, RandomElement, TLCEval(재귀 가속 캐시), TLCGet/TLCSet(TLCSet(i, val)로 양의 정수 i에 값을 저장하고 TLCGet(i)로 읽음, TLCGet에 문자열을 주면 실행 통계 — "level", "diameter", "distinct" 등).
• TLCExt: AssertEq, AssertError, Trace, TLCModelValue. Json: ToJson, JsonSerialize, JsonDeserialize. Randomization: RandomSubset, RandomSetOfSubsets, TestRandomSetOfSubsets — 쓰면 TLC가 모든 상태를 검사하지 않는다.

Append(<<1, 2>>, 3) = <<1, 2, 3>>
SubSeq(<<7, 8, 9>>, 1, 2) = <<7, 8>>
[a |-> 1, b |-> 3] (+) [a |-> 1] = [a |-> 2, b |-> 3]
[a |-> 1, b |-> 3] (-) [a |-> 1] = [b |-> 3]

함정 Nat·Int·Seq(set)은 TLC가 열거할 수 없어 한정자나 CHOOSE에는 못 쓰고 멤버십 검사만 된다. @@는 키가 겹치면 왼쪽 값을 쓴다. TLC 모듈 연산자는 참조 투명성을 깨므로 조심하고 Any는 Spec에 쓰지 않는다. Assert는 체킹을 끝내지만 AssertEq는 끝내지 않는다. TLCSet 캐시는 워커 스레드마다 따로다.

완역 읽기 → 표준 모듈

기타 자료 Other Resources

TLA+를 더 배우고 읽고 쓰고 커뮤니티에 참여하는 데 쓸 외부 자료를 분류별로 모은 목록이다. 항목마다 저자의 짧은 평이 붙는다.

• 학습: Specifying Systems(포괄적 소개·정형적 기초, 모델 체킹은 거의 없음) · TLA+ Video Course(창시자의 강좌) · Introduction to Formal Pragmatic Modeling(프로덕션급 스펙 3개, 기초 지식 전제).
• 레퍼런스: TLA+ Language Reference Manual(Apalache 개발자들, 작업 중) · TLA+ Version 2(재귀 연산자·람다) · Current Versions of the TLA+ Tools(명령줄 TLC 플래그, TLC 모듈 연산자) · PlusCal Manual(정형적 정의·명령줄 옵션) · Summary of TLA+(치트 시트, ASCII 대신 조판 기호).
• 읽을거리·강연: How Amazon Web Services uses Formal Methods(대기업 관심의 계기, 저자가 TLA+를 알게 된 경로) · TLA+ 예제 저장소 · TLA+ in Practice and Theory · Let's Prove Leftpad · Designing Distributed Systems with TLA+(저자) · Weeks of Debugging can save you Hours of TLA+(툴박스 핵심 개발자 Markus).
• 도구: TLA+ Community Modules(최소한인 표준 라이브러리 보완) · Apalache(상태 열거 대신 기호 모델 체킹 — 저자는 Informal Systems 컨설팅 중임을 고지) · TLAPS(증명 시스템) · VSCode 플러그인 · TLA2JSON · tree-sitter-tlaplus.
• 커뮤니티: TLA+ 홈페이지 · conf.tlapl.us(연례 콘퍼런스, 보통 Strange Loop와 공동 개최) · TLA+ Google Group(핵심 개발자들이 답함) · r/tlaplus.

함정 Specifying Systems에는 PlusCal·재귀 연산자 같은 2004년 무렵 이후 기능이 없다. Summary of TLA+의 일부 구문(액션 합성 등)은 어떤 도구로도 검사할 수 없다. PlusCal 매뉴얼의 "label" 옵션은 필요한 레이블을 자동 생성한다.

완역 읽기 → 기타 자료