도달 가능성

씬 그래프가 조립되면 프로젝트 전체 lute check는 각 노드에 프로젝트의 진입 집합에서 출발하는 만족 가능한 경로가 하나 이상 있는지 묻습니다 — 경로를 열거하지 않고, 수식 AST를 메모이제이션하는 구조적 재귀로 계산합니다:

reachable(visited(Y)) = ¬unreachable(Y)
reachable(completed(Q)) = ¬E-QUEST-UNREACHABLE(Q)
reachable(active(Q))    = ¬E-QUEST-UNREACHABLE(Q)
reachable(X && Y) = reachable(X) ∧ reachable(Y)
reachable(X || Y) = reachable(X) ∨ reachable(Y)

active(Q)와 completed(Q)는 여기서는 동일합니다. 둘 다 “이 노드보다 먼저 해당 노드에 도달할 수 있어야 한다”고 주장하고, 둘 다 동일한 quest(Q) 노드로 해석되며, 둘 다 precedence DAG에 동일한 엣지를 추가합니다 — 따라서 E-CONN-CYCLE, E-CONN-UNREACHABLE, E-CONN-UNKNOWN-NODE는 active가 존재하기 전과 정확히 동일하게 동작하고, active 원자는 다른 원자와 마찬가지로 E-CONN-FORMULA-TOO-COMPLEX에 포함됩니다. 둘의 차이는 envelope에서만 드러납니다. envelope는 경로가 존재하는지가 아니라 경로가 무엇을 기록했는지를 묻기 때문입니다. 도달 가능성은 더 약한 질문을 하므로 어느 쪽이든 같은 답을 얻습니다.

after가 없거나 비어 있는 노드는 모두 그래프 진입점입니다(reachable = true는 자명함) — 별도로 “시작점을 선언하는” 관례는 필요하지 않습니다. 문법에서 부정을 제외하므로 모든 수식은 단조적이며, 각 노드의 판정은 위상 순서를 따라 한 번 계산하고 메모이제이션합니다. 따라서 선형이고 폭발하지 않습니다. 만족 가능한 경로가 없는 노드는 E-CONN-UNREACHABLE입니다 — 이는 작성된 그래프 자체의 일관성에 관한 순수한 사실이므로, 유보가 필요 없는 유일한 연결성 오류입니다.

판정

lute scenario --project <DIR> reach --node <NODE>는 세 가지 판정 중 하나와 노드에 선언된 after 선행 조건 구조를 보고합니다:

Reachable — 선언된 after 그래프에서 만족 가능한 경로가 존재합니다.
Unreachable — 선언된 경로가 노드에 도달하지 않습니다(E-CONN-UNREACHABLE).
Unknown — 노드가 순환 위에 있거나 순환의 하류에 있으므로 선행 조건 순서를 해석할 수 없습니다(아래 참고).

<nodeId>는 씬의 정식 키(예: marina.s01ep02) 또는 퀘스트의 quest:<id>입니다.

$ lute scenario --project . reach --node narrator.s01ep02
project root: .
reach scene(narrator.s01ep02):
  verdict: Reachable — a satisfiable route exists under your declared routes.
  after: active("findkai")
  referenced node(s) (see `after` above for the && / || structure — this is NOT a flat requirement list):
    - quest(findkai): Reachable — a satisfiable route exists under your declared routes.

참조 노드 목록은 의도적으로 체크리스트가 아닙니다. 각 원자 자체의 판정을 보고하며, after: 위 줄만 && / || 구조가 존재하는 곳입니다. 수식이 논리합인 노드는 그중 하나만 필요로 합니다.

결말

lute scenario --project <DIR> reach --endings[=<OCCASION>](0.27.0)는 모든 결말을 한 번에 검사합니다. =<OCCASION>을 지정하면 해당 계기에 응답하는 모든 beat를 검사하고, 인자를 생략하면 콘텐츠에서 ::end를 실행할 수 있는 모든 beat를 검사합니다. 각 행은 옆에 after: 판정을 두고, when 판정, 즉 프로젝트 전체 lute check가 도달하는 판정(E-BEAT-UNREACHABLE / E-ENTRY-UNREACHABLE(결코 성립하지 않음) 또는 W-BEAT-SHADOWED(결코 승리하지 않음))을 표시합니다. 그리고 when을 반박하는 것이 없으면 읽는 상태 경로와 팩트, 그리고 이를 생성하는 주체를 표시합니다:

