보조 변수

히스토리 변수

이미 일어난 일을 나타내는 변수다. Q_was_true가 바로 히스토리 변수(history variable)다. 히스토리 변수가 한 번 설정된 뒤로는 바뀌지 않는다는 것을 확인하고 싶다면, 이를 액션 속성(action property)으로 만들면 된다:

Prop ==
  [][Q_was_true => UNCHANGED Q_was_true]_Q_was_true

히스토리 변수로 시스템에 더는 남아 있지 않은 과거 정보를 추적할 수도 있다. 예를 들어 클라이언트가 데이터베이스에 질의하는데, 요청을 처리하는 도중에 데이터베이스가 갱신될 수 있다고 해 보자. 이때 aux_client_request_value라는 변수를 추가해 클라이언트가 요청을 보내는 즉시 갱신되게 하면, 데이터베이스 값이 갱신되더라도 요청 시점에 그 값이 무엇이었는지에 대한 정보를 잃지 않는다.

에러 변수

either 분기가 있는 PlusCal 스펙을 작성한다고 해 보자:

either
  \* path 1
or
  \* path 2
or
  \* ...

에러 트레이스(error trace)에서는 어느 분기를 탔는지 알아보기 어려울 수 있다. 상태 변화를 보고 추론해야 하기 때문이다. 이를 피하려고 레이블(label)을 잔뜩 붙이는 사람들도 있다:

either
  Path1:
    \* ...
or
  Path2:
    \* ...
or
  \* ...

그러면 pc를 보고 어느 경로를 탔는지 알 수 있다. 하지만 이렇게 하면 스펙에 여분의 동시성(concurrency)이 잔뜩 더해진다 — 잘해야 상태 공간(state space)이 폭발하고, 최악의 경우에는 스펙의 의미론(semantics)이 바뀐다!

우리가 원하는 것은 스펙의 의미론을 바꾸지 않으면서 에러 트레이스를 풍부하게 만드는 것이다. 보조 변수가 활약하기 딱 좋은 자리다.

either
  aux_branch := "Path1";
    \* ...
or
  aux_branch := "Path2";
    \* ...
or
  \* ...

또 다른 흔한 용도는 언제 무슨 일이 일어났는지 이력 로그를 남기는 것이다:

\E w \in Workers:
  /\ \/ Action1(w)
     \/ Action2(w)
     \/ Action3(w)
  /\ aux_log' = Append(aux_log, w)

경계 변수

경계 변수(bounding variable)는 이미 우리의 reader_writer 스펙에서 하나 본 적이 있다. 어떤 프로세스도 큐에 끝없이 쓰게 두지 않고, 항상 최대 N개의 메시지만 쓰게 했다. 끝없이 쓸 수 있다면 경계 없는(unbound) 상태 공간이 되어 버리기 때문이다!

내가 즐겨 쓰는 경계 변수 활용법 하나는 시스템에 작은 오류를 끼워 넣는 것이다. 메시지 유실을 모델링하고 싶다면 이렇게 쓴다.

either
  queue := Append(queue, msg);
or
  await aux_drops_left > 0;
  aux_drops_left := aux_drops_left - 1;
end either;

(유한 상태 기계 장에 either await 패턴의 동작 방식이 설명되어 있다.)

그러면 유실이 전혀 없는 경우나 딱 한 번만 유실되는 경우로 시스템을 테스트할 수 있다. 시스템이 메시지를 하나도 빠짐없이 전부 유실할 수는 없다.

예언 변수

예언 변수(prophecy variable)는 미래에 일어날 일을 미리 정해 둔다. 사실상 비결정성(nondeterminism)을 스펙의 더 앞쪽으로 끌어당기는 방법이다. 예를 들어 계산기 스펙에서 나는 숫자를 비결정적으로 더하는 것을 이렇게 표현했다:

Digits == 0..9

(* --algorithm calculator
variables
  i = 0;
  sum = 0;

begin
  Calculator:
    while i < NumInputs do
      with x \in Digits do
          \* Add
          sum := sum + x;
      end with;
      i := i + 1;
    end while;

초기 상태는 하나뿐이지만, 루프를 한 번 돌 때마다 각 상태가 10갈래로 갈라진다. 대신 이렇게 쓸 수도 있다:

variables
  i = 1;
  sum = 0;
  aux_proph_digits \in [1..NumInputs -> Digits];

begin
  Calculator:
    while i <= NumInputs do
      sum := sum + aux_proph_digits[i];
      i := i + 1;
    end while;

이제 초기 상태는 더 많아졌지만, 각 초기 상태에서 가능한 행동은 하나뿐이다.

예언 값은 꽤 드물게 쓰이는 편이다. 주로 정제(refinement)를 만드는 데 쓰인다.