표준 모듈

Naturals

+ - * ^ % < > <= >=에 더해 다음을 정의한다.

Nat

{0, 1, ...} 집합(set)이다. TLC는 이 집합을 열거할 수 없지만(한정자(quantifier)나 CHOOSE에 쓰는 경우), 멤버십 검사에는 쓸 수 있다.

a..b

{a, a + 1, ..., b} 집합이다.

a \div b

내림 나눗셈: 10 \div 3 = 3.

Integers

Naturals에 있는 모든 것에 더해 다음을 정의한다.

Int

모든 정수의 집합이다. TLC는 이 집합을 열거할 수 없지만(한정자나 CHOOSE에 쓰는 경우), 멤버십 검사에는 쓸 수 있다.

-a

음수.

Sequences

PlusCal 프로시저(procedure)에 필요하다. 시퀀스(sequence)는 다른 언어의 리스트와 비슷하다. <<a, b, c>>처럼 쓰고, 원소로는 다른 어떤 값(value)이든 올 수 있다(다른 시퀀스도 포함해서). 관련된 시퀀스 절도 확인해 보자.

Seq(set)

값이 모두 set의 원소인 모든 시퀀스의 집합이다. 멤버십을 검사하는 경우라면 TLC에 전용 코드가 있어서 메모리/CPU를 많이 잡아먹지 않는다. TLC는 이 집합을 열거할 수 없지만(한정자나 CHOOSE에 쓰는 경우), 멤버십 검사에는 쓸 수 있다.

<<a>>          \in Seq({a, b})
<<a, b>>       \in Seq({a, b})
<<a, b, b, a>> \in Seq({a, b})
\* in practice, the output is a set that contains all sequences made from 'a's and 'b's,
\* so it also includes the sequence <<a, a, a, a, b, a, b>> for example. That's why it's nonenumerable.

Len(seq)

seq의 길이.

Len(<<2, 4, 6>>) = 3

Head(seq)

seq의 첫 번째 원소.

Head(<<1, 2, 3>>) = 1

Tail(seq)

seq에서 첫 번째 원소를 뺀 나머지 전부.

Tail(<<1, 2, 3>>) = <<2, 3>>

seq1 \o seq2

두 시퀀스를 이어 붙인다.

<<1>> \o <<2 , 3>> = <<1, 2, 3>>

Append(seq, e)

e를 seq의 끝에 덧붙인다. seq1 \o <<e>>와 같다.

Append(<<1, 2>>, 3) = <<1, 2, 3>>

SubSeq(seq, m, n)

seq에서 부분 시퀀스 <<s[m], s[m+1], ... , s[n]>>를 고를 때 쓴다. 인덱스는 양 끝을 포함한다. [문서에서 발췌]

SubSeq(<<7, 8, 9>>, 1, 2) = <<7, 8>>

SelectSeq(seq, Op(_))

Op를 이용한 시퀀스 필터.

IsEven(x) == x % 2
SelectSeq(<<1, 2, 3>>, IsEven) = <<2>>

FiniteSets

IsFiniteSet(set)

set이 무한 집합이 아닌지 검사한다.

IsFiniteSet({2, 5, 7}) = TRUE
IsFiniteSet(Seq({1})) = FALSE
IsFiniteSet(Nat) = FALSE

Cardinality(set)

set의 원소 개수.

Cardinality({2, 5, 7}) = 3

Bags

다중집합(multiset)이라고도 부른다. 백(bag)은 항목을 그 항목의 “개수”에 대응시키는 함수(function)다. 예를 들어 구조체(struct) [a |-> 1, b |-> 2]는 백이다. 백의 값은 양의 정수여야 한다.

IsABag(func)

func가 백인지 검사한다.

IsABag([a |-> 3, b |-> 7]) = TRUE

BagToSet(bag)

DOMAIN bag과 같다.

BagToSet([a |-> 3, b |-> 7]) = {"a", "b"}

SetToBag(set)

[x \in set |-> 1]과 같다.

SetToBag({}) = <<>>
SetToBag({"a","b"}) = [a |-> 1, b |-> 1]
SetToBag({"a", "b", "a", "a"}) = [a |-> 1, b |-> 1]

BagIn(e, bag)

e \in DOMAIN bag과 같다.

BagIn("a", [a |-> 1, b |-> 1]) = TRUE
BagIn("c", [a |-> 1, b |-> 1]) = FALSE

EmptyBag

<<>>와 같다.

EmptyBag = <<>>

bag1 (+) bag2

백 덧셈. 각 키마다 두 백에서 그 키가 가진 값을 합한 새 백을 만든다.

[a |-> 1, b |-> 3] (+) EmptyBag = [a |-> 1, b |-> 3]
[a |-> 1, b |-> 3] (+) [a |-> 1] = [a |-> 2, b |-> 3]
[a |-> 1, b |-> 3] (+) [c |-> 1] = [a |-> 1, b |-> 3, c |-> 1]