$ lute scenario --project . reach --endings=termEnd
project root: .
endings (the beats answering `termEnd`):
  end.other.keeper (beat, lore/endings/other.lute): reachable
    after: Reachable — a satisfiable route exists under your declared routes.
    when: `run.route == 'hotaru'` — whole-project `check` does not refute it; it needs:
      run.route — written by scene `common.festival` (choice into)
  …
  end.ren.lantern (beat, lore/endings/ren.lute): reachable
    after: Reachable — a satisfiable route exists under your declared routes.
    when: `run.route == 'ren' && @devoted(run.aff.ren)` — whole-project `check` does not refute it; it needs:
      run.aff.ren — written by beat `hangouts.council` via component `hangout`, scene `common.arrival`, scene `common.clash`, scene `common.injury`, scene `ren.confession`, scene `ren.date`
      run.route — written by scene `common.festival` (choice into)
  …
10 ending(s): 10 reachable, 0 unreachable, 0 unknown
reachable here means nothing static refutes it, not that a run reaches it: a play that presents the ending is the proof — `lute test --coverage` lists the beats no play presents.

여기서 “Reachable”은 정적으로 결말을 반박하는 것이 아무것도 없다는 뜻입니다. 기록된 쓰기가 run.aff.ren을 when에 필요한 값으로 만들 수 있는지는 분석하지 않습니다. 결말을 제시하는 플레이가 증명이며, lute test --coverage는 어떤 플레이도 제시하지 않는 beat를 나열합니다. 경로에서 아무것도 쓰지 않는 경우에는 nothing writes it이라고 표시하며, 이는 올바른 경우입니다.

순환에 따른 저하는 노드별입니다

E-CONN-CYCLE은 잘못된 순서를 표시하지만 전체 프로젝트 루트를 무효화하지는 않습니다. 도달 가능성은 그래프의 자연스러운 위상 순서로 계산됩니다. 모든 선행 조건 엣지가 해석되면 노드가 그 순서에 들어가며, 이 과정은 순환 구성원과 그 구조적 하류 노드에서만 재귀적으로 실패합니다. 따라서 순환과 위상적으로 독립된 노드는 완전하고 건전한 판정을 계속 받고, 순환 위에 있거나 그 하류에 있는 노드만 Unknown으로 저하됩니다.

허용된 한 가지 보수적 공백이 있습니다. 엣지 모델이 || 위치를 과대 근사하므로, 순환 노드를 거치는 논리합 항을 통해서만 도달 가능한 노드는 독립적인 다른 논리합 항이 도달 가능성을 증명할 수 있더라도 보수적으로 저하된 것으로 보고됩니다. 이는 건전합니다 — 거짓 Unknown은 언제나 안전하지만, 거짓 Reachable은 절대 안전하지 않습니다 — 이를 복구하려면 SCC 응축을 인식하는 분석이 필요합니다(향후 작업).

고정된 A-hybrid enforcement 방침에서는 그래프가 엔진이 준수할 수도 있는 권고 데이터이므로, 모든 도달 가능성 메시지는 무조건적인 런타임 주장으로 쓰지 않고 “사용자가 선언한 after 경로에 따른”이라고 표현합니다.

시작 순환과 피할 수 없는 교착

퀘스트의 start 조건도 그래프의 일부입니다. lute scenario는 순환을 닫는 엣지를 포함해 모든 start 앵커 엣지를 그립니다(0.48.1은 순환을 닫는 엣지를 조용히 버렸습니다).

start는 AND/OR 구조를 유지합니다. 최상위 && 항 하나가 앵커 하나이며, 모든 앵커가 성립해야 합니다. 앵커의 소스들은 대안이어서 하나만 있으면 충분합니다.

퀘스트가 영영 시작할 수 없고 앵커 엣지의 순환 위에 있으면 교착(deadlock) 상태입니다. 이는 시작 가능의 최소 고정점입니다:

