환경 설정

프로젝트 설정하기

가르치는 입장에서 나는 처음 배우는 사람에게 TLA+ IDE부터 쓰게 하는 편이다. 이 IDE는 초보자가 어려워할 수 있는 TLA+의 몇몇 부분을 추상화해 감춰 준다. 툴박스(Toolbox)의 최신 버전은 여기에서 내려받을 수 있다. 툴박스가 동작하려면 Java가 필요하다.

툴박스를 받고 나면 다음과 같은 화면이 보인다:

File > Open Spec > Add New Spec에서 새 스펙을 만든다.

그러면 다음과 같은 내용이 보일 것이다:

---- MODULE wire ----

====

‘유서 깊은 역사적 이유’로, MODULE $name은 최소 네 개의 대시로 둘러싸여야 하고, 모듈(module)은 최소 네 개의 등호로 끝나야 하며, 모듈의 $name은 파일 이름과 일치해야 한다(대소문자 구분). 모듈 이름 위와 ==== 아래에 있는 내용은 모두 무시되므로, 그곳은 메모를 적어 두기에 좋은 자리다.

이제 이 내용을 wire의 내용으로 바꾸자. 그러면 다음과 같이 된다:

(맨 위에는 MODULE 줄이 하나, 맨 아래에는 ==== 줄이 하나만 있어야 한다. 스펙 이름을 예제와 달리 Wire.tla로 지었다면 첫 줄의 모듈 이름도 꼭 바꿔 주자!)

스펙 변환하기

핵심 과정 개요에서 말했듯이, 우리는 PlusCal을 가르칠 것이다. File > Translate PlusCal Algorithm에서 PlusCal을 변환(translate)하자.

그러면 다음 화면이 보일 것이다:

모델 실행하기

이 스펙을 실제로 TLC로 검사하려면, 검사할 새 모델(model)을 만들어야 한다. TLC Model Checker > New Model에서 만든다.

그러면 다음 페이지가 보일 것이다:

1. “What is the behavior spec”은 “Temporal Formula”와 “Spec”으로 되어 있어야 한다. 그렇지 않다면 스펙에 ====가 하나만 있는지, 그리고 변환된 TLA+가 그 위에 있는지 확인한 다음, 두 필드를 직접 설정한다.

2. “Invariants” 상자를 클릭해 펼친다.

3. “Add”를 클릭한 다음 NoOverdrafts라는 텍스트를 입력한다.

4. 모델을 실행하거나 F11을 누른다.

실행하면 오른쪽에 에러가 뜬다:

이것이 에러 트레이스(error trace)로, 불변식(invariant)이 위반되기까지 거친 정확한 스텝(step)들을 보여 준다. 에러 트레이스는 불변식을 깊이 있게 다룰 때 좀 더 이야기하겠다.

스크래치 파일 만들기

나는 스펙 전체를 돌리지 않고 연산자(operator)의 출력만 시험해 보고 싶을 때가 많다. 그래서 “scratch”라고 부르는 별도의 스펙을 하나 둔다:

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

Eval == 0
====

이 파일은 일반적인 TLA+ 파일과 두 가지 점에서 다르다. 첫째, “What is the behavior spec”을 “Temporal formula”로 두는 대신 “no behavior spec”으로 설정한다. 둘째, “model checking results” 페이지에서 “Evaluate Constant Expression” 상자에 Eval을 넣는다.

이제 모델을 실행할 때마다 Eval의 출력이 아래쪽 “Value” 상자에 표시된다. 이 경우에는 0이 나온다. 하지만 Eval 식(expression)을 바꾸면 다른 결과가 나온다.

- Eval == 0
+ Eval == "hello world!"

이제 Eval을 실행하면 “hello world!”가 나온다.

스크래치 파일은 아주 유용하니 하나 만들어 두기를 권한다. 이 가이드에서도 가끔 다음과 같은 “식 평가(expression evaluation)” 결과를 올릴 것이다:

>>> 1+1

2

이것은 그저 Eval == 1+1로 설정했더니 출력으로 2가 나왔다는 뜻이다. 이를 이용해 여러분도 나와 같은 결과를 얻었는지 확인할 수 있다.

자, 이것으로 TLA+를 배우기 시작할 준비가 끝났다!