Supply Chain Inspection

The supply chain inspection contract models cargo inspection at a port with concurrent quality and compliance inspections, hold/release decisions, and compensation for failed hold operations. Its standout feature is ParallelStep -- two inspection branches run concurrently with a JoinPolicy that proceeds only when both succeed.

Business Domain

When a cargo shipment arrives at a port, it must pass both quality inspection and compliance inspection before being cleared. These two inspections are independent and can run concurrently: a quality inspector checks the physical goods while a customs officer verifies documentation and regulatory compliance. If both pass and defect counts are acceptable, the port authority clears the shipment. If either fails or defects exceed the threshold, the shipment is held.

Why This Domain

Supply chain inspection exercises Tenor features that no other domain contract covers:

ParallelStep with JoinPolicy for concurrent inspection branches
Three entities (Shipment, QualityLot, ComplianceLot) with coordinated state transitions
Multi-file imports for shared type definitions
Compensate handler that reverts quality records when a hold operation fails
Multi-entity effects where a single operation transitions three entities at once

Contract Structure

Entities

Entity	States	Initial	Transitions
`Shipment`	arrived, inspecting, cleared, held, released, rejected	arrived	arrived->inspecting, inspecting->cleared, inspecting->held, inspecting->rejected, held->released, held->rejected
`QualityLot`	pending, in_progress, passed, failed	pending	pending->in_progress, in_progress->passed, in_progress->failed
`ComplianceLot`	pending, in_progress, passed, failed	pending	pending->in_progress, in_progress->passed, in_progress->failed

QualityLot and ComplianceLot have identical state machines but represent different inspection processes. The Shipment entity tracks the overall cargo status, with a held state that can resolve to either released or rejected.

Personas

Persona	Authority
`customs_officer`	Begins inspection, records compliance pass, holds shipment, reverts quality
`quality_inspector`	Records quality pass
`port_authority`	Releases cleared shipments
`shipping_agent`	(Declared but not currently used in operations -- reserved for future extensions)

Facts and Sources

Fact	Type	Source	Default
`inspection_type`	Enum: standard, enhanced, expedited	`customs_service.inspection_type`	--
`defect_count`	Int(0..999)	`inspection_service.defect_count`	--
`inspection_items`	List(InspectionItem, max: 200)	`cargo_service.inspection_items`	--
`defect_threshold`	Int(0..100)	`policy_service.defect_threshold`	3
`quality_report`	InspectionReport	`inspection_service.quality_report`	--
`compliance_report`	InspectionReport	`inspection_service.compliance_report`	--
`cargo_weight_kg`	Int(0..1000000)	`cargo_service.total_weight_kg`	--

Named Types (types.tenor -- imported)

hcl

// Supply Chain Inspection — Shared Types (multi-file import leaf)
// Declares types shared across the supply chain domain.
// Imported by: inspection.tenor

// ── Named Types ──────────────────────────────────────────────────────────────

type InspectionReport {
  inspector_id:   Text(max_length: 64)
  pass:           Bool
  defect_count:   Int(min: 0, max: 999)
  notes:          Text(max_length: 1024)
}

type InspectionItem {
  item_id:      Text(max_length: 64)
  description:  Text(max_length: 256)
  compliant:    Bool
  weight_kg:    Int(min: 0, max: 100000)
}

Verdict Chain

Stratum 0 -- Individual Checks

Rule	Condition	Verdict
`all_items_compliant`	`forall item in inspection_items . item.compliant = true`	`items_compliant`
`defects_below_threshold`	`defect_count < defect_threshold`	`defects_acceptable`
`quality_passed`	`quality_report.pass = true`	`quality_ok`
`compliance_passed`	`compliance_report.pass = true`	`compliance_ok`
`defects_exceed_threshold`	`defect_count >= defect_threshold`	`defects_exceeded`

Note that defects_acceptable and defects_exceeded are mutually exclusive by construction: the defect count is either below or at/above the threshold.

Stratum 1 -- Clearance Decision

Rule	Dependencies	Verdict
`shipment_can_clear`	`quality_ok` AND `compliance_ok` AND `defects_acceptable` AND `items_compliant`	`clearance_approved`
`shipment_must_hold`	`defects_exceeded` OR NOT `quality_ok` OR NOT `compliance_ok`	`hold_required`

Clearance requires ALL four conditions. Hold triggers on ANY single failure. This asymmetry is intentional: clearing cargo requires high confidence, but holding requires only one red flag.

Flow Orchestration

inspection_flow

The flow demonstrates ParallelStep with JoinPolicy:

step_begin (OperationStep) -- Customs officer begins inspection, transitioning Shipment, QualityLot, and ComplianceLot simultaneously
step_parallel_inspect (ParallelStep) -- Two branches run concurrently:
- branch_quality: quality_inspector records quality pass
- branch_compliance: customs_officer records compliance pass
- JoinPolicy: on_all_success -> continue, on_any_failure -> terminate
step_release_decision (BranchStep) -- Routes on clearance_approved
- If true: step_release -- Port authority clears shipment
- If false: step_hold -- Customs officer holds shipment
step_hold on_failure: Compensate -- Reverts quality lot to failed state

Complete Contract Source

types.tenor

hcl

// Supply Chain Inspection — Shared Types (multi-file import leaf)
// Declares types shared across the supply chain domain.
// Imported by: inspection.tenor

// ── Named Types ──────────────────────────────────────────────────────────────

type InspectionReport {
  inspector_id:   Text(max_length: 64)
  pass:           Bool
  defect_count:   Int(min: 0, max: 999)
  notes:          Text(max_length: 1024)
}

type InspectionItem {
  item_id:      Text(max_length: 64)
  description:  Text(max_length: 256)
  compliant:    Bool
  weight_kg:    Int(min: 0, max: 100000)
}

inspection.tenor

hcl

// Supply Chain Inspection Contract (MEDIUM)
// Models cargo inspection at a port: concurrent quality and compliance
// inspections, hold/release decisions, and compensation for failed inspections.
//
// Key spec features exercised:
//   - ParallelStep (concurrent quality + compliance inspections)
//   - Compensate handler (rollback inspection on hold)
//   - Multi-entity effects (Shipment + QualityLot + ComplianceLot)
//   - Entity hierarchy (Shipment > QualityLot, Shipment > ComplianceLot)
//   - Bounded universal quantification (forall item in inspection_items)
//   - Multi-file import (types.tenor)
//   - Int fact with default value

import "types.tenor"

// ── Personas ─────────────────────────────────────────────────────────────────

persona customs_officer
persona quality_inspector
persona port_authority
persona shipping_agent

// ── Facts ────────────────────────────────────────────────────────────────────

fact inspection_type {
  type:   Enum(values: ["standard", "enhanced", "expedited"])
  source: "customs_service.inspection_type"
}

fact defect_count {
  type:   Int(min: 0, max: 999)
  source: "inspection_service.defect_count"
}

fact inspection_items {
  type:   List(element_type: InspectionItem, max: 200)
  source: "cargo_service.inspection_items"
}

fact defect_threshold {
  type:    Int(min: 0, max: 100)
  source:  "policy_service.defect_threshold"
  default: 3
}

fact quality_report {
  type:   InspectionReport
  source: "inspection_service.quality_report"
}

fact compliance_report {
  type:   InspectionReport
  source: "inspection_service.compliance_report"
}

fact cargo_weight_kg {
  type:   Int(min: 0, max: 1000000)
  source: "cargo_service.total_weight_kg"
}

// ── Entities ─────────────────────────────────────────────────────────────────

entity Shipment {
  states:  [arrived, inspecting, cleared, held, released, rejected]
  initial: arrived
  transitions: [
    (arrived, inspecting),
    (inspecting, cleared),
    (inspecting, held),
    (inspecting, rejected),
    (held, released),
    (held, rejected)
  ]
}

entity QualityLot {
  states:  [pending, in_progress, passed, failed]
  initial: pending
  transitions: [
    (pending, in_progress),
    (in_progress, passed),
    (in_progress, failed)
  ]
}

entity ComplianceLot {
  states:  [pending, in_progress, passed, failed]
  initial: pending
  transitions: [
    (pending, in_progress),
    (in_progress, passed),
    (in_progress, failed)
  ]
}

