일반 팁

ASSUME 활용하기

모든 CONSTANT에는 그 상수(constant)에 어떤 값이 기대되는지 알려 주는 ASSUME이 있어야 한다. 모델 값(model value)이라면 보통 ASSUME으로 그 값이 어떤 집합(set)의 원소가 아니라고 말해 주는 것으로 충분하다. 어떤 것이 특정 데이터 타입이라고 말하고 싶다면 그 타입의 빈 값과 비교하면 된다. 그 타입이 아니면 TLC가 ASSUME에서 크래시하는데, 이는 제대로 실패하는 것과 같은 역할을 한다.

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

이렇게 해 두면 Threads는 집합이고 NULL은 스레드(thread)가 아니라는 것이 분명해진다.

구조체로 태그드 유니언 모델링하기

TLC에서는 문자열과 정수가 섞인 집합을 만들 수 없다. 그런 게 필요하다면 대신 type과 val 필드를 가진 구조체(struct)를 쓰면 된다.

{
 [type |-> "int", val |-> 1],
 [type |-> "str", val |-> "1"] \* ok
}

구조체의 함수 분해하기

변수를 구조체의 함수(function)로 인코딩하는 사람을 자주 본다:

VARIABLE state
WorkerState == [queue: Seq(Msg), online: BOOLEAN]
Types ==
  state \in [Worker -> WorkerState]

\* ...

프로그래밍 언어에서 하는 방식에 더 가깝긴 하다. 하지만 TLA+에서는 다루기가 더 어려운데, 변수는 한 스텝(step)에 한 번만 갱신할 수 있기 때문이다. 그래서 한 스텝에서 online과 함께 queue도 갱신하고 싶다면 둘을 같은 식(expression) 안에서 처리해야 한다. 즉 이렇게는 쓸 수 없다

Label:
  state[w].online = FALSE;
  state[w].queue = <<>>;

대신 다음처럼 변수를 별개의 두 변수로 쪼개는 편이 더 쉽다:

VARIABLES worker_queue, worker_online

Types ==
  /\ worker_queue \in [Worker -> Seq(Msg)]
  /\ worker_online \in [Worker -> BOOLEAN]

\* ...

그러면 worker_queue와 worker_online을 따로따로 갱신할 수 있다.

이 방식의 단점은 1) 순수 TLA+로 작업할 때 UNCHANGED 문이 조금 더 지저분해지고, 2) 실제 구현의 모습과 조금 더 멀어진다는 것이다. 그래도 장점이 충분히 커서 그럴 만한 가치가 있다.

대체로 나는 구조체를 주로 메시지 본문 같은 불변 값에 쓴다.

안전성 모델과 라이브니스 모델 분리하기

라이브니스 속성(liveness property)은 검사하는 데 훨씬 오래 걸리기 때문에(게다가 대칭 집합(symmetry set)도 쓸 수 없다), 나는 라이브니스 속성만 검사하는 별도의 모델(model)을 두고, 거기에는 더 작은 상수를 쓴다.

모듈의 여분 공간 활용하기

모든 모듈(module)은 다음 형태를 따라야 한다

\* top area
---- MODULE name ----
\* actual module
====
\* bottom area

위쪽 공간과 아래쪽 공간에 있는 내용은 전부 무시된다. 나는 아래쪽 영역을 “스크래치 공간”으로 삼아 온갖 TLA+ 코드를 넣어 두기를 좋아한다. 위쪽 영역에는 모델링하려는 문제 도메인과 요구 사항에 대한 설명을 더 쓰고, 스펙 자체에 관한 정보도 적어 둔다.

최근에는 위쪽 영역에 설정 데이터를 넣고 스크립트로 그 부분을 겨냥해 처리하는 실험을 하고 있다. 이 가이드에 실린 스펙 diff 중 상당수를 그렇게 생성했다.

THEOREM

TLA+에는 THEOREM 키워드가 있는데, 표면상으로는 스펙의 속성(property)을 선언하는 용도다:

THEOREM Spec => []TypeInvariant

모델 체커(model checker)에는 아무 영향도 주지 않지만, 시스템의 속성을 문서화하는 데는 유용할 수 있다.

TypeInvariant와 ModelInvariant

TypeInvariant는 이미 많이 써 왔다. 어떤 시스템에든 좋은 불변식(invariant)이고, TypeInvariant에서는 늘 모든 변수를 빠짐없이 다루는 게 좋다. 원칙적으로 나는 TypeInvariant가 변수의 가능한 값만 다루고, 정당한 값까지는 다루지 않게 하는 편을 좋아한다. 예를 들어 두 수 집합이 서로소여야 한다면, 나는 이를 두 불변식으로 나눈다:

