상태 머신으로 TLA+ 명세 합성하기
원문은 Hillel Wayne님이 에 게재했습니다. 이 블로그 구독하기
작년 한 클라이언트가 내게 문제를 하나 들고 왔다. 더 큰 시스템의 일부로 두 개의 큰 TLA+ 명세를 합성하고 싶다는 것이었다. 보통은 이렇게 하면 안 되고 두 시스템을 모두 하드코딩한 하나의 큰 명세를 작성해야 하지만, 이 명세들은 엄청나게 컸고 각각 수많은 내부 불변식을 가지고 있었다. 이들은 두 명세를 독립적으로 개발한 뒤 최소한의 오버헤드로 통합할 방법이 필요했다.
이것이 내가 고안해 낸 방법이다. 경고: 이 해결책은 복잡하며 고급 TLA+ 사용자를 대상으로 한다. 훨씬(훨씬) 더 부드러운 입문서를 원한다면 내 웹사이트 learntla를 확인해 보라.
예제
동기 부여가 되는 시스템부터 시작해 보자. Worker가 Server에 인증 요청을 보낸다. 비밀번호가 서버의 내부 비밀번호와 일치하면 서버는 “valid”로 응답하고, 그렇지 않으면 “invalid”로 응답한다. Worker가 응답으로 “invalid”를 받으면 오류 상태가 된다. Worker는 그 상태에서 재시도하여 새로운 인증 요청을 제출할 수 있다.
Worker와 서버는 요청/응답을 통해 상태를 공유한다. 추가적인 복잡성을 위해 서버에 Worker에게는 보이지 않는 요청 로그 형태의 내부 상태를 추가하겠다.
이 예제를 통해 합성의 문제점과 나의 해결책을 보여줄 수 있다(다만 이 예제는 그럴 만한 가치를 보여주기엔 조금 단순하다고 해두겠다).
합성의 문제점
우리가 원하는 것은 합성이 가능한 한 단순하고 고통스럽지 않은 것이다. 우리 명세가 WorkerSpec과 ServerSpec이라면 가장 쉬운 합성은 그냥 다음과 같을 것이다.
CombinedSpec == WorkerSpec /\ ServerSpec이 문제에 대해서는 여기에서 자세히 다루지만, 요점은 ServerSpec과 WorkerSpec이 “일반적인” 명세라면 공유 변수에 서로 모순되는 제약을 가하게 된다는 것이다.
예를 들어 WorkerSpec은 서버 응답을 읽겠지만 수정하지는 않을 가능성이 높다. 따라서 합성과 독립적으로 WorkerSpec을 실행하려면 응답이 절대 변하지 않는다고 말해야 하는데, 이는 우리가 그것을 변경할 수 없다고 말하는 것과 같고, 그러면 ServerSpec이 응답을 보내는 것이 불가능해진다!
이를 우회하는 일반적인 방법은 WorkerSpec과 ServerSpec을 모두 액션들의 모음으로 분해한 뒤, 서로 모순되지 않도록 신중하게 다시 꿰매는 것이다. 말 그대로 들리는 만큼이나 복잡하다. 두 명세를 합성하는 일이 처음부터 새로 작성하는 것만큼 많은 작업이 될 수 있다.
그래서 더 나은 방법을 찾으려는 것이다.
핵심 아이디어
우리가 해야 할 일은 세계의 일부를 나타내도록 의도된 명세를 작성한 뒤, 이를 “전체 세계” 메인 명세에 통합하는 것이다. 이를 위해 TLA+의 가장 강력한 기능 중 하나를 사용할 것이다. x'를 이용해 x의 다음 값을 할당하는 동시에 다음 값이 될 수 있는 것을 제약할 수 있다는 점이다. 예를 들어 다음과 같다고 하자.
VARIABLE x, y
Foo ==
/\ x' \in {0, 1}
/\ y' \in {0, 1}
Bar == x' < y'
Next == Foo /\ BarTLC가 Next를 평가할 때, Foo에 있는 x'와 y'를 할당으로 읽는다. 가능한 할당이 네 가지이므로 모델 체커는 이를 모두 평가한다.
그런 다음 x'와 y'가 이미 선택되었으므로 TLC는 Bar의 문장을 제약으로 읽는다. 가능한 할당 중 세 가지는 그 제약을 위반하므로 TLC는 그 가능성들을 제거하고, 유일한 다음 상태만 남게 된다.
이는 명세 Q가 두 명세 X와 Y를 가져와 서로에 대해 제약할 수 있음을 의미한다. X에 x_log를 증가시키는 액션 Inc가 있을 수 있고, Q는 Inc가 y_flag가 참일 때만 일어날 수 있다고 말할 수 있다. 마찬가지로 Q는 하나의 할당이 다른 할당을 트리거하도록 만들 수도 있다.
Inc ==
/\ x_log' = x_log + 1
Sync ==
IF ~y_flag /\ y_flag'
THEN Inc
ELSE TRUE
Next == (X!Next \/ Y!Next) /\ Sync이제 y_flag를 true로 바꾸면 x_log의 증가가 강제된다. Q는 하나의 명세를 이용해 시스템에 부수 효과를 일으키고 있는 것이다.
이건 그저 상태 머신일 뿐이다! 전이에 대한 제약은 그저 가드 절(guard clause)이고, 전이에 대한 할당은 그저 효과(effect)일 뿐이다. 이들은 상태 머신이 알지 못하는 다른 명세들에 강제될 수 있다.
이 아이디어를 실제로 동작하게 만드는 방법은 다음과 같다.
- 핵심 컴포넌트의 모든 고수준 상태 전이에 대한 추상 상태 머신을 작성한다
- 다른 컴포넌트들을 다음 상태를 완전히 기술하지 않는 “열린(open)” 명세로 작성한다.
- 정제(refine)를 통해 핵심 컴포넌트를 메인 명세로 만들고, 상태 전이에 가드와 부수 효과를 추가하는
Sync액션을 넣는다.
해결책
이를 세 개의 별도 명세로 모델링하겠다. workerSM.tla, server.tla, 그리고 system.tla다.
상태 머신
전체 시스템이 Worker의 상태 머신을 중심으로 하므로 workerSM.tla부터 시작하자. 이는 Worker가 상태를 전이할 때 무슨 일이 일어나는지를 나타내지 않고, 단지 전이가 무엇인지만 나타낸다.
------------------- MODULE workerSM -------------------
EXTENDS Integers
VARIABLES state
Transitions == {
[from |-> "init", to |-> "ready"]
, [from |-> "ready", to |-> "requesting"]
, [from |-> "requesting", to |-> "done"]
, [from |-> "requesting", to |-> "error"]
, [from |-> "error", to |-> "ready"]
}
Init == state = "init"
Valid(t) == state = t.from
ValidTransitions == {t \in Transitions: Valid(t)}
ValidOutcomes == {t.to : t \in ValidTransitions}
Done ==
state = "done"
Next ==
\E t \in ValidOutcomes:
state' = t
Fairness ==
/\ WF_state(Next)
/\ SF_state(state' = "done")
Spec == Init /\ [][Next]_state /\ Fairness
Liveness == <>Done
=========================================================Transitions는 유효한 전이들의 집합을 나타낸다. 세 개의 Valid- 연산자는 그저 헬퍼일 뿐이다. 이들을 추가하는 것은 좋은 관행이다. 대부분의 TLA+ 명세는 헬퍼가 충분하지 않다.
Fairness 제약은 조금 복잡하지만, 말하고자 하는 바는 우리가 requesting에서 error로 항상 전이할 수는 없다는 것이다. 그곳에 충분히 자주 도달하면 결국 대신 done으로 전이하게 된다.
그 외에 이 명세는 전이에 어떤 조건도 두지 않는다. done으로 가기 위해 “무언가를 할” 필요가 없다. 그 역할은 system.tla가 담당한다.
cfg 보기
이를 이용해 Worker를 직접 테스트했다.
SPECIFICATION Spec
PROPERTY Liveness
CHECK_DEADLOCK FALSE테스트를 통과하며, 이는 이 명세가 <>Done을 보장한다는 의미다.
다음은 Worker와 통합할 외부 컴포넌트다.
서버
------------------- MODULE server -------------------
CONSTANTS Password, NULL
VARIABLE req, resp, log
internal == <<log>> \* (a)
external == <<req, resp>> \* (a)
vars == <<external, internal>> \* (a)
Init ==
/\ req = NULL
/\ resp = NULL
/\ log = {}
CheckRequest ==
/\ req # NULL
/\ log' = log \union {req}
/\ IF req = Password THEN
resp' = "valid"
ELSE
resp' = "invalid"
/\ req' = NULL
Next == \* (b)
CheckRequest
Spec == Init /\ [][Next]_internal \* (c)
====이 명세에서는 세 가지 특이한 일을 하고 있다. 첫째, 변수를 internal과 external 변수로 나눴다 (a). external 변수는 합성된 명세의 다른 부분과 공유되는 상태를 나타내고, internal은 server의 속성에만 해당한다. 여기서는 서버에 대한 요청을 req로, 응답을 resp로 나타낸다.
둘째, 이 명세는 자명하게 교착 상태(deadlock)에 빠진다 (b). Next는 CheckRequest 액션만 포함하고, CheckRequest는 req가 null이 아닐 때만 활성화되지만, 명세 안에서는 어떤 것도 req를 null이 아닌 값으로 만들지 않는다. 이 명세는 “자기 완결적(self-contained)”이지 않으며, 의미 있으려면 다른 명세에 의해 사용되어야 한다.
셋째, Spec은 internal 변수에 대해서만 stuttering invariant하다. 이는 [][Next]_vars 대신 [][Next]_internal이라고 쓰는 것으로 이루어진다 (c). 가장 놓치기 쉬운 부분이지만, 앞으로 명세 합성과 명세 정제를 모두 더 쉽게 만들어 줄 것이다.
이제 서버와 Worker를 합쳐 보자.
시스템
이 부분이 단연 가장 복잡하다. 전체 명세부터 시작하고, 그다음 가장 중요한 부분들을 나눠서 살펴보자.
시스템 명세
---- MODULE system ----
EXTENDS TLC, Integers, Sequences
CONSTANT NULL
VARIABLES ws \* worker state
, server_req \* requests to server
, server_resp \* server response
, server_log \* log (internal to server)
Strings == {"a", "b", "c"}
comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>
Worker == INSTANCE workerSM WITH state <- ws
Server == INSTANCE server WITH
req <- server_req,
resp <- server_resp,
log <- server_log,
Password <- "a"
Sync ==
LET i == <<ws, ws'>> IN
/\ CASE
i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
/\ server_req' = x
/\ server_resp' = NULL
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars
[] i = <<"requesting", "done">> ->
/\ server_resp = "valid"
/\ UNCHANGED comm_vars
[] OTHER -> UNCHANGED comm_vars
Init ==
/\ Worker!Init
/\ Server!Init
Done == \* No deadlock on finish
/\ Worker!Done
/\ UNCHANGED vars
ServerNext ==
/\ Server!Next
/\ UNCHANGED ws
WorkerNext ==
/\ Worker!Next
/\ Sync
/\ UNCHANGED server_log
Next ==
\/ WorkerNext
\/ ServerNext
\/ Done
Fairness ==
/\ WF_vars(Next)
Spec == Init /\ [][Next]_vars /\ Fairness
RefinesServer == Server!Spec
RefinesWorker == Worker!Spec
====VARIABLES ws \* worker state
, server_req \* requests to server
, server_resp \* server response
, server_log \* log (internal to server)
Strings == {"a", "b", "c"}
comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>나는 vars를 목적과 명세별로 그룹화하는 것을 좋아한다. 서버와 Worker가 모두 server_req와 _resp를 사용하므로 이들을 별도의 comm_vars 그룹으로 묶었다.
Worker == INSTANCE workerSM WITH state <- ws
Server == INSTANCE server WITH
req <- server_req,
resp <- server_resp,
log <- server_log,
Password <- "a"교육상의 편의를 위해 서버의 Password 상수를 하드코딩했다. NULL 상수는 system.tla와 server.tla에서 이름이 같으므로 자동으로 전파되어 따로 인스턴스화할 필요가 없다.
Sync ==
\* See next section
Init ==
/\ Worker!Init
/\ Server!Init
ServerNext ==
/\ Server!Next
/\ UNCHANGED ws
WorkerNext ==
/\ Worker!Next
/\ Sync
/\ UNCHANGED server_log
Done == \* No deadlock on finish
/\ Worker!Done
/\ UNCHANGED vars
Next ==
\/ WorkerNext
\/ ServerNext
\/ DoneInit은 각 변수를 설정하기 위해Worker!Init과Server!Init에 그냥 위임한다. 여기서는 그들이 변수를 공유하지 않으므로 쉽다. 만약 둘 다 사용하는 무언가가 있거나system에 추가적인 보조 변수가 필요하다면 여기서 별도로 처리할 것이다.ServerNext는 그저 “서버가 자체 상태 업데이트를 처리할 수 있다”고 말하지만,ws의 stuttering을 고려한다(모든 변수가 매 단계마다 값을 할당받아야 하기 때문이다). 서버는 시스템에서 독립적으로 동작하며 그 행위는 Worker에 동기적으로 의존하지 않는다. 컴포넌트를 분리해 두는 것이 합성 시 항상 가능한 것은 아니지만, 가능할 때는 더 편리하다.WorkerNext도 마찬가지다.ServerNext와 독립적으로 동작한다. 하지만 “시스템”이 역할을 하기 시작하는 지점이 바로Sync다.
Sync
Sync가 흥미로워지는 지점이다.
Sync ==
LET i == <<ws, ws'>> IN
CASE
i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
server_req' = x
/\ server_resp' = NULL
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars
[] i = <<"requesting", "done">> ->
/\ server_resp = "valid"
/\ UNCHANGED comm_vars
[] OTHER -> UNCHANGED comm_vars앞서 설명한 내용을 다시 정리하면, primed 변수는 할당된 뒤 다른 식에서 사용될 수 있다. 이는 한 액션에서 전이를 시도한 뒤, 이후 액션에서 그 전이가 유효한지 검사할 수 있음을 의미한다. 이것이 이 모든 것을 동작하게 만드는 핵심이다. 이것이 없다면 가드와 부수 효과를 전이와 같은 액션 안에 넣어야 할 것이다. 예를 들어 다음 줄에서:
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars우리는 requesting -> error 전이가 서버 응답이 “invalid”일 때만 가능하도록 제약하고 있다. 이는 Server!Next가 비밀번호를 거부했을 때만 가능하다. 하지만 우리 Worker는 이를 알 필요가 없다. 우리는 이들을 독립적으로 개발하고 Sync가 그 행위를 올바르게 합성하도록 믿으면 된다.
이를 이용해 시스템에 효과를 발생시킬 수도 있다.
[] i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
server_req' = x
/\ server_resp' = NULL이는 ready -> requesting 전이가 요청을 트리거하고(남아 있는 응답은 지우면서) 하도록 만든다. 그러면 Server!CheckRequest가 활성화되고, 이는 ServerNext를 활성화하므로 서버가 시스템에 반응할 수 있다.
정제
기억하자, 처음에 이 모든 장치를 추가한 이유는 두 개의 복잡한 명세를 함께 합성하기 위해서였다. 우리는 어느 쪽의 속성도 위반하지 않는 방식으로 합성하고 있는지 확인해야 한다. 그 역할은 다음 줄들이 담당한다.
RefinesServer == Server!Spec
RefinesWorker == Worker!Spec이들은 정제(refinement) 속성이다. 높은 수준에서 이들은 system.tla가 Server나 Worker가 보통 할 수 없는 일을 하게 만들지 않는지 검사한다. 예를 들어 log에서 무언가를 제거하면 이 속성은 실패할 것이다. Server!Spec에서는 그런 일이 불가능하기 때문이다. 1
TLA+에서 정제는 추이적이다. workerSM.tla는 활성 속성(liveness property)인 <>Done을 가지고 있었다. 이미 workerSM.cfg에서 이를 검증했으므로 system.tla에서 다시 테스트할 필요가 없다. RefinesWorker가 통과하면 Worker!Liveness도 통과한다는 것이 보장된다!
정제가 추이적인 이유
RefinesWorker를 테스트할 때 우리가 검증하는 것은 다음과 같다.
Spec => Worker!Spec
(S) (WS)workerSM.tla를 모델 체킹한 결과 이미 알고 있는 것은 다음과 같다.
Worker!Spec => Worker!Liveness (2)
(WS) (WL)함축은 추이적이다. S => WS이고 WS => WL이면, S => WL이다.
그리고 현재는 실패한다.
cfg 보기
SPECIFICATION Spec
CONSTANTS
NULL = NULL
PROPERTY
RefinesServer
RefinesWorker
문제는 Worker가 계속 잘못된 비밀번호를 선택할 수 있어 서버가 계속 거부하고 Worker가 절대 완료되지 못한다는 것이다. 한 가지 수정 방법은 시스템이 같은 비밀번호를 재시도하지 않도록 하는 것이다.
Sync ==
\* ...
/\ \E x \in Strings:
/\ x \notin server_log
/\ server_req' = x이렇게 하면 명세가 통과한다. 서버의 내부 로그가 시스템에 누출되는 것이 걱정된다면 Worker에도 로그를 추가할 수 있다. system.tla에 직접 추가하거나 Sync에 포함시키는 별도 컴포넌트에 추가하면 된다.2 다른 수정 방법은 강한 공정성(strong fairness) 제약을 사용하는 것이다.
Sync ==
\* ...
/\ \E x \in Strings:
/\ server_req' = x
Fairness ==
/\ WF_vars(Next)
/\ SF_vars(WorkerNext /\ server_req' = "a")이는 올바른 비밀번호를 보내도록 WorkerNext를 실행하는 것이 항상-결국 가능(always-eventually possible)하다면, 명세는 결국 그렇게 할 것이라는 의미다. 이렇게 하면 시스템의 본질적인 논리를 바꾸지 않고도 명세가 통과한다.
열린 세계 닫기
마지막으로 해야 할 일이 하나 있다. server.tla를 모델 체킹 가능하게 만드는 것이다. 이 명세는 “닫힌(closed)” 명세가 아니기 때문에 직접 테스트할 수 없다. 요청을 보내기 위해 다른 명세에 의존한다. 더 복잡한 명세의 경우 합성과 독립적으로 그 명세의 속성을 테스트할 수 있기를 원한다.
다행히도 이는 TLA+ 커뮤니티에서 “이미 해결된 문제”다. 열린 명세를 닫힌 명세로 정제하면 된다. 이를 위해 새로운 파일 MCserver.tla를 사용한다.
---- MODULE MCserver ----
EXTENDS TLC, server
Strings == {"a", "b", "c"}
ASSUME Password \in Strings
MCInit == Init
WorldNext ==
/\ \E x \in Strings:
req' = x
/\ UNCHANGED <<log, resp>>
MCNext ==
\/ Next
\/ WorldNext
MCSpec == MCInit /\ [][MCNext]_vars
====이는 서버에 요청을 보낼 수 있는 외부 World를 추가한다. 이제 MCserver.tla를 모델 체킹함으로써 server.tla의 행위를 테스트할 수 있다.
cfg 보기
SPECIFICATION MCSpec
CONSTANT
NULL = NULL
Password = "b"VSCode TLA+ 확장의 nightly 버전을 사용 중이라면 server.tla에서 “Check model with TLC” 명령을 실행하면 모델 체커가 MCserver.tla로 자동 실행된다. TLA+ 디버거도 함께 제공된다. VSCode 확장은 훌륭하다.
장단점
일이 꽤 많다! 그렇다면 왜 하나의 큰 명세를 작성하는 대신 이렇게 해야 할까?
애초에 명세를 합성하는 이유는 각각을 독립적으로 작업할 수 있게 하기 위해서다. 각 명세가 30줄 정도라면 큰 문제가 아니지만, 각각 200줄이 넘어가면 그냥 하나의 명세로 다시 작성할 수는 없다.
그래서 이를 더 전통적인 합성 접근 방식과 비교해 보자. Murat Demirbas가 여기에서 분석한 MongoDB Raft 합성을 예로 들겠다. 독립적인 명세는 MongoStaticRaft와 MongoLoglessDynamicRaft이며, 이들은 MongoRaftReconfig에서 함께 합성된다. MongoStaticRaft의 Next는 다음과 같이 생겼다.
\* MongoStaticRaft
Next ==
\* (a)
\/ \E s \in Server : ClientRequest(s)
\* etc
\* (b)
\/ \E s \in Server : \E Q \in Quorums(config[s]) : BecomeLeader(s, Q)
\* etc합성된 Next는 다음과 같이 생겼다.
\* MongoRaftReconfig
Next ==
\/ OSMNext /\ UNCHANGED csmVars
\/ CSMNext /\ UNCHANGED osmVars
\/ JointNext
OSMNext ==
\* (a)
\/ \E s \in Server : OSM!ClientRequest(s)
\* etc
JointNext ==
\* (b)
\/ \E i \in Server : \E Q \in Quorums(config[i]) :
/\ OSM!BecomeLeader(i, Q)
/\ CSM!BecomeLeader(i, Q)
\* etc(a) 아래의 액션들은 OSMNext에서 수동으로 반복되어야 하고, (b) 아래의 액션들은 JointNext에서 다른 명세와 신중하게 엮여야 한다. 이것이 두 명세를 합성하는 표준적인 방식이며, 통합해야 할 명세가 많아질수록 점차 더 어려워진다. 이 패러다임에서는 정제를 검사하기도 어렵다.
나는 Sync 기반 접근 방식으로 두 문제를 모두 피하려 하고 있다. 각 컴포넌트는 이미 변경 없이 사용할 수 있는 자체 Next를 가지고 있다. 공유 변수에 영향을 주는 모든 것은 추가적인 Sync 연산자가 처리한다.
이 명세가 내 접근 방식으로 이득을 볼까? 모르겠다. 나는 이 접근 방식을 외부 컴포넌트와 상호작용하는 주 “머신”을 위해 설계했는데, 여기서는 두 명세가 동등한 위치에 있다. 변환이 어떻게 보일지에 대한 스케치는 가지고 있지만, 그것이 반드시 더 낫다고는 말할 수 없다.
변경 사항 스케치
이는 추가적인 상태 머신을 더하지 않은 경우다. 하나의 “주” 명세를 고르자, 예를 들어 CSM이라고 하자. 그러면 Spec은 다음과 같이 된다.
Next ==
\/ OSMNext
\/ CSMNext
OSMNext ==
/\ OSM!Next
/\ UNCHANGED <<csmVars>>
/\ UNCHANGED <<sharedVars>> \* new op
CSMNext ==
/\ CSM!Next
/\ Sync
/\ UNCHANGED <<osmVars>>sharedVars를 OSMNext에 추가해야 OSM!BecomeLeader를 독자적으로 호출하지 않는다 — 그 호출은 Sync를 통해 일어나야 한다. sharedVars는 csmVars 및 osmVars와 일부 변수를 공유하게 될 것이다.
Sync는 JointNext와 비슷하게 생길 것이다.
Sync ==
\/ \E i \in Server : \E Q \in Quorums(config[i]) :
/\ OSM!BecomeLeader(i, Q)
/\ CSM!BecomeLeader(i, Q)
\/ \* ...
\/ UNCHANGED <<sharedVars>>CSM!BecomeLeader를 CSMNext와 Sync 모두에서 반복하는 것이 거슬리지만, OSM과 CSM이 i와 Q에 대해 같은 값을 사용하도록 보장하는 가장 직관적인 방법이다. 이를 중복 제거하는 몇 가지 방법을 찾아냈지만, 모두 TLA+ 의미론을 창의적으로 오용하는 것에 의존한다.
내 예상으로는 전통적인 합성이 더 다양한 경우에 동작하지만, Sync는 동작하는 경우에 더 유지보수하기 쉽고 확장성도 더 좋다.
어느 접근 방식도 “일대다(one-to-many)” 경우를 잘 처리하지 못한다. 단일 Worker에 대한 명세가 있고 이를 이용해 N명의 Worker를 추가하려는 경우인데, 여기서 N은 모델 파라미터다. 왜 이것이 그토록 어려운지는 내 글 Using Abstract Data Types in TLA+에서 논의한다.
결론
이는 강력한 기법이지만 경험을 필요로 하고 복잡성을 더하기도 한다. 매우 큰 명세를 작성해야 하거나 재사용 가능한 컴포넌트 라이브러리가 필요할 때 좋다. 더 작은 명세라면 모든 컴포넌트를 하나의 명세에 넣는 표준 기법을 권장한다.
이는 컨설팅 클라이언트를 위해 개발되었으며 훌륭하게 동작했다. 여러분 모두와 이를 공유하게 되어 기쁘다! 이 글이 마음에 들었다면 여기에서 모델 체킹을 더 빠르게 만드는 방법 같은 다른 고급 TLA+ 기법들도 읽어볼 수 있다.
Murat Demirbas와 Andrew Helwer에게 피드백을 주셔서 감사합니다. 이 글이 마음에 들었다면 내 뉴스레터에 가입해 주길 바란다! 매주 새로운 에세이를 올린다.
나는 기업을 대상으로 형식 기법(formal methods) 교육을 하며, 소프트웨어 개발을 더 빠르고, 더 저렴하고, 더 안전하게 만든다. 더 자세히 알아보려면 여기를 클릭하라.
부록: Sync without primes
일부 회사의 스타일 가이드는 이후 액션에서 primed 변수를 식으로 사용하는 것을 금지한다. 그런 경우 다음과 같이 동일한 효과를 얻을 수 있다.
-Sync ==
- LET i == <<ws, ws'>> IN
+Sync(t) ==
+ LET i == <<t.from, t.to>> IN
+Do(t) ==
+ /\ ws = t.from
+ /\ ws' = t.to
WorkerNext ==
- /\ Worker!Next
- /\ Sync
+ /\ \E t \in Worker!ValidTransitions:
+ /\ Do(t)
+ /\ Sync(t)
/\ UNCHANGED server_logDo(t)는 사실상 Worker!Next의 행위를 모방하는 것에 불과하지만, 우리가 사용하는 전이를 “저장”해 Sync에 전달할 수 있게 해준다.
이는 액션에 전달된 파라미터를 보존하는 데도 유용하며, 때로는 합성에 필요하다.
댓글
로그인하고 댓글 남기기