유한 상태 기계

정형 기법(formal methods)의 숨기고 싶은 비밀은, 이걸 큰 규모로 키울 방법으로 우리가 아는 게 상태 기계(state machine)를 쓰는 것 하나뿐이라는 점이다. 그러니 이왕이면 TLA+로 상태 기계를 쓰는 법을 배워 두자!

노트

상태 기계를 정식으로 소개하는 글을 쓰고 싶지만, 그때까지는 여기에 있는 좋은 상태 기계 입문 글을 보자.

간단한 상태 기계

내 침실에는 램프 스위치와 벽 스위치 양쪽으로 제어되는 램프가 있다. 램프가 켜지려면 두 스위치가 모두 켜져 있어야 한다. 상태 기계는 다음과 같다:

digraph StateMachine {
{rank=same; WallOff; LampOff}
{rank=max; On}
{rank=source; BothOff}
{BothOff On} -> WallOff[label="lamp switch"];
{BothOff On} -> LampOff[label="wall switch"];
WallOff -> BothOff[label="lamp switch"];
WallOff -> On[label="wall switch"];
LampOff -> On[label="lamp switch"];
LampOff -> BothOff[label="wall switch"];
}

눈여겨볼 점 몇 가지:

전이는 비결정적(nondeterministic)이다. BothOff에서는 벽 스위치를 켤 수도 있고 램프 스위치를 켤 수도 있다.
BothOff와 On 사이에는 전이가 없다. 스위치는 한 번에 하나씩 조작해야 하기 때문이다.
같은 이유로, WallOff와 LampOff 사이를 오갈 방법도 없다.

PlusCal에서는 await 문을 either-or 블록 안에 넣어서 상태 기계를 모델링할 수 있다. await의 조건이 거짓이면 그 분기는 막히지만 나머지 분기는 여전히 선택할 수 있으므로, 비결정성이 그대로 유지된다.

---- MODULE state_machine ----

(*--algorithm lamp
variable state = "BothOff";
process StateMachine = "SM"
begin
  Action:
    either \* this is the state machine
        await state = "BothOff";
        state := "WallOff";
      or
        await state = "BothOff";
        state := "LampOff";
    or
        await state = "LampOff";
        state := "BothOff";
      or
        await state = "LampOff";
        state := "On";
    or
        await state = "WallOff";
        state := "BothOff";
      or
        await state = "WallOff";
        state := "On";
    or
        await state = "On";
        state := "LampOff";
      or
        await state = "On";
        state := "WallOff";
    end either;
    goto Action;
end process;
end algorithm; *)
====

상태 9개 / 고유 상태 4개 spec

보다시피 좀 길다. 상태 기계의 전이마다 하나씩 적어 줘야 하기 때문이다. 매크로(macro)를 쓰면 이걸 간단하게 줄일 수 있다:

macro transition(from, to) begin
  await state = from;
  state := to;
end macro;

혹은 이렇게까지도 할 수 있다.

macro transition(from, set_to) begin
  await state = from;
  with to \in set_to begin
    state := to;
  end with;
end macro;

내 생각에는 그냥 전부 TLA+로 하는 편이 조금 더 깔끔해 보인다.

---- MODULE state_machine ----
VARIABLE state

Trans(a, b) ==
  /\ state = a
  /\ state' = b

Init == state = "BothOff"

Next == 
  \/ Trans("BothOff", "WallOff")
  \/ Trans("BothOff", "LampOff")
  \/ Trans("WallOff", "On")
  \/ Trans("WallOff", "BothOff")
  \/ Trans("LampOff", "BothOff")
  \/ Trans("LampOff", "On")
  \/ Trans("On", "WallOff")
  \/ Trans("On", "LampOff")
  \/ Trans("error", "fetching")

Spec == Init /\ [][Next]_state
====

상태 9개 / 고유 상태 4개 spec

그래서 앞으로는 TLA+만 쓰겠다. PlusCal로도 상태 기계를 만들 수는 있지만, 더 복잡한 걸 하려고 하면 코드가 더 지저분해질 뿐이다.

계층적 상태 기계

상태 기계보다 좋은 게 뭘까? 중첩된 상태 기계다.

하렐 스테이트차트(Harel Statecharts)라고도 부르는 계층적 상태 기계(hierarchical state machine)에서는 상태 안에 다른 상태를 둘 수 있다. 상태 P’가 상태 P 안에 있으면, P’는 P가 할 수 있는 전이를 무엇이든 할 수 있다. 간단한 예로 웹 앱의 UI를 들 수 있다. 로그인하거나 로그아웃할 수 있고, 로그인하면 홈페이지에서 시작해 다른 어느 페이지로든 이동할 수 있다. 좀 더 재미있게 하려고, 그 페이지들 중 하나에는 서브페이지도 있다고 하자.

$digraph hsl { compound=true; LogOut LogOut -> Main; subgraph cluster_app { label="Logged In"; Main -> Settings [dir=both]; Main -> Report1[ltail="cluster_app"]; Report1 -> {Main Settings}[ltail="cluster_reports"]; subgraph cluster_reports { label=Reports Report1; Report2; Report1 -> Report2[dir=both]; } } Main -> LogOut[ltail="cluster_app"]; }$

노트

HSM에는 몇 가지 변종이 있다. 여기서는 다음 세 가지 제약을 따른다:

전이는 어느 상태에서든 시작할 수 있지만, 반드시 “리프(leaf)” 상태에서 끝나야 한다. LoggedIn이나 Reports에 머물 수는 없고, Main이나 Report1에 있어야 한다.
한 상태가 서로 다른 부모 상태를 둘 가질 수는 없다.
상태 사이에 순환은 없다.

계층적 상태를 모델링하려면, Trans("LoggedIn", "Logout")이라고만 써도 앱의 모든 상태, 즉 Main, Settings, Report1, Report2가 전부 포함되게 하고 싶다. 그러려면 재귀적인 In(state1, state2)가 필요하다. 그러면 Trans는 이렇게 된다.

Trans(from, to) ==
  /\ In(state, from) \* Recursive!
  /\ state' = to

상태 계층은 하향식(top-down), 즉 각 상태를 자식 상태들의 집합으로 보내는 함수로 표현할 수도 있고, 상향식(bottom-up), 즉 각 상태를 그 부모 상태로 보내는 함수로 표현할 수도 있다. 각각 나름의 장단점이 있다:

하향식: 함수의 정의역(domain)이 모든 상태임이 보장된다. 실수로 두 상태에 같은 자식을 줄 수 있다.
상향식: 한 상태가 부모를 둘 가질 수가 없다. 모든 상태가 함수의 정의역에 들어 있지는 않으므로, In을 검사하는 코드가 더 번거로워진다. 어떤 상태에 자식이 없는지 확인하기도 더 어렵다.

에라 모르겠다, 둘 다 구현하고 서로 동등한지 확인해 보자.

---- MODULE reports ----
EXTENDS TLC \* For @@
VARIABLE state

States == {
  "LogOut", 
  "LogIn", "Main", "Settings", 
    "Reports", "Report1", "Report2"
}

TopDown == [LogIn |-> {"Main", "Settings", "Reports"}, 
              Reports |-> {"Report1", "Report2"}] @@ [s \in States |-> {}]
              \* @@ is function left-merge        ^^

BottomUp == [Report1 |-> "Reports", Report2 |-> "Reports",
           Reports |-> "LogIn", Main |-> "LogIn", Settings |-> "LogIn"]

\* For TopDown we need to make sure that there are no double-parents
ASSUME \A s1, s2 \in States: s1 # s2 => TopDown[s1] \cap TopDown[s2] = {}

RECURSIVE InTD(_, _)
InTD(s, p) ==
  \/ s = p
  \/ \E c \in TopDown[p]:
    InTD(s, c)

RECURSIVE InBU(_, _)
InBU(s, p) ==
  \/ s = p
  \/ \E c \in DOMAIN BottomUp:
      /\ p = BottomUp[c]
      /\ InBU(s, c)

\* Check the two are identical
ASSUME \A s, s2 \in States: InTD(s, s2) <=> InBU(s, s2)

Trans(from, to) ==
  /\ InTD(state, from)
  /\ state' = to

Init == state = "LogOut"

Next ==
  \/ Trans("LogOut", "Main")
  \/ Trans("Main", "Settings")
  \/ Trans("Settings", "Main")
  \/ Trans("LogIn", "LogOut")
  \/ Trans("LogIn", "Report1")
  \/ Trans("Report1", "Report2")
  \/ Trans("Report2", "Report1")
  \/ Trans("Reports", "Main")

Spec == Init /\ [][Next]_state
AlwaysInLeaf == TopDown[state] = {}
====

상태 16개 / 고유 상태 5개 spec