working-model

Working Model

작은 *.model.json 명세를 작성합니다: 매개변수(슬라이더), 상태, 작은 안전한 규칙 언어로 된 규칙, 이벤트 시나리오, 상태에 바인딩된 시각적 파트, 캡션, 그리고 주장(claim). CLI는 Node에서 이를 시뮬레이션하고, 모든 주장을 확인하며, 텍스트를 린트하고, 동일한 엔진을 실행하고 독자가 슬라이더를 드래그할 때 주장을 실시간으로 다시 확인하는 하나의 오프라인 HTML 페이지를 빌드합니다.

요점: 테스트된 설명입니다. 모델이 뒷받침할 수 없는 주장은 사용자가 보기도 전에 실패합니다.

명령어

모든 명령어는 Node 20 이상에서 실행되며 npm install이 필요 없습니다. 따옴표를 유지하세요: 경로에 공백이 포함될 수 있습니다.

node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" new token-bucket --dir ./explainers         # 이미 통과하는 명세
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json  # 스키마, 시뮬레이션, 주장, 린트
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --mutate   # 주장이 잘못된 규칙을 잡아내는가?
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" build ./explainers/token-bucket.model.json -o ./explainers/token-bucket.html
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" layout ./explainers/token-bucket.model.json --out ./explainers/shots   # 로컬 Chrome 또는 Edge 필요
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" snap ./explainers/token-bucket.model.json --at 2 -o shot.png           # 선택적 이미지
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" fuzz ./explainers/token-bucket.model.json --cases 300 --seed 7          # 시드 기반 반례 검색
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --trace t.normalized.json --mapping trace-map.json   # 모델 대 관찰된 트레이스

아래에서 working-model은 node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs"의 줄임말입니다. ${CLAUDE_SKILL_DIR}를 대체하지 않는 에이전트에서는 이 파일이 있는 폴더를 사용하세요. check 종료 코드: 0 모든 주장 통과, 1 주장 또는 린트 오류 실패, 2 명세가 유효하지 않음. 기계 판독 가능 출력을 위해 --json을 추가하고, 다른 슬라이더 위치를 시험하려면 --set name=value를 사용하세요. --mutate는 주장이 실패하지 않으면 0으로 종료됩니다. --mutate-strict(및 --min-score 80)를 추가하면 주장이 전혀 실패하지 않거나 점수가 낮을 때 1로 종료됩니다. build --mutate는 점수를 페이지에 저장합니다.

워크플로우

1. 놀라운 부분을 보여주는 가장 작은 모델을 선택하세요. 하나의 메커니즘, 하나의 시나리오, 2~4개의 슬라이더. 질문: 똑똑한 독자가 무엇을 잘못 이해할까? 그 순간이 화면에 나타나도록 시나리오를 만드세요 (버킷을 비우는 버스트, 함께 도착하는 재시도, 캐시를 플러시하는 스캔).
2. 스캐폴딩하거나 예제를 복사하세요. working-model new <name> 또는 examples/에서 가장 가까운 파일 (토큰 버킷, 지터가 있는 백오프, LRU 캐시, TCP AIMD, 서킷 브레이커, SIR 전염병, 복리, 로드 밸런싱, 블룸 필터, Raft 리더 선출, 재고 재주문 시점)로 시작하세요.
3. 매개변수, 상태 및 규칙을 작성하세요. 이산 시간: 각 틱은 rules.tick을 실행한 다음, 해당 틱의 이벤트가 rules.on.<event> 핸들러를 실행합니다. 단위를 정직하게 유지하세요 (timeUnit, 슬라이더 unit). 링크가 애니메이션화하거나 주장이 감시해야 하는 항목에는 emit('name', payload)를 사용하세요.
   • 시간은 부동 소수점입니다. t는 tick × dt이므로 t + lead로 저장된 시간은 나중의 t와 정확히 같을 수 없습니다. 마감일 및 카운트다운의 경우 틱 번호를 저장하세요 (due = tick + round(lead / dt), 그런 다음 tick >= due). references/spec.md에는 "Writing Rules That Behave" 아래에 이러한 함정이 더 많이 있습니다.
   • 리스트는 값입니다: a = b는 복사합니다. 중첩된 리스트는 인덱스를 통해 변경하세요 (push(queues[i], job)).