// ── Rules — Stratum 0 ────────────────────────────────────────────────────────

rule all_items_compliant {
  stratum: 0
  when:    ∀ item ∈ inspection_items . item.compliant = true
  produce: verdict items_compliant { payload: Bool = true }
}

rule defects_below_threshold {
  stratum: 0
  when:    defect_count < defect_threshold
  produce: verdict defects_acceptable { payload: Bool = true }
}

rule quality_passed {
  stratum: 0
  when:    quality_report.pass = true
  produce: verdict quality_ok { payload: Bool = true }
}

rule compliance_passed {
  stratum: 0
  when:    compliance_report.pass = true
  produce: verdict compliance_ok { payload: Bool = true }
}

rule defects_exceed_threshold {
  stratum: 0
  when:    defect_count >= defect_threshold
  produce: verdict defects_exceeded { payload: Bool = true }
}

// ── Rules — Stratum 1 ────────────────────────────────────────────────────────

rule shipment_can_clear {
  stratum: 1
  when:    verdict_present(quality_ok)
         ∧ verdict_present(compliance_ok)
         ∧ verdict_present(defects_acceptable)
         ∧ verdict_present(items_compliant)
  produce: verdict clearance_approved { payload: Bool = true }
}

rule shipment_must_hold {
  stratum: 1
  when:    verdict_present(defects_exceeded)
         ∨ ¬verdict_present(quality_ok)
         ∨ ¬verdict_present(compliance_ok)
  produce: verdict hold_required { payload: Bool = true }
}

// ── Operations ───────────────────────────────────────────────────────────────

operation begin_inspection {
  allowed_personas: [customs_officer]
  precondition:     inspection_type = "standard"
                  ∨ inspection_type = "enhanced"
                  ∨ inspection_type = "expedited"
  effects: [
    (Shipment, arrived, inspecting),
    (QualityLot, pending, in_progress),
    (ComplianceLot, pending, in_progress)
  ]
  error_contract: [precondition_failed, persona_rejected]
}

