툴박스 너머

대부분의 사람은 TLA+를 쓸 때 툴박스(Toolbox)를 쓴다. 하지만 vscode나 명령줄로도 쓸 수 있다.

명령줄

CLI의 핵심 파일은 tla2tools.jar다. 이 링크에서 바로 내려받을 수 있다. 툴박스를 설치한 디렉터리의 최상위에서도 찾을 수 있다.

Tlatools에는 TLC, PlusCal 변환기(PlusCal translator), LaTeX PDF 생성기(Tla2Tex), 파서(SANY)라는 네 가지 하위 도구가 있다. 뒤의 두 도구에 대한 설명은 Lamport에게 맡기고, 여기서는 변환기와 모델 체커(model checker)에 집중하겠다.

PlusCal 변환기

파일 안의 PlusCal 알고리즘을 변환하려면 다음과 같이 입력한다.

$ java -cp tla2tools.jar pcal.trans file.tla

이렇게 하면 다음 일이 일어난다.

파일 안에서 텍스트를 TLA+로 변환한다
백업용으로 file.old를 쓴다
file.cfg를 설정 파일로 쓰는데, 이미 있으면 덮어쓴다.

(3)을 막으려면 -nocfg를 플래그로 file.tla 앞에 붙인다. 변환기가 file.old를 쓰지 못하게 막을 방법은 없다. 나는 이 파일들을 찾아서 지워 주는 셸 감시기(watcher)를 따로 돌린다.

변환기의 나머지 옵션은 전부 여기의 67-69쪽에서 읽을 수 있고, java -cp tla2tools.jar pcal.trans -h를 실행해서 볼 수도 있다.

TLC

모델에 대해 TLC를 돌리려면 다음과 같이 입력한다.

$ java -jar tla2tools.jar -config configfile.cfg specfile.tla

-config를 주지 않으면 TLC는 기본적으로 specfile.cfg를 찾는다. 이 파일에 모델 실행을 위한 설정 옵션이 전부 들어 있다.

TLC에는 다른 플래그도 있지만, 설정 파일 형식을 쓸 줄 모르면 다 소용없으니 그것부터 이야기하자.

설정 파일 형식

모델 체킹(model checking) 설정 언어는 명령줄에서 TLC를 쓰기 위한 전용 DSL이다. 툴박스가 뒤에서 감춰 주는 것이 바로 이것이다.

모든 설정 파일에는 SPECIFICATION {spec} 줄이 있어야 하는데, 여기서 Spec은 초기 상태(initial state)와 다음 상태를 아우르는 액션(action)이면 무엇이든 된다. 관례상 이것을 Spec이라고 부르지만 필수는 아니다 — 설정 파일마다 시스템의 서로 다른 변형을 테스트하고 싶을 때 쓸모 있는 점이다.

검사하려는 불변식(invariant)에는 INVARIANT를, 시간 속성(temporal property)에는 PROPERTY를 앞에 붙여야 한다. 둘 다 쉼표로 여러 개를 나열할 수 있어서, 예를 들어 INVARIANT TypeInvariant, IsSafe는 유효한 줄이다. 툴박스와 달리 식(expression)을 불변식으로 지정할 수는 없다 — 반드시 이름 붙은 연산자(operator)여야 한다.

노트

그런데 툴박스에서는 왜 되는 걸까? 식을 불변식으로 지정하면 툴박스는 별도의 MC.tla 파일을 만들어 그 식을 연산자로 추가한 다음, 새 연산자를 불변식으로 삼아 MC.tla를 모델 체킹한다. 아래에 나오는 상수 식에 대한 제약을 피할 때도 비슷한 방법을 쓴다.

상수(constant)는 CONSTANT name = value로 쓴다. 값(value)으로는 단순한 값이나 단순한 값의 집합(set)을 쓸 수 있지만, 함수(function)나 식은 쓸 수 없다. 일반 대입 대신 모델 값(model value)을 지정하려면 CONSTANT name = name이라고 쓴다. 모델 값의 집합을 만들려면 name = {a, b, c}라고 쓰는데, 이때 a, b, c는 식별자다(문자열이 아니다).

경고

설정 파일에서는 임포트를 쓸 수 없는데 음수는 엄밀히 따지면 Integers 임포트이므로, 음수를 상수로 지정할 수 없다.