앵커가 있는 퀘스트가 아닌 노드는 위의 도달 가능성 분석으로 결정합니다. 씬, beat, entry는 도달 불가이거나 after 순환 위에 있지 않으면 라우팅 가능합니다. 앵커가 없는 퀘스트는 시작할 수 있습니다.
모든 앵커에 시작할 수 있는(퀘스트) 또는 라우팅 가능한(다른 노드) 소스가 하나라도 있으면 퀘스트는 시작할 수 있습니다.
“아무것도 시작할 수 없다”에서 출발해 더 변하지 않을 때까지 반복합니다.

accept 앵커도 start 앵커처럼 계산합니다. 스크립트 안의 소스(::accept, 보상의 accepts) 중 하나가 시작할 수 있거나 호스트 경로가 있으면 시작할 수 있습니다. 교착 상태인 각 퀘스트는 E-QUEST-START-CYCLE(오류, 프로젝트 전체)이며, 강연결 집합마다 하나씩 가장 작은 퀘스트에서 보고합니다. 그 퀘스트의 start에서 보고하고, 수락 기반이라 start가 없으면 id에서 보고합니다. 경로는 가장 짧은 앵커 순환이며 E-CONN-CYCLE처럼 표시하되 각 간선 종류를 이름으로 밝힙니다:

quest start cycle: quest(intro) -[start]-> quest(letter) -[accept]-> quest(intro) — each waits for the next (a `start` for its condition, an accept for the `::accept` or reward that grants it) and no source outside the cycle starts any of them; start one of them from something outside the cycle, or let the host grant one with `accept="external"`

외부에서 진입하는 순환은 문제없습니다. 퀘스트 A가 B가 active일 때 시작하고, B가 A가 active이거나 또는 visited("entry")일 때 시작하며, 씬 entry가 라우팅 가능하다면 B는 시작할 수 있고 따라서 A도 시작할 수 있습니다. 진단은 없습니다. 두 엣지는 여전히 그려지고, 위상 순서가 허용하는 곳에서는 두 퀘스트가 entry 뒤 층에 배치됩니다. 그렇지 않으면 층 없이 나열됩니다.

교착의 출력:

그래프 텍스트는 교착 퀘스트를 (unlayered -- part of a start cycle, E-QUEST-START-CYCLE): … 줄로 출력합니다. JSON과 DOT에는 startCycle이 들어갑니다. after 순환의 텍스트는 그대로입니다.
교착 퀘스트, 또는 교착 소스만을 통해 하류에 있는 퀘스트의 reach는 this quest's `start` waits on a start cycle (E-QUEST-START-CYCLE): <path>; it can never start under your declared routes. 라는 이유와 함께 Unknown입니다. 시작할 수 없는 퀘스트를 Reachable로 보고하지 않습니다(수락 기반 퀘스트는 “this quest’s accept waits on …”로 읽힙니다):

$ lute scenario --project . reach --node quest:letter
project root: .
reach quest(letter):
  verdict: Unknown — this quest's accept waits on a start cycle (E-QUEST-START-CYCLE): quest(letter) -[accept]-> quest(intro) -[start]-> quest(letter); it can never start under your declared routes. [unknown]
  follows: (none declared) — anchored; each anchor holds before it activates, through any one of its sources:
    [accept] quest(intro)
  referenced node(s) (see the anchors above — this is NOT a flat requirement list):
    - quest(intro): Unknown — this quest's `start` waits on a start cycle (E-QUEST-START-CYCLE): quest(intro) -[start]-> quest(letter) -[accept]-> quest(intro); it can never start under your declared routes. [unknown]

호스트가 진입하는 accept 순환은 문제없습니다. letter가 accept="external"이면 호스트 경로가 열리므로 두 퀘스트 모두 Reachable입니다. 상호 accept 순환의 어느 퀘스트에 호스트가 있어도 마찬가지입니다.

자기 퀘스트를 읽는 `start`

퀘스트 자신의 start에서 quest.<own id>.*를 읽으면 E-QUEST-START-SELF(오류, 문서별, start에서)입니다. 퀘스트가 시작되기 전에는 상태에 값이 없으므로 그 조건으로는 퀘스트를 시작할 수 없습니다. 호스트만 부여하는 퀘스트는 start 없이 accept="external"로 씁니다.

