The SaaS subscription contract models a multi-tenant platform's subscription lifecycle: trial period, activation, payment-gated suspension, reactivation, and cancellation. It is the most straightforward domain contract and serves as a good starting point for learning Tenor's entity state machines, verdict-driven operations, and flow orchestration with BranchStep.

Business Domain

Every SaaS platform needs to manage subscription states. A customer starts in a trial period, converts to an active subscription when they provide payment, gets suspended if payment fails, can reactivate after resolving payment issues, and can cancel at any time. This contract encodes those rules formally: what conditions must be true for each transition, who has authority to trigger them, and what happens when payment status changes mid-flow.

Why This Domain

SaaS subscription management exercises Tenor's core constructs in a clean, understandable way:

• A single entity with a clear state machine (trial -> active -> suspended -> cancelled)
• Record types for plan feature configuration
• Payment status as a verdict-gating mechanism
• System personas (billing_system) that act autonomously alongside human personas
• A linear flow with conditional branching

Contract Structure

Entities

Entity	States	Initial	Transitions
Subscription	trial, active, suspended, cancelled	trial	trial->active, trial->cancelled, active->suspended, active->cancelled, suspended->active, suspended->cancelled

The Subscription entity has 6 transitions covering the full lifecycle. Note that suspended->active enables reactivation, and both trial and suspended can transition to cancelled.

Personas

Persona	Authority
account_admin	Can cancel subscriptions
billing_system	Can activate, suspend, reactivate, and cancel subscriptions
support_agent	Can suspend subscriptions

The billing_system persona represents automated payment processing. It has the broadest authority because subscription state changes are typically driven by payment events, not human action.

Facts and Sources

Fact	Type	Source	Default
current_seat_count	Int(0..10000)	identity_service.active_users	--
subscription_plan	Enum: free, starter, professional, enterprise	billing_service.current_plan	--
plan_features	PlanFeatures	plan_service.features	--
payment_ok	Bool	billing_service.payment_status	true
account_age_days	Int(0..100000)	account_service.age_days	--
cancellation_requested	Bool	account_service.cancel_requested	false

Named Types

type PlanFeatures {
  max_seats:       Int(min: 1, max: 10000)
  api_access:      Bool
  sso_enabled:     Bool
  custom_branding: Bool
}

Verdict Chain

Stratum 0 -- Direct Fact Checks

Rule	Condition	Verdict
seats_within_limit	current_seat_count <= plan_features.max_seats	seats_ok
payment_current	payment_ok = true	payment_current
payment_failed	payment_ok = false	payment_failed
trial_eligible	account_age_days <= 30	within_trial_period

Note that payment_current and payment_failed are mutually exclusive -- exactly one will fire for any given fact set.

Stratum 1 -- Composite Verdicts

Rule	Dependencies	Verdict
can_activate	seats_ok AND payment_current	activation_approved
should_suspend	payment_failed	suspension_required

Activation requires both seat compliance and current payment. Suspension requires only payment failure -- seat counts are irrelevant when the customer can't pay.

Flow Orchestration

subscription_lifecycle Flow

A clean three-step flow with a single BranchStep:

1. step_activate (OperationStep) -- billing_system activates the subscription (trial -> active)
2. step_check_payment (BranchStep) -- Routes based on payment_current verdict
   • If true: Terminal(activated) -- subscription is active and paid
   • If false: step_suspend -- billing_system suspends the subscription (active -> suspended)

This models the real-world scenario where activation succeeds but the first payment check immediately fails, triggering suspension.

Complete Contract Source

// SaaS Subscription Lifecycle Contract
// Domain: Multi-tenant SaaS platform — seat management, feature flags,
// subscription state machine, payment-gated operations.
// Exercises: TypeDecl Record, Enum fact, Bool fact with default, entity states,
// multi-stratum rules, persona-restricted operations, linear flow with branch.

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

type PlanFeatures {
  max_seats:       Int(min: 1, max: 10000)
  api_access:      Bool
  sso_enabled:     Bool
  custom_branding: Bool
}

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

persona account_admin
persona billing_system
persona support_agent

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

fact current_seat_count {
  type:   Int(min: 0, max: 10000)
  source: "identity_service.active_users"
}

fact subscription_plan {
  type:   Enum(values: ["free", "starter", "professional", "enterprise"])
  source: "billing_service.current_plan"
}

fact plan_features {
  type:   PlanFeatures
  source: "plan_service.features"
}

fact payment_ok {
  type:    Bool
  source:  "billing_service.payment_status"
  default: true
}

fact account_age_days {
  type:   Int(min: 0, max: 100000)
  source: "account_service.age_days"
}

