대부분의 엔지니어들이 TLA+ 사용에 대해 제기하는 첫 번째 반론은 구문(syntax)이 적대적이라는 것입니다. 코드가 아니라 LaTeX처럼 보이기 때문입니다. 하지만 이제 최첨단 LLM(Large Language Models)은 TLA+를 쉽게 생성할 수 있습니다. 시스템을 이해하고 "정확성(correctness)"이 무엇을 의미하는지 정의하는 것은 여전히 여러분의 책임이며, 시간 논리(temporal logic)에 대한 고차원적인 이해가 필요합니다. 이 글에서 시간 논리에 대해 설명하겠습니다. 마지막에는 Claude를 사용하여 TLA+ 명세(spec)를 시작할 수 있는 예시 프롬프트를 보여드리겠습니다.

장난감 문제 (A toy problem)

여기에 고전적인 퍼즐이 있습니다. 당신에게는 콩 통이 하나 있습니다. 각 콩은 흰색 또는 검은색입니다. 통은 비어 있지 않은 상태로 시작합니다. 콩이 최소 2개 이상 있는 동안 다음을 반복합니다:

• 콩 2개를 선택합니다.
• 색상이 같다면: 둘 다 버리고, 흰색 콩 1개를 추가합니다.
• 색상이 다르다면: 둘 다 버리고, 검은색 콩 1개를 추가합니다.

두 가지 질문:

• 콩의 개수가 0에 도달할 수 있을까요?
• 만약 알고리즘이 b = 1인 상태로 종료된다면, 시작 시점에 무엇이 참이었어야 할까요?

당신은 아주 열심히 고민할 수도 있습니다. 아니면 TLA+로 작성하여 모델 체커(model checker)가 두 질문에 자동으로 답하게 할 수도 있습니다. 핵심은 생각을 피하는 것—또는 적어도, 당신의 생각이 맞았는지 기계가 검증하게 하는 것입니다. 또는 당신의 생각이 맞다는 것을 친구들에게 설득하거나, 연구 논문의 동료 심사(peer-review) 위원회를 설득하는 것입니다.

논리식(logical formulae)이 상태 머신(state machine)을 만드는 방법

TLA+는 1990년대에 Leslie Lamport에 의해 발명되었습니다. TLA는 "Temporal Logic of Actions"의 약자이며, TLA+는 특정 언어의 이름입니다. TLA+는 기본적인 불리언 논리(boolean logic)를 가지고 있으며, 집합(sets)과 함수(functions), 그리고 양화(quantification, "모든" 및 "존재한다")를 포함합니다. 또한 곧 살펴보게 될 시간적(temporal) 연산자도 가지고 있습니다.

TLA+로 명세(specification)를 작성할 때, 당신은 상태 머신(state machine)을 정의하는 논리식(logical formula)을 작성하는 것입니다. 이 머신은 고정된 변수 집합을 가지며, 각 *상태(state)*는 변수에 값이 할당된 상태를 의미합니다. 콩 문제의 경우, 변수는 w (흰색 콩의 수)와 b (검은색 콩의 수)가 있습니다. 각 상태는 w와 b에 값이 할당된 것입니다.

*행동 (behavior)*은 상태들의 시퀀스(sequence)이며, *명세 (specification)*는 허용된 행동들의 집합입니다.

초기 상태 (Initial state)

우리는 초기 상태 규칙(initial-state rule)이 필요합니다. 이는 우리가 시작하고자 하는 상태들에 대해서만 참이 되는 술어(predicate)입니다. 영어로 표현하면: “캔은 처음에 비어 있지 않다” 또는 w + b > 0 입니다.

다음 중 어떤 초기 상태가 술어와 일치할까요?

b = 0 /\/ w = 0
b = 0 /\/ w = 4
b = 6 /\/ w = 1
...

TLA+에서 “/\”는 “and”를 의미하므로, b = 0 /\ w = 0은 “b = 0 이고 w = 0이다”를 의미합니다.

