경계 없는 모델 다루기

이 스펙은 실행하지 마라:

---- MODULE Unbound ----
EXTENDS Integers

(*--algorithm seriously_dont_run_this
variable x = 0
begin
  while TRUE do
    x := x + 1;
  end while;
end algorithm; *)

모델 체커(model checker)는 가능한 모든 서로 다른 상태(state)를 찾아내는 방식으로 동작한다. 이 스펙에는 서로 다른 상태가 무한히 많다. x가 영원히 계속 증가할 수 있기 때문이다. 그러니 이 스펙은 모델 체킹이 절대 끝나지 않는다. 이런 모델을 경계 없는 모델(unbound model)이라고 한다.

경계 없는 모델은 보통 다음 두 곳 중 하나에서 생긴다:

위에서 본 것처럼, 스펙이 정숫값을 계속 증가시킨다
스펙이 시퀀스(sequence)에 원소를 계속 덧붙인다.

경계가 없을 수 있는 것이 최상위 값만은 아니라는 점에 유의하라. 타입이 [a: Int, b: BOOL]인 구조체(struct)가 있다면, 그 구조체는 a 키 쪽에서 경계가 없을 수 있다.

팁

모델에 경계가 없는지 알아채는 좋은 방법이 있다: 예상했던 것보다 상태를 훨씬 더 많이 만들어 내고 있는가? 지름(diameter)이 예상보다 훨씬 빠르게 늘어나고 있는가? 경계 있는 모델은 대부분 지름이 천천히 늘어나지만, 경계 없는 모델은 새로운 상태의 사슬을 빠르게 찾아낸다.

모델 불변식

경계 없는 모델을 탐지하는 가장 쉬운 방법은 스펙에 ModelInvariant를 추가하는 것이다. 모델 불변식(model invariant)은 타입 불변식(type invariant)과 비슷하지만, 모든 변수를 유한 집합(finite set)으로 제한한다는 점이 다르다.

CONSTANT MaxX

TypeInvariant == x \in Int
ModelInvariant == x \in 0..MaxX

ModelInvariant => TypeInvariant임에 주목하라: 모델 불변식을 깨는 상태가 타입상으로는 올바를 수도 있지만, 타입 에러는 모델 에러이기도 하다. 또한 ModelInvariant => Bound이다. 경계 있는 모델도 모델 불변식에서 괜한 실패를 낼 수는 있지만, 경계 없는 모델은 반드시 실패한다.

모델에 경계 두기

대부분의 경우 경계 없는 모델은 스펙 에러다: 어딘가에서 검사를 빠뜨렸고, 모델 체커가 그 틈을 파고든 것이다. 대개는 버그를 고치거나 스펙을 수정하는 것만으로 모델에 다시 경계를 세울 수 있다.

하지만 때로는 스펙에 새로운 가정을 추가하지 않고서는 이렇게 하기가 쉽지 않다. 이럴 때는 상태 제약(state constraint)을 추가하면 된다.

ModelConstraint == x \in 0..MaxInt

이것은 모델 불변식과 똑같지만, 결정적인 차이가 하나 있다: 이것을 불변식으로 사용하면, 모델 체커는 위반하는 상태를 에러로 띄우는 대신 거부한다. [역주: 문맥상 「불변식이 아니라 상태 제약(state constraint)으로 사용하면」의 뜻이다. 불변식으로 쓰면 위반 상태는 에러로 보고된다.] 스펙의 상태 공간(state space)은 여전히 무한하지만, 모델 체커는 그중 유한한 부분만 탐색한다. 이렇게 해서 모델에 경계가 생긴다.

경고

시간 속성(temporal property)도 함께 검사하고 있다면 이렇게 하지 마라! 사실상 행동(behavior)의 일부를 “잘라 내는” 셈이라, 모델 체커가 라이브니스(liveness)를 평가하는 데 쓸 행동 전체를 갖지 못하게 된다.

TLCGet

TLC 모듈에는 TLCGet이라는 특별한 연산자(operator)가 있다. 쓰임새가 몇 가지 있지만, 우리에게 가장 중요한 것은 생성된 상태의 수나 현재 트레이스(trace)의 길이 같은 런타임 통계를 얻을 수 있다는 점이다. 이것은 내가 경계 없는 모델의 상태 공간을 제한할 때 가장 좋아하는 방법이기도 하다:

ModelConstraint == TLCGet("level") < 9

이 방법이 변수의 값을 제약하는 것보다 나은 점은 무엇일까? 변수가 많으면, 각 변수의 경계를 얼마로 잡아야 할지 예측하기 어려울 수 있다. 적어도 처음에는, 변수는 전부 경계 없이 두고 모델 체커가 밟을 수 있는 스텝(step) 수만 제한하는 편이 훨씬 쉽다.