4. 핵심 통찰력을 포착하는 3~8개의 주장을 작성하고, 사소한 것은 피하세요. 규칙을 다시 읽는 주장 (규칙이 min(capacity, ...)일 때 "토큰이 용량을 초과하지 않음")은 실패할 수 없으며 가르치는 바가 없습니다. 흥미로운 주장은 독자가 추측하지 못할 내용을 말합니다: "캐시보다 키가 하나 더 큰 루프는 전혀 히트를 얻지 못함", "지터가 최대 재시도 부하를 낮춤". 올바른 종류를 사용하세요 (at, always, never, eventually, whenever, sweep, compare; references/claims.md 참조).
   • 적어도 하나의 주장은 기본값에서 성립하고 슬라이더가 이동할 때 실패해야 하므로 독자는 설명이 더 이상 유효하지 않은 지점을 볼 수 있습니다. check는 어떤 슬라이더 위치가 어떤 주장을 위반하는지 나열합니다.
   • 각 주장은 모델뿐만 아니라 실제 메커니즘에 대해 참이어야 합니다. 핵심 사실의 출처를 sources에 넣고 모델 가정을 summary에 명시하세요. 주장이 이 시드에 대해서만 성립하는 경우 "이 실행에서"라고 작성하세요.
   • 문장이 표현식이 확인하는 내용을 정확히 말하도록 하세요. check는 문장이 아니라 표현식을 증명합니다. 7단계는 주장이 전혀 실패할 수 있는지 테스트합니다.
   • 가장 느린 슬라이더 설정에 대해 duration을 충분히 길게 하거나, 그렇지 않으면 eventually 주장이 실행이 종료되었기 때문에만 실패합니다.
5. 텍스트의 숫자를 바인딩하세요. 캡션 및 주장 텍스트는 {expression} 홀을 사용합니다: 슬라이더가 이동할 때 구식이 되는 리터럴 10 대신 {capacity}를 작성하세요. check는 리터럴 숫자 (W_LITERAL_NUMBER)에 대해 경고하고 바인딩을 제안합니다. 캡션은 그것이 의존하는 주장을 인용해야 합니다 (cites); 실패하는 주장을 인용하는 것은 오류입니다.
6. check가 오류 없이 N/N claims pass를 말할 때까지 실행하세요. 경고도 수정하세요.
7. 그런 다음 check --mutate를 실행하세요: 주장을 테스트합니다. 의도적으로 규칙을 깨뜨립니다. 변이체당 하나의 작은 변경 (<를 <=로, pop을 shift로, 삭제된 줄, 한 틱 늦은 이벤트), 모든 변이체에 대해 모든 주장을 다시 확인하고, 어떤 주장이 어떤 버그를 잡는지 보고합니다.
   • 모든 주장은 적어도 하나의 변이체를 죽여야 합니다. "결코 실패하지 않은 주장" 아래에 나열된 주장은 실패할 수 없습니다: 규칙을 다시 말하거나, 무효로 통과하거나, 시나리오가 그것을 실행하지 않습니다. 강화하거나 (표현식이 문장 전체를 말하도록) 시나리오를 변경하여 주장이 시험대에 오르게 하세요 (단일 버스트 대신 엇갈린 도착, 맞지 않는 루프). references/claims.md에는 작업 예제가 있습니다.
   • 각 생존 변이체에 대해, 주장을 추가하거나 강화하거나, 변경 사항을 볼 수 없는 이유를 답변에 설명하세요 (예: 키 이름만 바꾸는 경우). 정말 무해한 것만 명세의 mutate.ignore에 그 이유와 함께 들어갑니다. 점수를 높이기 위해 주장이나 어설션을 절대 약화시키지 마세요.
   • 동등 또는 시각적 전용으로 표시된 변이체는 주장이 볼 수 있는 것을 변경하지 않습니다. 점수에서 제외됩니다. 시각적 전용 변이체는 페이지가 그리는 내용을 변경하므로 스크린샷에서 해당 숫자를 확인하세요.
8. 주장을 통과시키기 위해 절대 약화시키거나 삭제하지 마세요. 주장이 실패하면, 어떤 것이 잘못되었는지 결정하세요:
   • 모델이 잘못되었습니다 (규칙 버그, 잘못된 기본값, 누락된 메커니즘): 모델을 수정하세요;
   • 주장이 잘못되었습니다 (실제 메커니즘이 그렇게 동작하지 않거나, 조건 하에서만 그렇습니다): 주장을 수정하고 무엇이 잘못되었는지 말하세요. 어떤 것이었고 왜 그런지 한두 문장으로 사용자에게 알리세요. 통과할 때까지 허용 오차를 완화하거나 더 쉬운 주장으로 바꾸는 것은 허용되지 않습니다.