TypeInvariant ==
  /\ set1 \subseteq Int
  /\ set2 \subseteq Int

SetsAreDisjoint ==
  /\ set1 \intersect set2 = {}

SetsAreDisjoint를 TypeInvariant에 넣지 않는 이유는, 이것을 단순한 범위 검사라기보다 시스템의 “정확성” 속성으로 보기 때문이다.

모델 불변식(model invariant)은 TypeInvariant와 비슷하지만, 상태 공간(state space)이 유한한지 확인하는 데 쓴다는 점이 다르다. 예를 들면 이렇다:

CONSTANTS MinInt, MaxInt
ASSUME {MinInt, MaxInt} \subseteq Int

ModelInt == MinInt .. MaxInt
ModelInvariant ==
  /\ set1 \subseteq ModelInt
  /\ set2 \subseteq ModelInt

그런 다음 스펙이 ModelInvariant를 만족하도록 작성하거나, 모델 실행에 상태 제약(state constraint)으로 추가하면 된다.

매크로 활용하기

매크로(macro)는 PlusCal에서 문(statement)을 재사용하는 주된 수단이다.

while 루프는 해롭다

while 루프는 루프를 한 바퀴 돌 때마다 새 상태를 하나씩 만들어서, 스펙에 동시성(concurrency)과 상태 공간 폭발(state space explosion)을 잔뜩 더한다. 이를테면 큐에서 읽어 올 때처럼 가끔은 이게 바로 원하는 동작이다. 하지만 초보자들이 다음처럼 while 루프로 계산을 하는 모습을 자주 본다:

Double:
  while i <= Len(seq) do
    seq[i] := seq[i] * 2;
    i := i + 1;
  end while;

대신 시퀀스(sequence) 전체를 한 스텝에 재할당하자:

Double:
  seq := [i \in 1..Len(seq) |-> seq[i] * 2];

상태 스위핑

여기에서 다뤘다.

UNCHANGED 관리하기

변수가 많으면 모든 것이 정의되어야 한다는 원칙을 지키려고 쓰는 문이 금방 거추장스러워진다. 다행히 변수들을 시퀀스로 묶은 다음, 그 그룹들의 시퀀스에 UNCHANGED를 쓰면 된다.

VARIABLE worker_queue, worker_online
VARIABLE topic_subscribers, topic_id

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

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

헬퍼 액션

다음 상태 관계(next-state relation)를 여러 액션(action)으로 나눠도 괜찮다. 내가 자주 하는 일 하나는 pc를 갱신하는 헬퍼를 작성하는 것이다:

Trans(agent, a, b) ==
  /\ pc[agent] = a
  /\ pc' = [pc EXCEPT ![agent] = b]

그러면 다른 액션 안에서 Trans(agent, "state1", "state2")라고 쓸 수 있다.

@

함수 갱신에서 @는 이전 값을 가리킨다.

\* Verbose
f' = [f EXCEPT ![1][2].a = f[1][2].a + 1]

\* Clean
f' = [f EXCEPT ![1][2].a = @ + 1]

액션 매개변수화하기

이렇게 쓰는 대신

Add ==
  \E w \in Worker: s' = s \union {w}

Remove ==
  \E w \in Worker: s' = s \ {w}

Next == Add \/ Remove

이렇게 쓰자

Add(w) == s' = s \union {w}
Remove(w) == s' = s \ {w}

Next ==
  \E w \in Worker:
    \/ Add(w)
    \/ Remove(w)

\E를 맨 아래 층으로 옮기고 액션에는 값을 넘겨주자. 이렇게 하면 같은 값을 여러 액션에서 재사용할 수 있어서 더 좋다. 추가되거나 제거되는 워커를 전부 로그로 남기고 싶다고 해 보자. 첫 번째 버전의 스펙에서는 이걸 쉽게 할 수 없지만, 두 번째 버전에서는 이렇게 쓰면 된다

Log(w) == log' = Append(log, w)

Next ==
  \E w \in Worker:
    /\ \/ Add(w)
       \/ Remove(w)
    /\ Log(w)

액션 속성으로 리팩터링하기

액션을 단순화할 때는 그 단순화 때문에 액션이 달라지지 않았는지 확인하고 싶다.

OldAction(user) ==
  seq' = seq \o <<user>>

NewAction(user) ==
  seq' = Append(seq, user)

두 액션이 동등한지 확인하는 액션 속성(action property)을 추가하면 이를 검사할 수 있다:

RefactorProp == [][
  \A u \in User:
    OldAction(user) = NewAction(user)
]_vars

액션을 확장하려는 경우라면 NewAction이 하는 일이 OldAction이 하는 일의 상위집합이기만 하면 된다. 그럴 때는 =>를 = 대신 써서 요구 조건을 느슨하게 할 수 있다.