기본적인 설정 파일은 다음과 같은 모습이다.

SPECIFICATION Spec

INVARIANT Inv1, Inv2
PROPERTY Prop1

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

설정 파일에는 CONSTRAINT, ACTION-CONSTRAINT, VIEW도 넣을 수 있으며, 각각 대응하는 툴박스 옵션과 똑같이 동작한다. cfg에서 CHECK_DEADLOCK FALSE로 데드락(deadlock) 검사를 끌 수도 있다.

마지막으로 ALIAS가 있다. 이것을 쓰면 명령줄에서 에러 트레이스 탐색기(Error Trace Explorer)를 사실상 흉내 낼 수 있다. 다음과 같은 스펙이 있다고 하자.

---- MODULE aliases ----
EXTENDS Integers

VARIABLE x
Init ==
  x = 0

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

Alias ==
  [x |-> x,
   nextx |-> x',
   incx |-> x + 1]
=====

설정 파일에 ALIAS Alias를 추가하면, 에러 트레이스(error trace)가 에러 출력에 x, nextx, incx의 값을 보여 준다.

노트

별칭(alias)은 표준 에러 출력을 대체한다. 별칭에 넣지 않은 변수는 에러 출력에도 나타나지 않는다.

TLC 옵션

이제 설정 파일을 돌리는 법을 알았으니 TLC 옵션으로 돌아가자. 옵션 전체는 java -jar tla2tools.jar -help(절대 -h가 아니다)로 보거나 여기(9-11쪽)에서 읽을 수 있다. 대부분은 이름만 봐도 알 수 있거나 툴박스 옵션과 같다. 사용법에 대한 자세한 내용은 툴박스 사용하기 주제를 참고하라. 특히 눈여겨볼 옵션은 다음과 같다.

-continue: 위반을 발견한 뒤에도 모델 체킹을 계속한다. 불변식 위반이 하나도 빠짐없이 전부 출력으로 쏟아져 나온다.

경고

이 옵션을 툴박스에서 플래그로 넘기지 마라. 안 그러면 툴박스는 에러가 난 줄 안다.

An error has occurred. See error log for more details.

assertion failed: Two traces are provided. Unexpected. This is a bug

-dump file

TLC가 도달한 모든 상태(state)를 file에 아무 순서 없이 쓴다. 상태들이 서로 어떻게 연결되는지 알고 싶다면 대신 다음과 같이 쓴다.

-dump dot file

이 옵션은 대신 graphviz 그래프 파일을 출력한다. 노드는 상태이며, 각 노드에는 변수 할당값이 레이블로 붙는다. TLC는 파일 이름에 확장자를 붙여 주지 않으니 직접 붙여야 한다.

노트

스펙에 라이브니스 속성(liveness property)이 있으면 TLC는 file_liveness도 쓴다. 이것은 내부 표현이므로 무시해도 된다.

-dump dot,colorize file이라고 쓰면 간선이 관련된 액션에 따라 색이 입혀지고, -dump dot,actionlabels라고 쓰면 간선에 해당 액션이 레이블로 붙는다. 둘을 함께 쓸 수도 있다.

-metadir dir

TLC는 탐색한 상태 공간(state space)을 스펙과 같은 디렉터리에 저장하는 대신 dir에 저장한다. 나는 CLI를 스크립트로 다룰 때 이 옵션이 유용했는데, 상태 공간을 임시 디렉터리에 저장해 두면 정리하기 쉽기 때문이다.

-workers num/auto

모델 체킹에 쓸 워커 스레드(thread) 수를 지정한다. 이 옵션은 아주 중요하다. 이 옵션이 없으면 CLI는 기본값으로 워커 하나만 쓴다. auto를 넘기면 코어 수만큼 워커를 쓴다.

-noGenerateSpecTE

최신 버전의 TLA+는 속성 에러를 발견할 때마다 에러 파일을 저장한다. 이 플래그는 그 파일을 쓰지 않게 한다.

-fpmem num

시스템 메모리 중 몇 퍼센트를 모델 체킹용으로 떼어 둘지를 소수로 나타낸다. 기본값은 0.25(메모리의 1/4)다.