operation record_quality_pass {
  allowed_personas: [quality_inspector]
  precondition:     verdict_present(quality_ok)
  effects:          [(QualityLot, in_progress, passed)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation record_compliance_pass {
  allowed_personas: [customs_officer]
  precondition:     verdict_present(compliance_ok)
  effects:          [(ComplianceLot, in_progress, passed)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation release_shipment {
  allowed_personas: [port_authority]
  precondition:     verdict_present(clearance_approved)
  effects:          [(Shipment, inspecting, cleared)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation hold_shipment {
  allowed_personas: [customs_officer]
  precondition:     verdict_present(hold_required)
  effects:          [(Shipment, inspecting, held)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation revert_quality {
  allowed_personas: [customs_officer]
  precondition:     verdict_present(hold_required)
  effects:          [(QualityLot, in_progress, failed)]
  error_contract:   [precondition_failed, persona_rejected]
}

// ── Flows ────────────────────────────────────────────────────────────────────

flow inspection_flow {
  snapshot: at_initiation
  entry:    step_begin

  steps: {
    step_begin: OperationStep {
      op:      begin_inspection
      persona: customs_officer
      outcomes: {
        success: step_parallel_inspect
      }
      on_failure: Terminate(outcome: inspection_blocked)
    }

    step_parallel_inspect: ParallelStep {
      branches: [
        Branch {
          id:    branch_quality
          entry: step_quality
          steps: {
            step_quality: OperationStep {
              op:      record_quality_pass
              persona: quality_inspector
              outcomes: { success: Terminal(quality_cleared) }
              on_failure: Terminate(outcome: quality_failed)
            }
          }
        },
        Branch {
          id:    branch_compliance
          entry: step_compliance
          steps: {
            step_compliance: OperationStep {
              op:      record_compliance_pass
              persona: customs_officer
              outcomes: { success: Terminal(compliance_cleared) }
              on_failure: Terminate(outcome: compliance_failed)
            }
          }
        }
      ]
      join: JoinPolicy {
        on_all_success:  step_release_decision
        on_any_failure:  Terminate(outcome: inspection_failed)
        on_all_complete: null
      }
    }

    step_release_decision: BranchStep {
      condition: verdict_present(clearance_approved)
      persona:   port_authority
      if_true:   step_release
      if_false:  step_hold
    }

    step_release: OperationStep {
      op:      release_shipment
      persona: port_authority
      outcomes: {
        success: Terminal(shipment_cleared)
      }
      on_failure: Terminate(outcome: release_failed)
    }

    step_hold: OperationStep {
      op:      hold_shipment
      persona: customs_officer
      outcomes: {
        success: Terminal(shipment_held)
      }
      on_failure: Compensate(
        steps: [{
          op:         revert_quality
          persona:    customs_officer
          on_failure: Terminal(revert_failed)
        }]
        then: Terminal(inspection_reverted)
      )
    }
  }
}

Static Analysis Output

$ tenor check inspection.tenor

  Elaborating inspection.tenor ...
  Importing types.tenor ...

  ── Types ──────────────────────────────────────────────────────────
  InspectionReport   (types.tenor)        4 fields    ok
  InspectionItem     (types.tenor)        4 fields    ok

  ── Facts ──────────────────────────────────────────────────────────
  inspection_type          Enum(3)                     ok
  defect_count             Int(0..999)                 ok
  inspection_items         List(InspectionItem, 200)   ok
  defect_threshold         Int(0..100)    default      ok
  quality_report           InspectionReport            ok
  compliance_report        InspectionReport            ok
  cargo_weight_kg          Int(0..1000000)             ok

  ── Entities ───────────────────────────────────────────────────────
  Shipment                 6 states   6 transitions    ok
  QualityLot               4 states   3 transitions    ok
  ComplianceLot            4 states   3 transitions    ok

  ── Rules ──────────────────────────────────────────────────────────
  Stratum 0:
    all_items_compliant         → items_compliant          ok
    defects_below_threshold     → defects_acceptable       ok
    quality_passed              → quality_ok               ok
    compliance_passed           → compliance_ok            ok
    defects_exceed_threshold    → defects_exceeded         ok
  Stratum 1:
    shipment_can_clear          → clearance_approved       ok
    shipment_must_hold          → hold_required            ok

  ── Operations ─────────────────────────────────────────────────────
  begin_inspection        [customs_officer]              ok
  record_quality_pass     [quality_inspector]            ok
  record_compliance_pass  [customs_officer]              ok
  release_shipment        [port_authority]               ok
  hold_shipment           [customs_officer]              ok
  revert_quality          [customs_officer]              ok

  ── Flows ──────────────────────────────────────────────────────────
  inspection_flow       6 steps   2 terminals   1 parallel   ok

  ── S-Properties ───────────────────────────────────────────────────
  S1  Determinism         All rules produce deterministic verdicts   PASS
  S2  Stratification      2 strata, no circular dependencies        PASS
  S3  Totality            All verdict references resolve             PASS
  S4  Reachability        All entity states reachable                PASS
  S5  Authority           All operations have authorized personas    PASS
  S6  Termination         All flow paths reach terminal states       PASS
  S7  Compensation        All compensate handlers are well-formed    PASS

  ✓ inspection.tenor — 7/7 S-properties satisfied

Authority Topology

  customs_officer ──────┬── begin_inspection ─────→ Shipment, QualityLot, ComplianceLot
                        ├── record_compliance_pass → ComplianceLot
                        ├── hold_shipment ─────────→ Shipment
                        └── revert_quality ────────→ QualityLot

  quality_inspector ──── record_quality_pass ──────→ QualityLot

  port_authority ──────── release_shipment ────────→ Shipment

The customs officer has the broadest authority, reflecting their role as the primary inspection coordinator. The quality inspector has authority only over quality results, and the port authority has authority only over final clearance.

Flow Path Enumeration

inspection_flow

Path	Steps	Outcome
Both pass + clearance	step_begin -> step_parallel_inspect[both ok] -> step_release_decision[true] -> step_release	Terminal(shipment_cleared)
Both pass + hold	step_begin -> step_parallel_inspect[both ok] -> step_release_decision[false] -> step_hold	Terminal(shipment_held)
Quality fails	step_begin -> step_parallel_inspect[quality fail]	Terminate(inspection_failed)
Compliance fails	step_begin -> step_parallel_inspect[compliance fail]	Terminate(inspection_failed)
Hold with compensation	step_begin -> ... -> step_hold[fail] -> compensate(revert_quality)	Terminal(inspection_reverted)
Begin blocked	step_begin[fail]	Terminate(inspection_blocked)
Release fails	step_begin -> ... -> step_release[fail]	Terminate(release_failed)

Sample Fact Sets

Pass Path (All Clear)

Standard inspection, 1 defect (below threshold of 3), all items compliant, both reports pass:

json

{
  "inspection_type": "standard",
  "defect_count": 1,
  "inspection_items": [
    {"item_id": "CARGO-001", "description": "Steel beams", "compliant": true, "weight_kg": 5000},
    {"item_id": "CARGO-002", "description": "Copper wiring", "compliant": true, "weight_kg": 1200},
    {"item_id": "CARGO-003", "description": "Plastic sheeting", "compliant": true, "weight_kg": 800}
  ],
  "defect_threshold": 3,
  "quality_report": {
    "inspector_id": "QI-2024-001",
    "pass": true,
    "defect_count": 1,
    "notes": "Minor surface defect on beam lot"
  },
  "compliance_report": {
    "inspector_id": "CO-2024-015",
    "pass": true,
    "defect_count": 0,
    "notes": "All documentation in order"
  },
  "cargo_weight_kg": 7000
}

Hold Path (Defects Exceed Threshold)

Enhanced inspection, 5 defects (above threshold of 3), reports pass but defects are too high:

json

{
  "inspection_type": "enhanced",
  "defect_count": 5,
  "inspection_items": [
    {"item_id": "CARGO-101", "description": "Chemical drums", "compliant": true, "weight_kg": 3000},
    {"item_id": "CARGO-102", "description": "Pipe fittings", "compliant": true, "weight_kg": 2500}
  ],
  "defect_threshold": 3,
  "quality_report": {
    "inspector_id": "QI-2024-009",
    "pass": true,
    "defect_count": 5,
    "notes": "Multiple surface defects found on chemical drums"
  },
  "compliance_report": {
    "inspector_id": "CO-2024-022",
    "pass": true,
    "defect_count": 0,
    "notes": "Hazmat documentation verified"
  },
  "cargo_weight_kg": 5500
}

Sample Evaluation Output

Pass Path

$ tenor eval inspection.tenor --facts inspection_pass.facts.json

  Evaluating with 7 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ all_items_compliant         → items_compliant          = true
    provenance: [inspection_items]
  ✓ defects_below_threshold     → defects_acceptable       = true
    provenance: [defect_count, defect_threshold]
  ✓ quality_passed              → quality_ok               = true
    provenance: [quality_report]
  ✓ compliance_passed           → compliance_ok            = true
    provenance: [compliance_report]
  · defects_exceed_threshold    — not satisfied (defect_count < threshold)

  ── Stratum 1 ──────────────────────────────────────────────────────
  ✓ shipment_can_clear          → clearance_approved       = true
    provenance: [quality_ok, compliance_ok, defects_acceptable, items_compliant]
  · shipment_must_hold          — not satisfied (all checks pass)

  ── Flow: inspection_flow ──────────────────────────────────────────
  step_begin              → success (begin_inspection as customs_officer)
  step_parallel_inspect   → all_success
    branch_quality        → success (record_quality_pass as quality_inspector)
    branch_compliance     → success (record_compliance_pass as customs_officer)
  step_release_decision   → true    (clearance_approved present)
  step_release            → success (release_shipment as port_authority)
  Flow outcome: shipment_cleared

  ── Entity States ──────────────────────────────────────────────────
  Shipment:       arrived → inspecting → cleared
  QualityLot:     pending → in_progress → passed
  ComplianceLot:  pending → in_progress → passed

  5 verdicts produced, 6 entity transitions, flow outcome: shipment_cleared

Hold Path

$ tenor eval inspection.tenor --facts inspection_hold.facts.json

  Evaluating with 7 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ all_items_compliant         → items_compliant          = true
    provenance: [inspection_items]
  · defects_below_threshold     — not satisfied (defect_count >= threshold)
  ✓ quality_passed              → quality_ok               = true
    provenance: [quality_report]
  ✓ compliance_passed           → compliance_ok            = true
    provenance: [compliance_report]
  ✓ defects_exceed_threshold    → defects_exceeded         = true
    provenance: [defect_count, defect_threshold]

  ── Stratum 1 ──────────────────────────────────────────────────────
  · shipment_can_clear          — not satisfied (defects_acceptable absent)
  ✓ shipment_must_hold          → hold_required            = true
    provenance: [defects_exceeded]

  ── Flow: inspection_flow ──────────────────────────────────────────
  step_begin              → success (begin_inspection as customs_officer)
  step_parallel_inspect   → all_success
    branch_quality        → success (record_quality_pass as quality_inspector)
    branch_compliance     → success (record_compliance_pass as customs_officer)
  step_release_decision   → false   (clearance_approved absent)
  step_hold               → success (hold_shipment as customs_officer)
  Flow outcome: shipment_held

  ── Entity States ──────────────────────────────────────────────────
  Shipment:       arrived → inspecting → held
  QualityLot:     pending → in_progress → passed
  ComplianceLot:  pending → in_progress → passed

  5 verdicts produced, 5 entity transitions, flow outcome: shipment_held

Formal Properties and Patterns

ParallelStep with JoinPolicy: The two inspection branches run concurrently. The on_all_success join policy means both branches must complete successfully before the flow proceeds to the release decision. on_any_failure immediately terminates the entire flow if either branch fails. This models real-world concurrent inspections where both must pass.

Multi-entity atomic operations: The begin_inspection operation transitions three entities simultaneously: Shipment (arrived -> inspecting), QualityLot (pending -> in_progress), and ComplianceLot (pending -> in_progress). This ensures all three entities are always in consistent states.

Compensate handler for partial failure: If the hold_shipment operation fails after both inspections have passed, the Compensate handler reverts the quality lot to failed. This prevents a situation where inspection records show "passed" but the shipment was never properly held.

Multi-file imports: Type definitions (InspectionReport, InspectionItem) are in a separate types.tenor file. This demonstrates Tenor's module system -- shared types can be defined once and imported by multiple contracts.

Asymmetric clearance/hold logic: Clearance requires ALL conditions (conjunction), while hold triggers on ANY failure (disjunction). This is a deliberate design pattern for safety-critical decisions: the "allow" path requires complete confidence, while the "deny" path has a low trigger threshold.

Default threshold values: The defect_threshold fact defaults to 3. This means that if the policy service is unavailable, the system falls back to a reasonable default rather than failing. The threshold can be overridden by providing a different value at evaluation time.

Business Domain ​

Why This Domain ​

Contract Structure ​

Entities ​

Personas ​

Facts and Sources ​

Named Types (types.tenor -- imported) ​

Verdict Chain ​

Stratum 0 -- Individual Checks ​

Stratum 1 -- Clearance Decision ​

Flow Orchestration ​

inspection_flow ​

Complete Contract Source ​

types.tenor ​

inspection.tenor ​

Static Analysis Output ​

Authority Topology ​

Flow Path Enumeration ​

inspection_flow ​

Sample Fact Sets ​

Pass Path (All Clear) ​

Hold Path (Defects Exceed Threshold) ​

Sample Evaluation Output ​

Pass Path ​

Hold Path ​

Formal Properties and Patterns ​

Business Domain

Why This Domain

Contract Structure

Entities

Personas

Facts and Sources

Named Types (types.tenor -- imported)

Verdict Chain

Stratum 0 -- Individual Checks

Stratum 1 -- Clearance Decision

Flow Orchestration

inspection_flow

Complete Contract Source

types.tenor

inspection.tenor

Static Analysis Output

Authority Topology

Flow Path Enumeration

inspection_flow

Sample Fact Sets

Pass Path (All Clear)

Hold Path (Defects Exceed Threshold)

Sample Evaluation Output

Pass Path

Hold Path

Formal Properties and Patterns