fact cancellation_requested {
  type:    Bool
  source:  "account_service.cancel_requested"
  default: false
}

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

entity Subscription {
  states:  [trial, active, suspended, cancelled]
  initial: trial
  transitions: [
    (trial, active),
    (trial, cancelled),
    (active, suspended),
    (active, cancelled),
    (suspended, active),
    (suspended, cancelled)
  ]
}

// ── Rules — Stratum 0 (direct fact checks) ───────────────────────────────────

rule seats_within_limit {
  stratum: 0
  when:    current_seat_count <= plan_features.max_seats
  produce: verdict seats_ok { payload: Bool = true }
}

rule payment_current {
  stratum: 0
  when:    payment_ok = true
  produce: verdict payment_current { payload: Bool = true }
}

rule payment_failed {
  stratum: 0
  when:    payment_ok = false
  produce: verdict payment_failed { payload: Bool = true }
}

rule trial_eligible {
  stratum: 0
  when:    account_age_days <= 30
  produce: verdict within_trial_period { payload: Bool = true }
}

// ── Rules — Stratum 1 (composite verdicts) ───────────────────────────────────

rule can_activate {
  stratum: 1
  when:    verdict_present(seats_ok)
         ∧ verdict_present(payment_current)
  produce: verdict activation_approved { payload: Bool = true }
}

rule should_suspend {
  stratum: 1
  when:    verdict_present(payment_failed)
  produce: verdict suspension_required { payload: Bool = true }
}

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

