Skip to content

Conversation

@ootakazuhiko
Copy link
Collaborator

背景

  • Docker Tests (.github/workflows/docker-tests.yml) の schedule/手動実行が短時間で失敗しており、Hermetic containers (Issue 🔧 Test Stability Issues - Flaky Test Resolution and CI Hardening #1005 Phase 3) の検証に使えない。
  • 直近の main 手動実行では quality(golden) が examples/ を参照するが、Dockerfile.test に取り込まれておらず snapshot が 0 件になり失敗していた。
  • 併せて、docker compose up + abort-on-container-exit は one-shot test containers と相性が悪く、先に終了したコンテナのタイミングで他の suite を強制停止しやすい。

変更

  • docker/Dockerfile.test: golden snapshot が参照する examples/ をコンテナへコピー。
  • .github/workflows/docker-tests.yml: service_filter 未指定時のデフォルト実行を sequential (test-unit,test-integration,test-quality) に変更。
    • abort-on-container-exit / test-reporter 依存の挙動を避け、schedule を決定的にする。

テスト

  • (予定) Workflow "Docker Tests" を workflow_dispatch で実行し、service_filter 未指定で完走することを確認。

影響

  • Docker Tests のデフォルト実行が並列実行ではなく sequential になる(安定性優先)。
  • service_filter 指定で個別 suite の検証は引き続き可能。

ロールバック

  • 本PRを revert。

関連

Copilot AI review requested due to automatic review settings January 23, 2026 15:12
@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@github-actions
Copy link
Contributor

Quality Summary

  • Adapters:

  • Formal: n/a

  • Replay: n/a

  • Trace IDs:

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
Unlinked (top 5) - Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/07ee662111261c150661fd76ae8745a071e5b398/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-OK modules (top 5) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 07ee662111

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Copy link
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR aims to stabilize the Docker Tests workflow by fixing missing test dependencies and improving the execution model for scheduled and manual runs. The changes address failures in quality tests that require the examples/ directory and replace the brittle abort-on-container-exit approach with deterministic sequential execution.

Changes:

  • Added COPY examples/ to Dockerfile.test to provide golden snapshot test data
  • Changed default Docker Tests execution from parallel (via test-reporter + abort-on-container-exit) to sequential execution of test-unit, test-integration, and test-quality

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File Description
docker/Dockerfile.test Adds examples/ directory copy to support quality tests that reference golden snapshots
.github/workflows/docker-tests.yml Replaces test-reporter dependency with direct sequential execution of core test suites

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
Unlinked (top 5) - Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/62c1bde2a4456675662662d0262c496d28e92b4a/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-OK modules (top 5) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
Unlinked (top 5) - Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/445d597cd9ed8be2ec1a605156c410b8e1cd0988/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-OK modules (top 5) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@github-actions
Copy link
Contributor

github-actions bot commented Jan 23, 2026

CI Status Snapshot (2026-01-23T16:03:38.326Z)

@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
Unlinked (top 5) - Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/8997cb581d0cb8d0b0509661e46bd696b52dc5bb/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-OK modules (top 5) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
Unlinked (top 5) - Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/4b43bb2c53219d105bd5088556b33f3686b07c24/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-OK modules (top 5) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
Unlinked (top 5) - Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/dc0bd08445e1e008b886b161fdc1f2ea3dde6ce8/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-OK modules (top 5) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@ootakazuhiko ootakazuhiko merged commit a7b80aa into main Jan 23, 2026
69 of 73 checks passed
@ootakazuhiko ootakazuhiko deleted the ci/fix-docker-tests-schedule branch January 23, 2026 16:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants