--- id: ATS-PFM-OPS-014 scope: CAP-PFM-OPS-014 product_area: platform module: operations revision: 2 status: proposed approved_by: null approved_at: null source_sha: services-platform: ad3f6a6582843008ed0f5a17b131878d15829af1 macroservice-libraries: 54536a441935c6e09fdb7f96f0bec71c52ba4e03 react-console: baf6dae382d6f41dce976c7f848667ccc37e076f scenarios: - id: ATS-PFM-OPS-014-01 title: Resolve the expected available set level: unit proves: - BR-CAP-PFM-OPS-014-01 - INV-DOM-PFM-OPS-004-04 preconditions: Always-available and licensed applications have mixed operational states. steps: Resolve workspace availability. expected: Only the expected application set is available. negative: false data_needs: Controlled records and caller contexts matching this scenario’s preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers the available ones, and only those, from the same resolution evidence_candidates: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers the available ones, and only those, from the same resolution category: rule binding_evidence: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers the available ones, and only those, from the same resolution - id: ATS-PFM-OPS-014-02 title: Let an explicit withhold prevail level: unit proves: - BR-CAP-PFM-OPS-014-02 - INV-DOM-PFM-OPS-003-05 preconditions: 'A grant, contract and withhold are effective together.' steps: Resolve with different input ordering. expected: The withhold remains the governing refusal. negative: true data_needs: Controlled records and caller contexts matching this scenario’s preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#lets a withhold beat a window covering today, the one way to take a bought application away evidence_candidates: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#lets a withhold beat a window covering today, the one way to take a bought application away category: invariant binding_evidence: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#lets a withhold beat a window covering today, the one way to take a bought application away - id: ATS-PFM-OPS-014-03 title: Apply term and grace boundaries level: unit proves: - BR-CAP-PFM-OPS-014-03 preconditions: 'Contract windows ended recently, ended beyond grace or begin tomorrow.' steps: Resolve today’s availability. expected: 'Current grace remains eligible, elapsed coverage expires and future coverage grants nothing yet.' negative: false data_needs: Controlled records and caller contexts matching this scenario’s preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers expired the day after the grace ends, which is when a licence really runs out evidence_candidates: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers expired the day after the grace ends, which is when a licence really runs out category: boundary binding_evidence: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers expired the day after the grace ends, which is when a licence really runs out - id: ATS-PFM-OPS-014-04 title: Prefer current coverage and use a later grant fallback level: unit proves: - BR-CAP-PFM-OPS-014-04 preconditions: 'Current and expired windows exist, followed by an expired-only case with a grant.' steps: Resolve both cases. expected: The first reports contract coverage and the second override coverage. negative: false data_needs: Controlled records and caller contexts matching this scenario’s preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#falls back to a grant override once the contract has expired, which is a goodwill extension evidence_candidates: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#falls back to a grant override once the contract has expired, which is a goodwill extension category: rule binding_evidence: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#falls back to a grant override once the contract has expired, which is a goodwill extension - id: ATS-PFM-OPS-014-05 title: Preserve always-available access unless withheld level: unit proves: - BR-CAP-PFM-OPS-014-05 preconditions: An always-available application failed preparation and later receives a withhold. steps: Resolve before and after the decision. expected: Failed readiness alone preserves availability while the withhold removes it. negative: false data_needs: Controlled records and caller contexts matching this scenario’s preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#lets a withhold beat always_available, which is the only way to take one of those away evidence_candidates: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#lets a withhold beat always_available, which is the only way to take one of those away category: edge binding_evidence: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#lets a withhold beat always_available, which is the only way to take one of those away - id: ATS-PFM-OPS-014-06 title: Explain each unavailable result once level: unit proves: - BR-CAP-PFM-OPS-014-06 - INV-DOM-PFM-OPS-004-07 preconditions: Applications have each commercial and operational refusal state. steps: Resolve them. expected: Each unavailable result contains its governing refusal reason. negative: false data_needs: Controlled records and caller contexts matching this scenario’s preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#gives each unavailable one the reason its own half of the rule refused by evidence_candidates: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#gives each unavailable one the reason its own half of the rule refused by category: rule binding_evidence: - >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#gives each unavailable one the reason its own half of the rule refused by - id: ATS-PFM-OPS-014-07 title: Use the replacement commercial key level: unit proves: - BR-CAP-PFM-OPS-014-09 preconditions: The grant map contains the renamed accounting application. steps: Inspect mapped application keys. expected: Accounting is granted and the retired key is absent from grants. negative: false data_needs: Controlled records and caller contexts matching this scenario’s preconditions. bound_to: - TST-PFM-OPS-112 provenance: test source: >- services-platform:modules/licensing/tests/unit/catalog/product-grants.spec.ts#grant `accounting` and never the retired `collect`, which is the rename of 2026-10-13 evidence_candidates: - >- services-platform:modules/licensing/tests/unit/catalog/product-grants.spec.ts#grant `accounting` and never the retired `collect`, which is the rename of 2026-10-13 category: rule binding_evidence: - >- services-platform:modules/licensing/tests/unit/catalog/product-grants.spec.ts#grant `accounting` and never the retired `collect`, which is the rename of 2026-10-13 - id: ATS-PFM-OPS-014-08 title: Restore contract coverage after withdrawing a withhold category: interaction level: api proves: - BR-CAP-PFM-OPS-011-04 - BR-CAP-PFM-OPS-014-02 exercises: - CAP-PFM-OPS-014 - CAP-PFM-OPS-011 preconditions: An enabled application has current contract coverage and an effective withhold. steps: 'Resolve access, withdraw the withhold, and resolve again.' expected: The commercial source of the restored result is the surviving contract. negative: false data_needs: Isolated workspace records and caller contexts for both sides of the interaction. bound_to: [] provenance: proposed source: >- services-platform:modules/licensing/tests/e2e/licensing.e2e.spec.js#refuses to withdraw the same override twice, with 409; services-platform:modules/licensing/services/availability/application-availability.ts:licenceStateOf; CAP-PFM-OPS-011; WF-PFM-OPS-016 - id: ATS-PFM-OPS-014-09 title: Reflect a cancellation without extending stale coverage category: interaction level: api proves: - BR-CAP-PFM-OPS-012-08 - BR-CAP-PFM-OPS-014-01 exercises: - CAP-PFM-OPS-014 - CAP-PFM-OPS-012 preconditions: A company has current windows and an enabled workspace application. steps: >- Fail one provider read, then successfully synchronize a cancelled contract and resolve availability. expected: >- The failed read preserves the earlier copy; the successful cancellation removes its contribution to access. negative: false data_needs: Isolated workspace records and caller contexts for both sides of the interaction. bound_to: [] provenance: proposed source: >- services-platform:modules/licensing/tests/integration/services/sync/sync-company-licences.integration.spec.js#changes no snapshot, no window and no last success; services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers the available ones, and only those, from the same resolution; CAP-PFM-OPS-012; WF-PFM-OPS-016 - id: ATS-PFM-OPS-014-10 title: Separate licensing from operational resumption category: interaction level: api proves: - BR-CAP-PFM-OPS-014-01 - BR-CAP-PFM-OPS-015-02 exercises: - CAP-PFM-OPS-014 - CAP-PFM-OPS-015 preconditions: 'A licensed application is enabled, then suspended by staff.' steps: 'Resolve it before suspension, during suspension and after resumption.' expected: The commercial standing remains traceable while availability follows the operational change. negative: false data_needs: Isolated workspace records and caller contexts for both sides of the interaction. bound_to: [] provenance: proposed source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers the available ones, and only those, from the same resolution; services-platform:modules/licensing/tests/integration/services/enablement/provision-tenant-application.integration.spec.js#refuses every move for an application the tenant has never been provisioned for; CAP-PFM-OPS-015; WF-PFM-OPS-016 - id: ATS-PFM-OPS-014-11 title: Keep application availability separate from personal authority category: interaction level: api proves: - BR-CAP-PFM-OPS-014-08 exercises: - CAP-PFM-OPS-014 - CAP-PFM-SEC-007 preconditions: >- A licensed ready application is available to the workspace but the person lacks its application authority. steps: Read workspace standing and request a protected action as that person. expected: The standing read does not itself grant the person permission to use a protected action. negative: false data_needs: Isolated workspace records and caller contexts for both sides of the interaction. bound_to: [] provenance: proposed source: >- services-platform:docs/licensing.md#9. How a licence reaches the permission check; CAP-PFM-SEC-007; WF-PFM-OPS-016 - id: ATS-PFM-OPS-014-12 title: Observe an access change across cache refresh category: interaction level: api proves: - BR-CAP-PFM-OPS-014-08 exercises: - CAP-PFM-OPS-014 - CAP-PFM-SEC-015 preconditions: An application decision changes while an older authorization answer remains cached. steps: 'Complete the change, observe the requested refresh job, then request a new access decision.' expected: >- The refresh request refers to the changed scope; access reflects the current decision after refresh or expiry. negative: false data_needs: Isolated workspace records and caller contexts for both sides of the interaction. bound_to: [] provenance: proposed source: >- services-platform:docs/licensing.md#9. How a licence reaches the permission check; CAP-PFM-SEC-015; WF-PFM-OPS-016 - id: ATS-PFM-OPS-014-13 title: Read commercial standing across a term and grace category: transition level: unit proves: - BR-CAP-PFM-OPS-014-03 - INV-DOM-PFM-OPS-003-06 preconditions: 'A finite window has a first day, last covered day and last grace day.' steps: 'Resolve standing at the first day, immediately after the term, and immediately after grace.' expected: The clock moves the explanation from current coverage through grace to expired coverage. negative: false data_needs: Run-owned records and controlled clocks or dependency responses named in the preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#a licence window, read against a day models: - STATE-PFM-OPS-005 transitions: - 1 - 2 - 3 - id: ATS-PFM-OPS-014-14 title: Resolve an empty application registry category: edge level: unit proves: - BR-CAP-PFM-OPS-014-01 preconditions: The resolver receives no registered applications. steps: Resolve workspace availability with the empty registry. expected: Both the application results and the available set are empty. negative: false data_needs: Run-owned records and controlled clocks or dependency responses named in the preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#answers nothing at all for a registry with no applications in it - id: ATS-PFM-OPS-014-15 title: Keep HQ available outside workspace application records category: invariant level: unit proves: - BR-CAP-PFM-OPS-014-05 - INV-DOM-PFM-OPS-004-08 preconditions: HQ has no workspace application catalogue or operational row. steps: Evaluate the by-rule availability decision for HQ and for registered workspace applications. expected: Only HQ receives the separate by-rule result. negative: false data_needs: Run-owned records and controlled clocks or dependency responses named in the preconditions. bound_to: - TST-PFM-OPS-110 provenance: test source: >- services-platform:modules/licensing/tests/unit/availability/application-availability.spec.ts#is Rhythm HQ and nothing else evidence: - >- Pinned capability rules, object invariants, state transitions and workflows are reviewed for testing obligations. - >- Executable bindings refer only to existing suites; no module executable suite runs during this documentation job. coverage: rule: covered transition: covered validation: 'gap: FND-PFM-OPS-066' permission: not-applicable edge: covered failure: 'gap: FND-PFM-OPS-066' boundary: covered concurrency: 'gap: FND-PFM-OPS-066' invariant: covered interaction: covered coverage_notes: validation: Invalid input and rejected configuration need dedicated proof. permission: >- This internal operation defines no independent caller permission; its callers and audience checks have separate scenarios. failure: Injected dependency failures need dedicated proof. concurrency: >- No controlled overlapping execution proves the capability’s read or write behavior while related state changes. related_capabilities: - CAP-PFM-OPS-011 - CAP-PFM-OPS-012 - CAP-PFM-OPS-015 - CAP-PFM-SEC-007 - CAP-PFM-SEC-015 workflow_interactions: - WF-PFM-OPS-016 coverage_obligations: finding: FND-PFM-OPS-066 uncovered_must_prove: [] object_invariants_requiring_explicit_trace: - INV-DOM-PFM-OPS-004-01 - INV-DOM-PFM-OPS-004-02 - INV-DOM-PFM-OPS-004-03 - INV-DOM-PFM-OPS-004-05 - INV-DOM-PFM-OPS-004-06 related_scenarios: - capabilities: - CAP-PFM-OPS-014 - CAP-PFM-OPS-011 scenario: ATS-PFM-OPS-014-08 - capabilities: - CAP-PFM-OPS-014 - CAP-PFM-OPS-012 scenario: ATS-PFM-OPS-014-09 - capabilities: - CAP-PFM-OPS-014 - CAP-PFM-OPS-015 scenario: ATS-PFM-OPS-014-10 - capabilities: - CAP-PFM-OPS-014 - CAP-PFM-SEC-007 scenario: ATS-PFM-OPS-014-11 - capabilities: - CAP-PFM-OPS-014 - CAP-PFM-SEC-015 scenario: ATS-PFM-OPS-014-12 unbound_scenarios: - ATS-PFM-OPS-014-08 - ATS-PFM-OPS-014-09 - ATS-PFM-OPS-014-10 - ATS-PFM-OPS-014-11 - ATS-PFM-OPS-014-12 transition_review: - model: STATE-PFM-OPS-004 transition: 1 from: scheduled to: in force provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-004 transition: 2 from: in force to: ended provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-004 transition: 3 from: in force to: revoked provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-004 transition: 4 from: scheduled to: revoked provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-004 transition: 5 from: ended to: revoked provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-005 transition: 4 from: current to: replaced provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-005 transition: 5 from: in grace to: replaced provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-006 transition: 1 from: never provisioned to: provisioning provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-006 transition: 2 from: never provisioned to: enabled provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-006 transition: 3 from: provisioning to: enabled provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-006 transition: 4 from: provisioning to: provisioning failed provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-006 transition: 5 from: provisioning failed to: provisioning provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-006 transition: 6 from: enabled to: suspended provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. - model: STATE-PFM-OPS-006 transition: 7 from: suspended to: enabled provenance: unknown source: FND-PFM-OPS-066 note: >- Existing cases may exercise this move, but exhaustive transition-to-scenario trace is not established. permission_review: [] gap_detail: >- Invalid composite-read inputs, failed persistence reads and availability resolved while its inputs change need additional proof. workflow_scenarios: WF-PFM-OPS-016: - ATS-PFM-OPS-011-15 - ATS-PFM-OPS-014-12 --- # Resolve a workspace’s application availability: Capability Test Specification ## Coverage The category map distinguishes authored scenarios from unresolved proof obligations. A bound scenario names an existing executable suite; its recorded result remains unrun. | Rule | Proof status | |---|---| | `BR-CAP-PFM-OPS-014-01` | `ATS-PFM-OPS-014-01`, `ATS-PFM-OPS-014-09`, `ATS-PFM-OPS-014-10`, `ATS-PFM-OPS-014-14` | | `BR-CAP-PFM-OPS-014-02` | `ATS-PFM-OPS-014-02`, `ATS-PFM-OPS-014-08` | | `BR-CAP-PFM-OPS-014-03` | `ATS-PFM-OPS-014-03`, `ATS-PFM-OPS-014-13` | | `BR-CAP-PFM-OPS-014-04` | `ATS-PFM-OPS-014-04` | | `BR-CAP-PFM-OPS-014-05` | `ATS-PFM-OPS-014-05`, `ATS-PFM-OPS-014-15` | | `BR-CAP-PFM-OPS-014-06` | `ATS-PFM-OPS-014-06` | | `BR-CAP-PFM-OPS-014-09` | `ATS-PFM-OPS-014-07` | ## Interactions With Related Capabilities Restore contract coverage after withdrawing a withhold. The commercial source of the restored result is the surviving contract. Reflect a cancellation without extending stale coverage. The failed read preserves the earlier copy; the successful cancellation removes its contribution to access. Separate licensing from operational resumption. The commercial standing remains traceable while availability follows the operational change. Keep application availability separate from personal authority. The standing read does not itself grant the person permission to use a protected action. Observe an access change across cache refresh. The refresh request refers to the changed scope; access reflects the current decision after refresh or expiry. ## Evidence and Boundaries Pinned assertion sources support the listed executable bindings. Proposed cases retain the proof required beyond those boundaries. Structured obligations name incomplete object, transition and permission trace; row-level concurrency proof does not establish complete workflow serialization.