두 번째와 세 번째 상태는 술어와 일치합니다. 첫 번째는 w와 b의 합이 0이므로 일치하지 않으며, 마지막 상태는 1과 문자열 "foo"를 더할 수 없으므로 말이 되지 않습니다. TLA+에는 타입 시스템 (type system)이 없고 집합 (sets)만 존재하기 때문에, w가 문자열이 되는 것을 막을 방법이 없습니다. Lamport는 이런 것을 “어리석은 (silly)” 것이라고 부릅니다. 우리는 w와 b가 자연수 (natural numbers)여야 한다고 명시함으로써 이러한 어리석은 상태를 방지합니다.

EXTENDS Integers
Init == w \in Nat /\ b \in Nat /\ w + b > 0

EXTENDS Integers는 자연수 집합인 Nat와 같이 정수를 다루는 데 필요한 모든 것을 가져옵니다. \in은 집합 멤버십 연산자 (set-membership operator)이며, ==는 “~로 정의됨 (defined as)”을 의미합니다. 이는 C 언어와는 다소 반대라 혼란스러울 수 있는데, C에서는 단일 =가 equality(등가)를 테스트하는 반면, TLA+에서 ==는 (매크로처럼) 수식 (formula)에 이름을 붙이는 역할을 합니다.

상태 전이 (State transitions)

상태 전이 규칙 (state-transition rule)은 현재 상태와 다음 상태라는 두 개의 상태에 대한 술어로, 어떤 전이가 합법적인지를 말해줍니다. 우리의 알고리즘을 TLA+의 상태 전이 규칙으로 바꿔봅시다.

영어 문장으로부터 시작하면 다음과 같습니다:

• 흰 콩 2개: 흰 콩 2개를 제거하고, 흰 콩 1개를 추가함 → 순 효과: w -= 1
• 검은 콩 2개: 검은 콩 2개를 제거하고, 흰 콩 1개를 추가함 → 순 효과: b -= 2
• 각각 1개씩: 흰 콩 1개와 검은 콩 1개를 제거하고, 검은 콩 1개를 추가함 → 순 효과: w -= 1

첫 번째와 세 번째 케이스가 상태에 미치는 효과가 동일하다는 점에 주목하세요. 둘 다 단순히 w에서 1을 빼고 b는 그대로 둡니다. 이것이 바로 무언가를 정밀하게 기록할 때 자연스럽게 얻게 되는 통찰입니다.

TLA+에서 이것들은 세 가지 **액션 (actions)**이 됩니다:

WW == w > 1 /\/ w' = w - 1 // UNCHANGED b * Picked 2 white
BB == b > 1 // b' = b - 2 // w' = w + 1 * Picked 2 black
WB == w > 0 // b > 0 // w' = w - 1 // UNCHANGED b * Picked 1 of each