bag1 (-) bag2

백 뺄셈. bag2[e] >= bag1[e]이면 최종 백의 키에서 e가 빠진다.

\* Nothing changes:
[a |-> 1, b |-> 3] (-) EmptyBag = [a |-> 1, b |-> 3]
\* a is removed from the bag:
[a |-> 1, b |-> 3] (-) [a |-> 1] = [b |-> 3]
\* a is decreased by the amount of the second bag:
[a |-> 2, b |-> 3] (-) [a |-> 1] = [a |-> 1, b |-> 3]
\* c is not in the domain of the bag on the left, hence nothing changes:
[a |-> 1, b |-> 3] (-) [c |-> 1] = [a |-> 1, b |-> 3]

BagUnion(set)

bag1 (+) bag2 (+) ...와 같다(단, set = {bag1, bag2, ...}).

BagUnion({}) = <<>>
BagUnion({[a |-> 2]}) = [a |-> 2]
BagUnion({[a |-> 2], [b |-> 3]}) = [a |-> 2, b |-> 3]

B1 \sqsubseteq B2

DOMAIN B1의 모든 e에 대해 백 B2가 가진 e의 사본 수가 백 B1이 가진 수 이상일 때, 그리고 오직 그때만 B1 sqsubseteq B2이다. [문서에서 발췌]

[a |-> 2, b |-> 3] \sqsubseteq [b |-> 2] = FALSE
[a |-> 2, b |-> 3] \sqsubseteq [a |-> 2, b |-> 2] = FALSE
[a |-> 2, b |-> 3] \sqsubseteq [a |-> 2, b |-> 3] = TRUE
\* it doesn't matter if B2 has "c |-> 1", because has enough copies of a and b.
[a |-> 2, b |-> 3] \sqsubseteq [a |-> 2, b |-> 3, c |-> 1] = TRUE
[a |-> 2, b |-> 3] \sqsubseteq [a |-> 5, b |-> 3, c |-> 1] = TRUE

SubBag(bag)

bag의 모든 부분 백의 집합.

SubBag(EmptyBag) = {<<>>}
SubBag([a |-> 2]) = {<<>>, [a |-> 1], [a |-> 2]}

BagOfAll(Op(_), bag)

bag[e] = x이면 out[Op(e)] = x이다. 예:

b == <<1, 3, 5>>
>>> BagOfAll(LAMBDA x: x^2, b)

(1 :> 1 @@ 4 :> 3 @@ 9 :> 5)

BagCardinality(bag)

bag에 있는 모든 값의 합.

BagCardinality(EmptyBag) = 0
BagCardinality([a |-> 2]) = 2
BagCardinality([a |-> 5, b |-> 3, c |-> 1]) = 9

CopiesIn(e, bag)

e가 bag에 있으면 bag[e], 아니면 0.

CopiesIn("a", EmptyBag) = 0
CopiesIn("a", [a |-> 5, b |-> 3]) = 5

TLC

PlusCal assert에 필요하다. TLC에 있는 연산자(operator) 중 상당수는 참조 투명성(referential transparency) 같은 TLA+의 핵심 가정을 깨뜨린다. 조심해서 쓰자!

a :> b

함수 [x \in {a} |-> b].

func1 @@ func2

함수 병합. 두 함수가 같은 키를 공유하면 func1의 값을 쓴다(결코 func2의 값이 아니다).

Permutations(set)

set의 순열 역할을 하는 모든 함수의 집합. 예:

>>> Permutations({"a", "b"})

{[b |-> "b", a |-> "a"],
 [b |-> "a", a |-> "b"]}

SortSeq(seq, Op(_, _))

비교자 Op로 시퀀스를 정렬한다.

ToString(val)

문자열 변환.

JavaTime

현재 에포크 시간.

Print(val, out)

ToString(val)을 출력하고, 식(expression)으로서는 out으로 평가된다.

PrintT(val)

Print(val, TRUE)와 같다.

Any

x \in Any는 어떤 값 x에 대해서도 성립한다. Spec의 일부로 쓰지는 말아야 하지만, 속성(property)을 모델링할 때는 이따금 쓸모가 있다.

Assert(bool, errmsg)

bool이 거짓이면 errmsg와 함께 모델 체킹(model checking)을 종료한다. 그렇지 않으면 TRUE로 평가된다.

RandomElement(set)

무작위로 set에서 원소 하나를 뽑는다. 실행할 때마다 값이 달라질 수 있다!

TLCEval(v)

식 v를 평가하고 그 결과를 캐시한다. 재귀 정의의 속도를 높이는 데 쓸 수 있다.

TLCGet(val)

val은 정수일 수도 있고 문자열일 수도 있다. 정수면 대응하는 TLCSet의 값을 가져온다. 문자열이면 현재 모델 실행의 통계를 가져온다. 유효한 문자열은 다음과 같다.

• “queue”

• “generated”

• “distinct”

• “duration”: 모델 체킹을 시작한 뒤로 흐른 초 수

• “level”: 현재 행동(behavior)의 길이

• “diameter”: 가장 긴 전역 행동의 길이

• “stats”: 모든 전역 통계(“level”을 뺀 전부)를 구조체로 담은 것.

TLCGet("level")은 경계 없는 모델(unbound model)에 경계를 두는 데 쓸 수 있다.

TLCSet(i, val)

TLCGet(i)의 값을 설정한다. i는 양의 정수여야 한다. TLCSet은 같은 스텝(step) 안에서 여러 번 호출할 수 있다.

노트

각 TLC 워커 스레드(thread)는 TLCGet(i) 값에 대해 저마다 별도의 “캐시”를 가진다. 그러므로 한 스텝을 넘어 유지되는 정보를 프로파일링하는 데 TLCSet을 쓰는 것은 대체로 권하지 않는다.

하지만 초기 상태(initial state)에서 평가된 TLCSet 문은 모든 워커에 확실히 전파된다.

Json

ToJson(val)

val을 JSON 문자열로 변환한다. 집합과 시퀀스는 배열로, 함수는 문자열 키를 가진 객체로 인코딩된다.

>>> ToJson(1..3)
"[1,2,3]"

>>> ToJson([x \in 0..2 |-> x^2])

"{\"0\":0,\"1\":1,\"2\":4}"

인자가 여럿인 함수는 TLA+ 튜플(tuple) 표기법을 쓴 키로 인코딩된다.

>>> ToJson([p, q \in BOOLEAN |-> p => q])

"{\"<<FALSE, FALSE>>\":true,
  \"<<TRUE, FALSE>>\":false,
  \* ...

JsonSerialize(absoluteFilename, value)

value를 JSON 객체로 파일에 내보낸다.

JsonDeserialize(absoluteFilename)

파일에서 JSON 객체를 가져온다.

Randomization

이 모듈은 집합의 의사 난수 부분집합을 고르는 연산자를 정의한다. 이 모듈을 쓰면 TLC는 가능한 모든 상태(state)를 검사하지는 않는다. 예를 들어 다음 스펙(spec)을 보자.

EXTENDS Integers, TLC, Randomization
VARIABLE x

Init ==
    /\ x = 0

Next ==
    \/ /\ x = 0
       /\ x' \in {1, 2, 3}
    \/ /\ PrintT(x)
       /\ UNCHANGED x

\* Magic magic magic
Spec == Init /\ [][Next]_x

이 스펙을 실행하면 숫자 {0, 1, 2, 3}을 출력한다. {1, 2, 3}을 RandomSubset(2, {1, 2, 3})으로 바꾸면 세 숫자 중 두 개만 출력하며, 어느 두 개인지는 실행할 때마다 바뀔 수 있다. 그래서 Randomization은 최적화에 유용하지만, 조심해서 써야 한다.

RandomSubset(k, S)

S의 크기 k짜리 무작위 부분집합을 반환한다.

RandomSubset(1, {"a"}) = {"a"}
\* Running multiple times will yield different subsets
RandomSubset(2, {"a", "b", "c"}) = {"b", "c"}
RandomSubset(2, {"a", "b", "c"}) = {"a", "c"}

RandomSetOfSubsets(k, n, S)

S의 무작위 부분집합 k개를 고르는데, 각 무작위 부분집합의 원소는 평균적으로 n개다. 이 과정에서 중복된 부분집합이 생길 수 있으므로, 이 연산자는 k개보다 적은 부분집합을 반환할 수도 있다. 공집합을 반환할 수도 있다.

RandomSetOfSubsets(1, 1, {"a"}) = {{"a"}}

\* Each element has a 3-in-5 chance of appearing in each subset
RandomSetOfSubsets(2, 3, {"a", "b", "c", "d", "e"}) = {{"a", "d", "c"}, {"a", "b", "e", "c"}}
RandomSetOfSubsets(2, 3, {"a", "b", "c", "d", "e"}) = {{"a", "e"}, {"d", "e", "b", "c"}}

\* Fewer than 4 results because it generated a duplicate
RandomSetOfSubsets(4, 1, {"a", "b"}) = {{}, {"b"}, {"a", "b"}}

TestRandomSetOfSubsets(k, n, S)

RandomSetOfSubsets(k, n, s)를 다섯 번 호출하고, 매번 반환된 고유한 집합의 개수를 반환한다.

TestRandomSetOfSubsets(1, 1, {"a"}) = <<1, 1, 1, 1, 1>>
\* Different executions will yield different results:
TestRandomSetOfSubsets(3, 4, {"a", "b", "c", "d", "e"}) = <<3, 3, 2, 2, 2>>