9. 빌드한 다음 layout을 실행하세요. 모든 E_ 문제 (겹치는 파트, 텍스트 흘러넘침, 텍스트 충돌, 390px에서 페이지가 옆으로 스크롤됨)를 수정하세요. 일반적으로: 파트에 더 많은 그리드 셀을 제공하거나, 레이블을 줄이거나, 파트를 이동하세요. W_LINK_CROSSES도 수정하세요 (다른 파트를 가로지르는 화살표): 파트를 이동하거나 via 포인트를 추가하세요. 작성된 스크린샷을 보고 표시된 모든 숫자가 의도한 숫자인지 확인하세요: 파트 바인딩은 어떤 주장도 테스트하지 않습니다. 독자가 의존할 카운터 또는 게이지의 경우 expect를 추가하고 (동일한 숫자를 계산하는 독립적인 방법, 예: "expect": "len(queue)"), check는 둘이 다르면 실패합니다.
10. 인계: HTML 경로, 주장 요약 줄 (6/6 claims pass) 및 변이 점수, 주장당 한 줄, 그리고 어떤 슬라이더가 어떤 주장을 깨는지. 독자가 알아야 할 모델 가정이 있으면 언급하세요.

반례 찾기

check 및 check --mutate가 통과한 후, working-model fuzz spec.model.json --cases 300 --seed 7은 시드가 있는 근처 경우 (슬라이더 값, 모델 시드, 퍼즈 블록이 퍼즈 가능으로 표시한 이벤트)에 대해 동일한 주장을 실행합니다. 그런 다음 working-model minimize spec.model.json --case .working-model/fuzz/first-failure.json은 동일한 주장이 실패하는 것을 유지하면서 첫 번째 실패를 축소합니다. 축소된 경우를 평범한 언어로 보고하세요 ("흩어진 실패와 차단기 트립 사이의 성공을 떨어뜨리기"). 기본값이 아닌 설정에서의 실패는 설명이 더 이상 유효하지 않은 지점에 대한 발견입니다: 실질적인 근거로 주장이나 모델을 수정하고, 반례를 유지하며, 주장을 절대 약화시켜 침묵시키지 마세요. "실패를 찾지 못함"은 증명이 아닙니다. 세부 사항: docs/FUZZ.md.

관찰된 트레이스와 비교하기

사용자가 실제 시스템의 트레이스 (JSONL 또는 OTLP JSON 하위 집합)를 가지고 있거나 examples/reality-bridge/의 합성 데모를 요청하는 경우에만 이것을 사용하세요. 트레이스는 절대 필요하지 않습니다.

1. 먼저 트레이스에 개인 데이터 (요청 ID, 사용자 ID, IP, 토큰)가 포함될 수 있으며 로컬에서 작업한다고 말하세요. 가져오기는 매핑이 읽는 속성만 유지합니다: working-model trace import trace.jsonl --mapping trace-map.json --out trace.normalized.json. 사용자가 계측이 매핑된 종류의 모든 이벤트를 기록한다고 확인하는 경우에만 --complete를 전달하세요. 그렇지 않으면 완전성은 unknown으로 유지됩니다.
2. 작성 내용에서 네 가지를 분리하세요: 모델 가정, 출처의 메커니즘 사실, 모델 내의 주장, 관찰된 어설션. 가정을 명세의 reality.assumptions에 넣으세요.
3. 트레이스가 실제로 포함하는 내용에서 매핑을 작성하세요. 상관 관계 ID나 트레이스가 기록하지 않는 이벤트를 절대 발명하지 마세요. 양쪽에 주체가 없는 출력은 상관 관계가 없으며 그 어설션은 결정적이지 않습니다. 모든 모델 이벤트는 재생되거나 internalEvents에 나열됩니다.
4. working-model check spec.model.json --trace trace.normalized.json --mapping trace-map.json을 실행하세요. 모델 라인과 관찰된 라인을 별도로 보고하세요 (Model: 4/4 claims pass | Observed: 1 pass, 2 fail, 0 inconclusive), 첫 번째 불일치와 해당 이벤트 ID, 그리고 모든 결정적이지 않은 이유를 그대로 보고하세요. 종료 1은 주장 또는 관찰된 어설션이 실패했음을 의미합니다. 2는 유효하지 않은 트레이스 또는 매핑; 3은 누락된 파일 또는 제한입니다.
5. 트레이스가 일치하지 않으면 실질적인 근거로 가정을 수정하세요. 일반적으로 두 번째 모델에서, 그리고 반례를 유지하세요. 통과하기 위해 minPrecision, minRecall 또는 withinMs를 절대 완화하지 마세요.
6. 볼 페이지를 위해 working-model build spec.model.json --trace trace.normalized.json --mapping trace-map.json -o page.html을 실행하세요: 일반 설명자에 모델 대 관찰된 타임라인, 첫 번째 불일치 및 모든 어설션이 추가됩니다. 정규화된 트레이스를 보유하므로 로컬로 유지됩니다.
7. 사용자가 게시를 요청하는 경우에만 working-model bundle spec.model.json --public ... --preview를 먼저 실행하고, 키 목록을 보여준 다음, --preview 없이 실행하세요. 실제 트레이스에는 명시적인 --acknowledge-privacy가 필요합니다. 사용자를 대신하여 절대 전달하지 마세요.
8. 증거가 보여주지 않는 것을 말하세요: 관찰되지 않은 상태, 샘플링된 트레이스, 적용된 시간 창. 트레이스 증거가 있는 실행 가능한 설명이지, 형식적인 검증이 아닙니다.

