툴박스 사용하기

에러 트레이스 정보

간단히 표시를 달아 보았다:

1. 이걸 클릭하면 에러 트레이스를 TLA+ 구조체(struct)로 복사한다. 툴박스 수석 개발자가 JSON으로도 복사하는 기능을 지금 만들고 있지만, 아직 완성되지는 않았다.

2. 이걸 클릭하면 에러 트레이스에서 변수를 걸러 낼 수 있다(보조 변수 같은 것). 각 스텝에서 바뀌지 않은 변수를 전부 숨길 수도 있다.

3. 트레이스 스텝을 전부 펼치고 접는다. 액션(action) 흐름을 빠르게 훑어보기에 좋다.

4. 이걸 켜 두면, 액션 줄을 클릭할 때 스펙에서 그 액션이 있는 곳으로 자동으로 이동한다.

상태(state)와 값(value)을 클릭해서 할 수 있는 일도 있다:

• 변수를 Alt-클릭하면 트레이스에서 숨겨진다. 다시 보이게 하려면 필터 버튼을 다시 클릭한다.

• 액션을 더블클릭하면 해당하는 스펙 코드로 이동한다. Ctrl-더블클릭하면 해당하는 PlusCal 레이블(label)로 이동한다.

• 액션을 우클릭하면 그 액션의 상태를 초기 상태(initial state)로 삼아 같은 모델(model)을 다시 돌릴 수 있다.

트레이스 탐색기

에러 패널의 마지막이자 가장 복잡한 기능은 “Error-Trace Exploration” 창이다. 이 창에 추가한 식(expression)은 무엇이든 에러 트레이스의 모든 상태에서 평가되고, 그 결과가 표시된다. 예를 들어 prod == x * y를 추가하고 Explore 버튼을 클릭하면, 에러 트레이스에 prod가 나타난다.

원래 트레이스로 돌아가려면 Restore를 클릭한다.

탐색기는 아주 강력한 기능이다. 탐색기에 추가한 연산자(operator)는 다른 탐색기 식에서도 쓸 수 있으니, prod > x도 올바른 식이다. 게다가 프라임 값(primed value)을 넣을 수도 있다! 기억하자, x'은 다음 상태에서의 x 값이다. 연산자도 마찬가지다: prod' = x' * y'.

마지막으로, 액션 전체를 테스트할 수도 있다. 액션은 다음 상태를 정확하게 기술하면 참이다.

트레이스 탐색기(Trace Explorer)는 스펙을 디버깅하는 강력한 도구이니, 시간을 좀 들여 익숙해지기를 권한다.

추가 스펙 옵션(Additional Spec Options)

상태 제약(State Constraint)

TLC는 모델의 상태 중 상태 제약을 만족하지 않는 것은 모두 무시한다. 예를 들어 다음 스펙을 보자:

EXTENDS Integers
VARIABLE x

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

보통은 이 스펙을 INVARIANT Inv 설정으로 돌리면 실패한다. 하지만 상태 제약 x < 5를 추가하면, 상태 6개를 찾고 통과한다. x >= 5인 상태는 버려지고, 그 상태들로부터는 새 상태를 찾지 않는다.

다만 상태가 버려지기 전에 불변식(invariant)은 먼저 검사된다. 그래서 상태 제약을 x < 10으로 바꾸면 실패한다. 상태 제약은 버려진 상태로부터 TLC가 새 상태를 탐색하는 것만 막는다.

상태 제약이 켜져 있으면 라이브니스(liveness) 불변식은 검사할 수 없다.

팁

상태 제약은 경계 없는 모델(unbound model)에 경계를 두는 좋은 방법이다.

액션 제약(Action Constraint)

상태 제약과 비슷하지만, 액션이라는 점이 다르다. 위 스펙에서 x' > x라고 쓰면 x가 증가하는 상태만 탐색한다.

정의 오버라이드(Definition Override)

여기서는 일부 연산자의 정의를 직접 만든 정의로 바꿀 수 있다. 예를 들어 정의 오버라이드 Int <- 1..10을 추가할 수 있다. 이 기능은 변수가 “아무 정수”로 시작한다고 말하고 싶지만 모델 체킹(model checking)을 위해서는 유한 집합(set)으로 제한하고 싶은 사람들이 주로 쓴다.