operation activate_subscription {
  allowed_personas: [billing_system]
  precondition:     verdict_present(seats_ok)
  effects:          [(Subscription, trial, active)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation suspend_subscription {
  allowed_personas: [billing_system, support_agent]
  precondition:     verdict_present(suspension_required)
  effects:          [(Subscription, active, suspended)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation reactivate_subscription {
  allowed_personas: [billing_system]
  precondition:     verdict_present(activation_approved)
  effects:          [(Subscription, suspended, active)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation cancel_subscription {
  allowed_personas: [account_admin, billing_system]
  precondition:     cancellation_requested = true
  effects:          [(Subscription, active, cancelled)]
  error_contract:   [precondition_failed, persona_rejected]
}

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

flow subscription_lifecycle {
  snapshot: at_initiation
  entry:    step_activate

  steps: {
    step_activate: OperationStep {
      op:      activate_subscription
      persona: billing_system
      outcomes: {
        success: step_check_payment
      }
      on_failure: Terminate(outcome: activation_failed)
    }

    step_check_payment: BranchStep {
      condition: verdict_present(payment_current)
      persona:   billing_system
      if_true:   Terminal(activated)
      if_false:  step_suspend
    }

    step_suspend: OperationStep {
      op:      suspend_subscription
      persona: billing_system
      outcomes: {
        success: Terminal(suspended)
      }
      on_failure: Terminate(outcome: suspension_failed)
    }
  }
}

Static Analysis Output

$ tenor check saas_subscription.tenor

  Elaborating saas_subscription.tenor ...

  ── Types ──────────────────────────────────────────────────────────
  PlanFeatures                            4 fields    ok

  ── Facts ──────────────────────────────────────────────────────────
  current_seat_count       Int(0..10000)               ok
  subscription_plan        Enum(4)                     ok
  plan_features            PlanFeatures                ok
  payment_ok               Bool           default      ok
  account_age_days         Int(0..100000)              ok
  cancellation_requested   Bool           default      ok

  ── Entities ───────────────────────────────────────────────────────
  Subscription             4 states   6 transitions    ok

  ── Rules ──────────────────────────────────────────────────────────
  Stratum 0:
    seats_within_limit        → seats_ok               ok
    payment_current           → payment_current         ok
    payment_failed            → payment_failed          ok
    trial_eligible            → within_trial_period     ok
  Stratum 1:
    can_activate              → activation_approved     ok
    should_suspend            → suspension_required     ok

  ── Operations ─────────────────────────────────────────────────────
  activate_subscription       [billing_system]          ok
  suspend_subscription        [billing_system, support] ok
  reactivate_subscription     [billing_system]          ok
  cancel_subscription         [account_admin, billing]  ok

  ── Flows ──────────────────────────────────────────────────────────
  subscription_lifecycle  3 steps   2 terminals         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        No compensate handlers (N/A)               PASS

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

Authority Topology

  account_admin ──────── cancel_subscription ──────→ Subscription

  billing_system ──────┬ activate_subscription ────→ Subscription
                       ├ suspend_subscription ─────→ Subscription
                       ├ reactivate_subscription ──→ Subscription
                       └ cancel_subscription ──────→ Subscription

  support_agent ─────── suspend_subscription ──────→ Subscription

The billing_system persona has the broadest authority, reflecting how most subscription state changes are automated. The support_agent can only suspend (for abuse/fraud cases), and the account_admin can only cancel (self-service).

Flow Path Enumeration

subscription_lifecycle

Path	Steps	Outcome
Activation + payment OK	step_activate -> step_check_payment[true]	Terminal(activated)
Activation + payment failed	step_activate -> step_check_payment[false] -> step_suspend	Terminal(suspended)
Activation failed	step_activate[fail]	Terminate(activation_failed)
Suspension failed	step_activate -> step_check_payment[false] -> step_suspend[fail]	Terminate(suspension_failed)

Sample Fact Sets

Activation Path (Happy Path)

Professional plan, 15 seats used out of 50 allowed, payment current, 14-day-old account:

{
  "current_seat_count": 15,
  "subscription_plan": "professional",
  "plan_features": {
    "max_seats": 50,
    "api_access": true,
    "sso_enabled": true,
    "custom_branding": false
  },
  "payment_ok": true,
  "account_age_days": 14
}

Suspension Path

Starter plan, 8 seats used, payment has failed, account past trial period:

{
  "current_seat_count": 8,
  "subscription_plan": "starter",
  "plan_features": {
    "max_seats": 25,
    "api_access": true,
    "sso_enabled": false,
    "custom_branding": false
  },
  "payment_ok": false,
  "account_age_days": 45
}

Sample Evaluation Output

Activation Path

$ tenor eval saas_subscription.tenor --facts saas_activate.facts.json

  Evaluating with 6 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ seats_within_limit       → seats_ok               = true
    provenance: [current_seat_count, plan_features]
  ✓ payment_current          → payment_current         = true
    provenance: [payment_ok]
  · payment_failed           — not satisfied (payment_ok = true)
  ✓ trial_eligible           → within_trial_period     = true
    provenance: [account_age_days]

  ── Stratum 1 ──────────────────────────────────────────────────────
  ✓ can_activate             → activation_approved     = true
    provenance: [seats_ok, payment_current]
  · should_suspend           — not satisfied (payment_failed absent)

  ── Flow: subscription_lifecycle ───────────────────────────────────
  step_activate       → success (activate_subscription as billing_system)
  step_check_payment  → true    (payment_current present)
  Flow outcome: activated

  ── Entity States ──────────────────────────────────────────────────
  Subscription: trial → active

  4 verdicts produced, 1 entity transition, flow outcome: activated

Suspension Path

$ tenor eval saas_subscription.tenor --facts saas_suspend.facts.json

  Evaluating with 6 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ seats_within_limit       → seats_ok               = true
    provenance: [current_seat_count, plan_features]
  · payment_current          — not satisfied (payment_ok = false)
  ✓ payment_failed           → payment_failed          = true
    provenance: [payment_ok]
  · trial_eligible           — not satisfied (account_age_days > 30)

  ── Stratum 1 ──────────────────────────────────────────────────────
  · can_activate             — not satisfied (payment_current absent)
  ✓ should_suspend           → suspension_required     = true
    provenance: [payment_failed]

  ── Flow: subscription_lifecycle ───────────────────────────────────
  step_activate       → success (activate_subscription as billing_system)
  step_check_payment  → false   (payment_current absent)
  step_suspend        → success (suspend_subscription as billing_system)
  Flow outcome: suspended

  ── Entity States ──────────────────────────────────────────────────
  Subscription: trial → active → suspended

  3 verdicts produced, 2 entity transitions, flow outcome: suspended

Formal Properties and Patterns

Mutually exclusive verdicts: payment_current and payment_failed can never both fire because payment_ok is a single boolean. This is guaranteed by construction and verified by S1 (Determinism).

Payment gating: Operations require verdict-based preconditions rather than raw fact checks. The activate_subscription operation requires seats_ok, not a raw comparison -- this ensures the seat limit check is evaluated through the rule engine with full provenance tracking.

System personas: The billing_system persona represents an automated process, not a human actor. Tenor makes no distinction between human and machine personas -- both must satisfy the same authority checks. This is intentional: it means automated systems are held to the same contract as humans.

Default values as safety: payment_ok defaults to true, meaning new accounts are assumed to be in good standing until a payment failure is recorded. cancellation_requested defaults to false, preventing accidental cancellations.

Reactivation through the same verdict chain: The reactivate_subscription operation requires activation_approved, which requires both seats_ok and payment_current. This means a suspended account can only reactivate if it resolves its payment AND its seat count is still within limits -- the system re-evaluates eligibility on every state transition.