형식, 선택기 및 어설션 종류: docs/REALITY-BRIDGE.md. 위협 모델: docs/TRACE-SECURITY.md. 증거의 한계: docs/CONFORMANCE-LIMITS.md.

CI에서 정직하게 유지하기

사용자가 모든 풀 리퀘스트에서 설명이 확인되기를 원할 때 .working-model-ci.json (모델, 그리고 주장, 변이, 퍼즈, 현실 및 패리티 중 무엇을 명시적 임계값으로 실행할지)을 추가하고 .github/workflows/working-model-ci.example.yml을 복사하세요. working-model ci --config .working-model-ci.json --format markdown은 검토자가 읽는 요약을 출력합니다. CI를 통과시키기 위해 임계값을 절대 낮추지 마세요. 세부 사항: docs/CI.md.

한눈에 보는 명세

{
  "title": "Token Bucket Rate Limiter",
  "summary": "A bucket holds up to {capacity} tokens and refills at {refill} per second.",
  "sources": [{ "title": "RFC 2697", "url": "https://www.rfc-editor.org/rfc/rfc2697" }],
  "timeUnit": "s", "dt": 0.1, "duration": 16, "seed": 7,
  "params": [{ "id": "capacity", "label": "Bucket size", "min": 1, "max": 30, "step": 1, "default": 10, "unit": "tokens" }],
  "events": [{ "name": "request", "at": 1, "count": 15 }],
  "state": { "tokens": "capacity", "accepted": 0, "rejected": 0 },
  "derived": { "fill": "tokens / capacity" },
  "rules": {
    "tick": "tokens = min(capacity, tokens + 2 * dt)",
    "on": { "request": ["if tokens >= 1 {", "  tokens -= 1; accepted += 1; emit('accept')", "} else {", "  rejected += 1; emit('reject')", "}"] }
  },
  "layout": { "cols": 12, "rows": 8 },
  "parts": [
    { "id": "bucket", "type": "tank", "at": [4, 0, 4, 4], "label": "Bucket", "level": "fill", "text": "{tokens:.1} of {capacity}" },
    { "id": "chart", "type": "chart", "at": [0, 5, 12, 3], "label": "Tokens", "series": [{ "expr": "tokens" }] }
  ],
  "narration": [{ "from": 1, "to": 3, "text": "The first {capacity} requests spend the stored tokens.", "cites": ["burst-passes"] }],
  "claims": [{ "id": "burst-passes", "kind": "at", "t": 1, "expr": "accepted == capacity", "text": "A full bucket lets exactly the first {capacity} requests through." }]
}

• state의 문자열은 표현식입니다 ("capacity"); 텍스트 값에는 내부 따옴표가 필요합니다 ("'closed'").
• 규칙 언어: 숫자, 문자열, 리스트, true/false, + - * / % **, 비교, and or not, c ? a : b, let, if / else if / else, while, for x in list, break, continue, 할당 연산자, 및 min max abs clamp round sqrt exp log rand randint chance pick len push pop shift unshift remove contains indexOf slice sum range fill emit과 같은 함수. 멤버 액세스, 사용자 함수, eval 없음. 전체 참조: references/spec.md.
• 파트: box tank queue stack grid counter gauge lamp node link chart label group, at: [col, row, width, height]로 그리드에 배치. 바인딩 및 옵션: references/parts.md.
• 주장 및 좋은 주장 작성 방법: references/claims.md