여기서 우리는 처음 보는 두 가지 연산자를 보게 됩니다. 프라임 (prime, ') 연산자는 "이 변수의 다음 값"을 의미합니다: w' = w - 1은 "다음 상태(next state)에서 w는 현재의 w에서 1을 뺀 값과 같을 것이다"라는 뜻입니다. UNCHANGED b는 b' = b의 축약형입니다. 여러분은 모든 액션(action)에서 모든 변수를 고려해야 합니다. TLA+는 언급되지 않은 변수가 그대로 유지될 것이라고 가정하지 않습니다. 이는 번거로운 일이지만, 각 액션이 전체 상태(state)에 어떤 영향을 미치는지 생각하도록 강제합니다.

프라임이 없는 항들은 **가드 (guard)**입니다. 이는 액션이 실행되기 위해 지금 반드시 충족되어야 하는 조건입니다. 프라임이 있는 항들은 **할당 (assignment)**입니다. 즉, 다음 상태가 어떤 모습일지를 나타냅니다. 만약 가드가 거짓(false)이라면, 해당 액션은 비활성화됩니다. *는 주석을 시작합니다 (네, 백슬래시와 별표입니다).

완전한 TLA+ 명세 (spec)

여기 전체 명세(specification)가 있습니다:

-------------- MODULE beans -----------------
EXTENDS Integers
VARIABLES w, b
...

Next 공식은 세 가지 액션 모두의 OR (\/)로 정의됩니다. 즉, 어떤 주어진 상태에서든 가드가 충족되는 액션들은 활성화됩니다. 이것이 바로 **비결정론 (nondeterminism)**입니다. 명세는 어떤 액션이 일어나는지 말하지 않고, 단지 어떤 액션들이 가능한지만을 말합니다. 모델 체커(model checker)는 이 모든 가능성을 탐색합니다.

Spec 라인은 모든 TLA+ 명세의 중추이며, 여러분이 읽게 될 거의 모든 TLA+ 명세에서 볼 수 있습니다. 이 라인은 다음과 같이 말합니다: "이 명세에 의해 허용되는 모든 동작(behavior)은 Init이 참(true)인 초기 상태(initial state)에서 시작하며, 모든 전이(transition)는 Next를 만족한다." WF_vars(Next) 부분은 "알고리즘은 계속해서 진전(progress)을 이루어야 한다. 즉, 액션이 활성화되었을 때 영원히 멈춰 있을 수 없다"는 것을 의미합니다. 이것을 **공정성 제약 (fairness constraint)**이라고 부릅니다. 계속 지켜봐 주세요...

[][Next]_vars 부분은 제가 건너뛸 복잡한 내용을 담고 있습니다. 이를 깊이 이해하고 싶다면 Lamport의 "Specifying Systems"를 읽어보세요. 프롬프팅(prompting) 목적을 위해서라면, 그저 저 부분이 그 역할을 수행한다는 것만 알면 됩니다.

상태와 동작 (States and behaviors)

**동작 (behavior)**이란 초기 상태(initial state)에서 시작하여 각 단계가 Next에 의해 허용되는 상태들의 무한한 시퀀스(sequence)를 의미합니다. 관례적으로 동작은 무한히 길게 정의됩니다. 만약 알고리즘이 종료된다면(더 이상 어떤 동작도 활성화되지 않는 상태에 도달한다면), 마지막 상태는 그저 영원히 반복됩니다. 이러한 반복을 **스터터링 (stuttering)**이라고 부릅니다. 따라서 TLA+에서 "종료 (termination)"란 알고리즘이 스터터링 상태에 도달하여 그곳에 머무는 것을 의미합니다.

우리의 명세(spec)에는 무한히 많은 초기 상태(init states)가 존재합니다. w + b > 0을 만족하는 임의의 자연수 쌍은 모두 유효한 초기 상태입니다. 상태 공간(state space)의 부분 집합, 즉 b=3이고 w=5에서 시작하는 상태들만 살펴보겠습니다:

각 노드(node)는 하나의 상태입니다. 각 엣지(edge)는 유효한 전이(transition)이며, 어떤 동작(action)이 적용되는지 라벨이 붙어 있습니다. 어떤 엣지에는 "WW/WB"라고 적혀 있는데, 이는 w > 1이고 b > 0일 때 WW와 WB 동작이 모두 활성화되어 동일한 다음 상태로 이어지기 때문입니다 (두 동작 모두 단순히 w를 1만큼 감소시킵니다). 모델 체커(model checker)는 두 동작을 모두 탐색하지만 동일한 후속 상태(successor state)를 발견하므로, 이들은 하나의 엣지로 합쳐집니다.

이 그림에서 **동작 (behavior)**은 초기 노드에서 터미널 노드(terminal node)까지의 경로이며, 그 뒤에는 스터터링이 이어집니다. 다음은 하나의 동작의 예시입니다:

모델 체킹 (Model-checking)

모델 체커인 TLC는 초기 상태 집합에서 시작하여, 다음 상태 관계(next-state relation)를 적용해 후속 상태들을 생성하며, 이미 확인한 상태를 다시 방문하지 않기 위해 해싱(hashing, TLC에서는 이를 "핑거프린팅 (fingerprinting)"이라고 부릅니다)을 사용합니다.

TLC는 상태를 발견함에 따라 불변량(invariants)과 속성(properties)을 검사합니다. (이것들이 무엇인지는 잠시 후에 배우겠지만, 지금은 다음과 같이 이해하세요: 이것들은 당신의 명세가 올바름을 보여주는 단언(assertions)입니다.) 만약 TLC가 위반(violation)을 발견하면, 잘못된 상태로 이어지는 상태의 시퀀스인 반례(counterexample)를 보고합니다. TLC는 너비 우선 탐색(breadth-first search)을 수행하기 때문에, 불변량 위반에 대해 가장 짧은 반례(또는 가장 짧은 것 중 하나)를 찾아냅니다. 이는 진단에 매우 유용합니다. 100단계의 트레이스(trace)보다 4단계의 트레이스가 디버깅하기 훨씬 쉽기 때문입니다.

명세와 설정 (The spec and the config)

명세와 설정 (The spec and the config)

TLA+ 명세 (specs)는 시제 논리 (temporal logic)가 담긴 beans.tla 파일과 모델 검사 (model-checking) 설정이 담긴 beans.cfg 파일, 이렇게 두 개의 파일로 구성됩니다. 왜 파일이 두 개일까요? 명세 (specification)는 시스템에 대한 이상적인 기술이며, 그 상태 공간 (state space)과 동작 (behaviors)은 대개 무한합니다. 이 명세를 통해 할 수 있는 일은 매우 많습니다. 명세가 올바른지 *증명 (prove)*하거나, 알고리즘을 문서화하여 친구들에게 설명하는 용도로 사용하는 것 등이 있습니다. 모델 검사 (model-checking)는 명세를 사용하는 여러 방법 중 하나일 뿐이므로, 모델 검사 설정은 별도의 파일에 둡니다.

물론, 상태가 무한하다면 모델 검사는 불가능합니다. 우리는 보통 초기 상태 (init-state) 집합의 크기에 제한을 두거나, 수행되는 액션 (actions)의 횟수를 제한하는 등의 방식으로 상태 공간을 인위적으로 제한해야 합니다. 이러한 모든 제한 사항은 설정 (config) 파일에 포함되어야 합니다.

명세에 버그가 있다면, 대개 작은 유계 모델 (bounded model)에서 이를 발견하게 됩니다. (우리는 이를 "소규모 모델 가설 (small-model hypothesis)"라고 부릅니다.) 실제로 첫 번째 검사에서 1~2초 만에 명백한 버그를 잡아내는 경우가 많습니다. 위반 (violation) 없이 몇 시간 동안 실행을 지속한다면, 더 높은 신뢰를 가질 수 있습니다. 모든 버그를 찾기 위해 경계 (bound)를 얼마나 크게 설정해야 할까요? 그것은 말하기 어렵습니다. 알고리즘에 대한 여러분의 추론과 직관에 달려 있습니다.

그럼, 이것이 beans.tla라고 가정해 봅시다 (위에서 보여드린 것과 동일한 명세입니다):

-------------- MODULE beans -----------------
EXTENDS Integers
VARIABLES w, b
...

이것은 초기 상태가 무한하기 때문에 경계가 정해지지 않았으며 (unbounded), 모델 검사를 할 수 없습니다. 모델에 경계를 설정하기 위해, 저는 Init을 다음과 같이 업데이트할 수 있습니다:

CONSTANTS WMAX, BMAX
Init == w \in 0..WMAX /\ b \in 0..BMAX /\ w + b > 0

beans.cfg는 다음과 같습니다:

CONSTANTS
WMAX = 3
BMAX = 3
...

이제 초기 상태는 15개이며, 전체 상태는 17개입니다. (연습 문제: 왜 이 숫자들이 나오는지 알아낼 수 있나요?)

질문에 답하기

너무 깊이 고민하지 않고도 우리의 두 가지 질문에 답하기 위해 모델 검사기 (model-checker)인 TLC를 어떻게 사용할 수 있을까요?

콩의 개수가 0에 도달할 수 있는가? 우리는 모든 도달 가능한 상태(reachable state)에서 항상 참이라고 주장하는 상태 술어(state predicate)인 **불변량 (invariant)**을 작성합니다:

NotEmpty == w + b > 0

우리는 beans.tla에 이를 정의하고 beans.cfg에서 참조함으로써 TLC가 이를 확인하도록 합니다:

INVARIANT NotEmpty

TLC는 전체 도달 가능한 상태 그래프(reachable state graph)를 너비 우선 탐색 (breadth-first search)하여 어떤 상태도 이를 위반하지 않음을 확인합니다. 콩 통은 결코 비지 않습니다.

왜 그럴까요? 가드 (guards)를 살펴보십시오. 모든 액션 (action)은 활성화되기 위해 최소 2개의 콩을 필요로 합니다 (w > 1, b > 1, 또는 w > 0 / > 0). 그리고 모든 액션은 전체 콩의 개수를 정확히 1씩 감소시킵니다. 따라서 콩이 1개 남게 되면 어떤 액션도 활성화되지 않으며 알고리즘은 종료됩니다. 1에서 0으로 갈 수는 없습니다.

종료 시점에 b = 1이라면, 초기 상태에서는 무엇이 참이었어야 하는가? b를 변경하는 유일한 액션인 BB를 보십시오. 이는 b를 2만큼 감소시킵니다. 이는 초기 상태부터 끝까지 b의 기우성 (parity, 홀수 또는 짝수)이 변하지 않음을 의미합니다. 따라서 b = 1 (홀수)로 종료된다면, 시작 시점의 b도 홀수였어야 합니다. 우리는 이를 단일 상태가 아닌 전체 동작 (behavior)에 대한 공식인 **시제 속성 (temporal property)**으로 표현할 수 있습니다:

TerminationWithOneBlack == (b % 2 = 1) => <>[](b = 1 /\
 w = 0)

이를 다음과 같이 읽습니다: “만약 b가 홀수라면, 결국 항상 (eventually-always) b는 1이 되고 w는 0이 된다.”

여기에는 두 가지 **시제 연산자 (temporal operators)**가 사용되었습니다: <> (다이아몬드, “언젠가 (eventually)”를 의미)와 [] (박스, “항상 (always)”을 의미). 이들이 <>[]로 결합되면 “결국 어떤 상태에 도달하여 그 상태를 유지한다”는 의미가 되며, 이는 정확히 종료 (termination)를 의미합니다.

우리는 이 정의를 beans.tla에 추가하고 beans.cfg에서 참조합니다:

PROPERTY TerminationWithOneBlack

NotEmpty에 사용했던 INVARIANT 대신 PROPERTY를 beans.cfg에 사용한 이유는 이것이 시제 속성 (시제 연산자를 사용하며 전체 동작에 적용됨)이기 때문입니다. TLC는 모든 동작에 대해 이 속성이 유지되는지 검증하여, 홀수 b에서 시작하는 모든 동작이 b = 1로 종료됨을 확인합니다.

하지만 잠깐—b가 홀수라면 결국 b=1이고 w=0이 된다는 것이 정말로 사실일까요? 만약 b가 홀수인데 상태 머신(state machine)이 아무것도 하지 않고 그냥 가만히 있다면 어떻게 될까요? 바로 그 점을 공정성 제약 조건(fairness constraint)인 WF_vars(Next)가 보장합니다. 이 조건은 만약 Next가 지속적으로 활성화되어 있다면(즉, 최소 두 개의 콩이 있기 때문에 동작 중 하나가 활성화된 상태라면), 그것이 결국 실행될 것임을 의미합니다. 이는 어떤 "결국(eventually)" 속성이 참이 되기 위해 반드시 필요합니다.

시제 연산자 (The temporal operators)

시제 논리(Temporal logic)는 일반적인 1차 논리(first-order logic) 위에 두 가지 핵심 연산자를 추가하며, 이를 흥미로운 방식으로 조합할 수 있습니다.

<>P

(eventually P / 결국 P): 이 동작의 어느 시점에 P가 참이 됩니다. 만약 P가 잠시 나타났다가 사라지더라도 이는 여전히 참으로 간주됩니다.

[]P

(always P / 항상 P): 이 동작의 모든 시점에 P가 참입니다.