앵커 역할을 하는 자기 읽기는 도움이 되지 않는 소스로 계산되므로, 앵커의 소스가 그것뿐인 퀘스트는 교착 상태입니다. 그 퀘스트와 의존 대상은 Reachable이 아닙니다. 자기 읽기만으로 인한 교착은 E-QUEST-START-CYCLE이 아니라 E-QUEST-START-SELF로 보고합니다.

앵커가 없는 퀘스트

앵커가 없는 퀘스트는 reachable holds [proven]이며 이유는 unanchored: available from the start of play입니다. 스크립트 안의 어떤 accept도 이름 붙이지 않고 follows도 없는 accept="external" 퀘스트는 앵커 없이 남습니다. lute scenario reach와 lute constraints는 같은 하나의 도달 가능성 주장을 읽으므로 서로 어긋날 수 없습니다.

수락 기반 퀘스트로 향하는 호스트 경로

수락 기반 퀘스트(start 없음)는 스크립트 안의 accept가 이름 붙이거나 follows를 선언하면 경로들의 any-of인 accept 앵커를 가집니다. 둘 다 아니면 외부 퀘스트든 아니든 앵커가 없어 앵커가 없는 퀘스트로 남습니다:

스크립트 안의 모든 accept(::accept, 보상의 accepts)는 퀘스트의 follows가 무엇이든 상관없이 무조건 경로입니다. follows는 accept를 게이트하지 않습니다.
accept="external" 퀘스트는 호스트 경로를 더합니다. follows가 없으면 열려 있고, 있으면 그 follows 식이 성립할 때 열리는데, 이는 호스트 정책입니다(형식이 잘못된 식이면 경로는 Unknown).
accept="external"이 아니고 아무것도 이름 붙이지 않으면서 follows를 선언한 퀘스트는 빈 accept 앵커를 가집니다. follows는 경로가 아니므로 reach는 Unknown이고 W-QUEST-NEVER-ACCEPTED가 발생합니다.

판정은 경로들의 OR입니다. 작성 측 설명은 수락 기반 퀘스트로 들어오는 경로에 있습니다. follows가 있는 호스트 경로에만 기댄 Reachable 판정은 heuristic 증거를 가집니다(JSON "evidence": "heuristic", 앵커의 "host": {"follows": …}). 이유는 reachable if the host grants it once `follows` holds (host policy; Lute does not enforce it)입니다. follows가 없는 호스트 경로는 proven(“available from the start of play”)을 유지합니다. follows 식은 메타데이터인 (declared ordering; not an activation route)로 출력되고 그 원자는 여전히 간선을 그리지만, 진입 보장이 되지는 않습니다. lute constraints도 같은 주장을 읽으므로, 이런 퀘스트에 건 reachable 제약은 heuristic 증거로 성립합니다.

$ lute scenario --project . reach --node quest:letter
project root: .
reach quest(letter):
  verdict: Reachable — a satisfiable route exists under your declared routes.
  follows: (none declared) — anchored; each anchor holds before it activates, through any one of its sources:
    [accept] the host (accept="external") | quest(intro)
  referenced node(s) (see the anchors above — this is NOT a flat requirement list):
    - quest(intro): Reachable — a satisfiable route exists under your declared routes.

순환을 닫을 accept 간선은 그려지지 않습니다. reach는 노드를 위상 순서로 평가하고, 그려지지 않은 accept(또는 raise) 간선이나 호스트 follows의 그려지지 않은 원자가 판정을 바꿀 수 있는 동안에는 더 이상 바뀌지 않을 때까지 반복합니다. 상호 accept 순환의 어느 퀘스트에 호스트가 있어도 두 퀘스트는 모두 Reachable입니다.

보상 효과가 그리는 엣지

플러그인 보상 종류는 효과(0.50)를 선언할 수 있으며, 그래프는 이를 보상 소유자의 지급 지점(퀘스트의 완료 또는 실패, 목표의 완료)에서 읽습니다:

사실을 assert하는 보상은 핸들러 안의 ::assert처럼, 그 사실을 start에서 읽는 퀘스트로 향하는 사실 엣지를 그립니다. lute scenario --facts는 그래프에 있는 퀘스트(follows가 있는 퀘스트)에 대해 이를 출력합니다. plugin-surfaces 예제에서는 quest(firstVisit) -> quest(secondVisit) [met(mira)]입니다. 따라서 holds('met', ['mira'])로 게이트된 퀘스트는 firstVisit의 보상이 met(mira)를 assert하면 도달 가능합니다: E-QUEST-UNREACHABLE이 없습니다. 조건부 보상(when=)은 조건부 생산자입니다.
퀘스트를 accept하는 보상은 씬의 ::accept가 그리는 엣지인 quest(first) -> quest(second) [accept]를 그립니다. 보상 accepts만 이름을 부르는 수락 기반 퀘스트는 도달 가능하며 W-QUEST-NEVER-ACCEPTED를 내지 않습니다. 그 경고의 메시지는 이제 ”… but no ::accept or reward accepts in the project names it …”입니다.
accept 교착은 시작 순환입니다. 0.53부터, 바깥 소스가 들어오지 않고 호스트 경로도 열려 있지 않은 start와 스크립트 안 accept 앵커(보상 accept 포함)의 순환은 E-QUEST-START-CYCLE입니다(위). 보상을 통해서만 서로를 accept하는 수락 기반 퀘스트 둘은 교착하며, 둘 중 하나에 accept="external"을 쓰면 풀립니다.
lute scenario knowledge와 lute lore는 보상이 assert한 사실의 생산자를 지목합니다: met(mira) — produced by reward BADGE of quest `firstVisit`.

raise되지 않는 occasion

raisedBy: declared로 선언된 occasion은 호스트가 디렉티브나 보상 종류의 선언된 raises를 통해서만 발생시킵니다(0.51). 그런 occasion에 응답하며 after:가 없는 씬이나 번들 비트는 그 raise가 닿는 노드에 앵커되고, 그래프는 각 노드에서 [raises] 엣지를 그립니다(씬 그래프 참고).

도달 가능성은 모든 앵커를 읽는 방식대로 이 앵커를 읽습니다. 앵커된 노드의 Unreachable은 Unknown으로 읽습니다. 선언된 raise는 증명이 아니라 호스트의 약속입니다.
W-OCCASION-NEVER-RAISED(경고, 프로젝트 전체)는 W-QUEST-NEVER-ACCEPTED의 짝입니다. 어떤 선언된 raise도 닿지 않는 raisedBy: declared occasion(대상이 있든 없든)에 응답하는 각 씬이나 비트의 on: 위치에 보고됩니다: scene `chapter2` answers `cutscene` for `scene.chapter2`, which `acme.stage` declares `raisedBy: declared`, but no `effects.raises` in the project raises it — add a `raises` entry to the directive or reward kind that leads here, or drop `raisedBy: declared` if the host raises `cutscene` on its own.
시계는 선언된 raise가 아닙니다. 프로젝트 시계가 발생시키는 occasion(raise: 맵)은 선언된 raise와 무관하게 발생하므로, 그 occasion에는 raisedBy: declared가 앵커를 그리지 않고 W-OCCASION-NEVER-RAISED도 침묵합니다.
플레이 스텝은 소스가 아닙니다. occasion을 발생시키는 lute play나 lute test 스텝은 계산에 넣지 않습니다. 테스트는 게임이 아니라 테스트를 증명합니다.
시계 분석은 선언된 raise를 셉니다. 시계에 매핑된 occasion의 선언된 raise는 시계의 raise: 맵이 예약한 위치만이 아니라 어느 시계 위치에서든 그것을 전달할 수 있습니다. 그래서 어떤 선언된 raise가 닿는 씬이나 비트에 대해 체커는 더 이상 occasion이 예약된 위치에서만 발생한다고 주장하지 않으며, W-BEAT-UNRAISED(“never plays”) 같은 예약 전용 주장은 발생하지 않습니다. 진짜 when 창 실패는 여전히 보고됩니다. 다음 씬의 when이 모든 위치에서 만료된 체인에는 W-CHAPTER-STALL이 여전히 나올 수 있습니다. 선언된 raise가 닿지 않는 응답자는 이전처럼 판정됩니다.

0.34.0의 증거

시나리오 reach 결과에는 JSON에서 evidence가 포함됩니다. 구조적 도달 가능성 증명은 proven이고, 순환으로 저하되었거나 결정되지 않은 결과는 unknown입니다. 사람용 문구는 선언된 after 경로 범위로 한정되며, 유한 분석이 런타임 경로가 전혀 없음을 증명한다고 주장하지 않습니다.

판정

결말