추가 TLC 옵션(Additional TLC Options)

워커 스레드(Worker threads)

TLC 검사를 몇 개의 워커에 나눠 맡길지 정한다. 기본값은 코어 수다. 스레드(thread)를 더 적게 쓰면 (일반적으로) TLC가 더 오래 걸리고 CPU 자원을 덜 쓴다. 스레드를 하나만 쓰면 실행할 때마다 결정적인 모델 체킹이 보장되는데, print 문을 쓰고 있다면 유용할 수 있다.

메모리 비율(Fraction of memory)

TLC가 검사에 쓸 수 있는 메모리 양을 정한다. 모델이 이 한도를 넘으면 TLC는 찾은 상태를 디스크에 쓰기 시작하고, 그러면 모델 체킹 시간이 크게 늘어난다.

TLC는 모델 체킹을 시작하기 전에 그 메모리를 전부 미리 할당하고, 끝난 뒤에 해제해야 한다는 점에 주의하자. 모델이 충분히 작고 컴퓨터가 충분히 크면, 할당 시간이 모델 실행 시간보다 길어질 수도 있다!

뷰(View)

이건 흑마법이라 아주 조심해서 다뤄야 한다. 보통 TLA+는 모든 변수를 써서 상태를 구별한다. VIEW 식을 정의하면, 대신 그 식이 TLC가 쓰는 기준이 된다.

예를 들어 변수가 x와 y 두 개 있다고 하자. 기본 VIEW는 <<x, y>>일 것이다. 대신 VIEW x라고 쓰면, x가 같은 두 상태는 y 값과 상관없이 같은 상태로 취급된다.

현명하게 쓰면 모델 최적화에 유용할 수 있다. 잘못 쓰면 스펙을 완전히 망가뜨릴 수 있다.

깊이 우선(Depth-first)

보통 TLC는 너비 우선 탐색을 한다. 이 옵션은 대신 깊이 우선 탐색을 하도록 바꾼다. 불변식 위반이 흔하지만 행동(behavior)의 깊은 곳에서 일어날 것으로 예상될 때 유용하다. 검사할 최대 깊이를 지정할 수 있으므로, 경계 없는 모델의 일부를 검사하는 좋은 방법이기도 하다.

시뮬레이션 모드(Simulation Mode)

이 모드에서 TLC는 최대 트레이스 길이까지 무작위 트레이스를 생성한다. 라이브니스는 검사하지 않는다.

시뮬레이션 모드 실행은 상태 공간(state space)을 빠짐없이 검사한 뒤에도 절대 멈추지 않는다. 직접 끝내야 한다.

프로파일링(Profiling)

프로파일링은 두 종류가 있다. “Action Enablement”는 각 액션이 얼마나 자주 호출됐는지 기록한다. 이 결과는 모델 체킹 결과의 통계(statistics) 항목 아래에 표시된다. 이걸로 한 번도 활성화되지(enabled) 않는 액션이 있는지 확인할 수 있는데, 그런 액션이 있다면 스펙에 버그가 있는 것이다.

“On”은 전체 프로파일링을 한다: 각 연산자가 얼마나 자주 호출되는지, 식의 각 분기가 얼마나 자주 쓰였는지, 각 연산자를 호출하는 데 비용이 얼마나 들었는지. 이걸 모델 최적화에 활용할 수 있다.

(모델 체킹 최적화에 관한 주제를 쓸 계획이다. 그때가 되면 프로파일링을 더 자세히 다뤄 보겠다.)

상태 그래프 시각화(Visualize state graph)

graphviz가 필요하다. 모델 체킹이 끝난 뒤 방향 그래프를 생성한다. 작은 상태 공간을 이해하는 데 유용할 수 있다. 하지만 큰 상태 공간이라면 출력을 직접 덤프해서 그래프를 가지치기하거나 Gephi 같은 도구에 불러오는 편이 낫다.

TLC 커맨드 라인 매개변수(TLC command-line parameters)

툴박스 GUI에 노출되지 않은 추가 커맨드 라인 매개변수를 TLC에 넘길 수 있다. 무엇을 넘길 수 있는지는 여기를 참고하라.