Tutorial 4: Behavior & State Machines¶

Duration: 1 hour
Prerequisites: Tutorials 1-3 completed
What you'll learn: State machine modeling, transitions, guards, effects, nested states, and formal verification

Overview¶

State machines model how entities evolve over time with guaranteed correctness. USL provides:

Formal state machine syntax with compile-time verification
Transition guards (preconditions) that prevent invalid state changes
Effects (state modifications) with atomic guarantees
Nested and parallel states for complex workflows
Automatic deadlock and liveness verification
Event-driven transitions with pub/sub integration
State persistence and recovery

Project: Order Fulfillment Workflow¶

We'll model a complete e-commerce order lifecycle including payment processing, inventory management, and shipping logistics with real-world complexity.

Step 1: Define the Domain¶

First, create the order domain:

domain OrderManagement {
  entity Order {
    id: OrderId @primary
    customerId: UserId
    items: List[LineItem]
    totalAmount: Money
    status: OrderStatus
    createdAt: Timestamp
    confirmedAt: Option[Timestamp]
    shippedAt: Option[Timestamp]
    deliveredAt: Option[Timestamp]
    cancelledAt: Option[Timestamp]
    cancellationReason: Option[String]

    invariant positive_total {
      this.totalAmount.amount > 0.0
    }

    invariant has_items {
      len(this.items) > 0
    }
  }

  entity LineItem {
    id: LineItemId @primary
    orderId: OrderId
    productId: ProductId
    quantity: Int
    price: Money

    invariant positive_quantity {
      this.quantity > 0
    }
  }

  enum OrderStatus {
    Pending,
    Confirmed,
    Processing,
    Shipped,
    Delivered,
    Cancelled,
    Refunded
  }
}

Step 2: Simple State Machine¶

Create the basic order lifecycle:

behavior OrderLifecycle for Order {
  initial state Pending {
    description: "Order created but not yet confirmed"
  }

  state Pending {
    on confirm -> Confirmed
      requires hasPaymentMethod(this)
      requires allItemsAvailable(this)
      effects {
        this.status = OrderStatus.Confirmed
        this.confirmedAt = Some(now())
        emit OrderConfirmed(this.id, this.customerId)
        reserveInventory(this.items)
      }

    on cancel -> Cancelled
      effects {
        this.status = OrderStatus.Cancelled
        this.cancelledAt = Some(now())
        this.cancellationReason = Some("Customer requested cancellation")
        emit OrderCancelled(this.id)
      }
  }

  state Confirmed {
    on process -> Processing
      requires paymentCaptured(this)
      effects {
        this.status = OrderStatus.Processing
        emit OrderProcessing(this.id)
      }

    on cancel -> Cancelled
      requires canCancelOrder(this)
      effects {
        this.status = OrderStatus.Cancelled
        this.cancelledAt = Some(now())
        refundPayment(this)
        releaseInventory(this.items)
      }
  }

  state Processing {
    on ship -> Shipped
      requires allItemsPacked(this)
      requires shippingLabelCreated(this)
      effects {
        this.status = OrderStatus.Shipped
        this.shippedAt = Some(now())
        emit OrderShipped(this.id, this.trackingNumber)
        decrementInventory(this.items)
      }
  }

  state Shipped {
    on deliver -> Delivered
      effects {
        this.status = OrderStatus.Delivered
        this.deliveredAt = Some(now())
        emit OrderDelivered(this.id)
        sendDeliveryConfirmation(this.customerId)
      }
  }

  state Delivered {
    // Terminal success state
    entry {
      scheduleReviewRequest(this.customerId, this.id)
    }
  }

  state Cancelled {
    // Terminal cancellation state
    entry {
      auditLog("ORDER_CANCELLED", this.id, this.cancellationReason)
    }
  }
}

Key State Machine Features¶

States: - initial state: Entry point for new instances - state Name { ... }: Normal state with transitions - final state: Terminal state (no outgoing transitions)

Transitions: - on event -> TargetState: Triggered transition - requires: Guard conditions (must be true) - effects: Atomic state modifications

Built-in Hooks: - entry { ... }: Executed when entering state - exit { ... }: Executed when leaving state

Formal Verification

USL automatically verifies: - No unreachable states - No deadlocks (stuck states) - All invariants preserved across transitions - Guards are satisfiable

Step 3: Nested States¶

Model complex substates for processing:

behavior DetailedOrderProcessing for Order {
  initial state Pending

  state Processing {
    initial substate PaymentProcessing

    substate PaymentProcessing {
      on paymentSuccess -> InventoryCheck
        effects {
          markPaymentCaptured(this)
        }

      on paymentFailure -> PaymentFailed
        effects {
          this.paymentError = Some(context.errorMessage)
        }
    }

    substate PaymentFailed {
      on retry -> PaymentProcessing
        requires retryCountBelow(this, 3)

      on cancel -> ^Cancelled  // ^ means parent's state
        effects {
          notifyCustomer(this.customerId, "Payment failed")
        }
    }

    substate InventoryCheck {
      on inventoryAvailable -> Packing
        effects {
          allocateInventory(this.items)
        }

      on inventoryUnavailable -> BackOrder
        effects {
          notifyBackOrder(this)
        }
    }

    substate BackOrder {
      on inventoryRestocked -> Packing
        effects {
          allocateInventory(this.items)
        }

      timeout after 14 days -> ^Cancelled
        effects {
          this.cancellationReason = Some("Inventory unavailable")
        }
    }

    substate Packing {
      on packed -> QualityCheck
    }

    substate QualityCheck {
      on passed -> ReadyToShip

      on failed -> Packing
        effects {
          repackItems(this)
        }
    }

    substate ReadyToShip {
      on ship -> ^Shipped
        effects {
          createShippingLabel(this)
        }
    }
  }
}

Nested State Benefits¶

Encapsulation: Group related substates
Hierarchy: Parent states inherit transitions
Refinement: Add detail without changing interface
Reusability: Common patterns as nested machines

Step 4: Guards and Conditions¶

Add complex business logic:

behavior OrderWithBusinessRules for Order {
  state Confirmed {
    on process -> Processing
      requires {
        paymentVerified(this) &&
        fraudCheckPassed(this) &&
        shippingAddressValid(this) &&
        itemsInStock(this) &&
        !customerBlacklisted(this.customerId) &&
        this.totalAmount.amount <= 10000.00
      }
      effects {
        this.status = OrderStatus.Processing
        logOrderProcessing(this.id)
      }

    on cancel -> Cancelled
      requires {
        let hoursSinceCreation = hoursBetween(this.createdAt, now())
        hoursSinceCreation < 24  // Cancel only within 24 hours
      }
      effects {
        this.status = OrderStatus.Cancelled
        refundPayment(this)
      }
  }

  state Processing {
    on expedite -> ExpressProcessing
      requires {
        this.customer.tier == "Premium" &&
        this.totalAmount.amount > 100.00 &&
        expediteSlotAvailable()
      }
      effects {
        this.processingPriority = Priority.High
        notifyWarehouse("EXPEDITE", this.id)
      }
  }
}

Guard Best Practices¶

✅ DO: - Keep guards side-effect free (pure functions) - Make guards deterministic - Test edge cases - Document complex conditions

❌ DON'T: - Modify state in guards - Call external APIs directly - Use guards for effects

Step 5: Time-Based Transitions¶

behavior OrderWithTimeouts for Order {
  state Pending {
    on confirm -> Confirmed

    timeout after 72 hours -> Cancelled
      effects {
        this.status = OrderStatus.Cancelled
        this.cancellationReason = Some("Order expired")
        releaseReservation(this.id)
      }
  }

  state Processing {
    timeout after 24 hours -> Stalled
      effects {
        alertOperations("Order stalled", this.id)
      }
  }

  state Stalled {
    on resume -> Processing
      effects {
        clearStalledFlag(this)
      }

    timeout after 48 hours -> Cancelled
      effects {
        this.status = OrderStatus.Cancelled
        refundCustomer(this)
      }
  }
}

Step 6: State Machine Testing¶

spec OrderLifecycleTests {
  test "can confirm pending order with payment" {
    let order = Order {
      id: generateId(),
      status: OrderStatus.Pending,
      items: [createLineItem()],
      totalAmount: Money(100.00, "USD"),
      customerId: createTestUserId()
    }

    // Mock preconditions
    mock hasPaymentMethod(order) returns true
    mock allItemsAvailable(order) returns true

    // Execute transition
    let result = order.confirm()

    // Verify post-conditions
    assert order.status == OrderStatus.Confirmed
    assert order.confirmedAt.is_some()
    assert eventEmitted(OrderConfirmed)
  }

  test "cannot confirm without payment method" {
    let order = createTestOrder()

    mock hasPaymentMethod(order) returns false

    expect_error {
      order.confirm()
    }
  }

  test "timeout cancels pending order" {
    let order = Order { status: OrderStatus.Pending, /* ... */ }

    // Simulate time passage
    advance_time(73 hours)

    assert order.status == OrderStatus.Cancelled
    assert order.cancellationReason == Some("Order expired")
  }

  property "delivered orders are never cancelled" {
    forall order in Order where order.status == OrderStatus.Delivered {
      always (order.status != OrderStatus.Cancelled)
    }
  }
}

Step 7: Verification¶

Compile with verification enabled:

usl verify order-lifecycle.usl --state-machines

USL verifies:

Reachability: All states can be reached
Termination: No infinite loops
Deadlock Freedom: No stuck states
Invariant Preservation: All invariants hold in every state
Guard Satisfiability: Guards can be true
Determinism: No conflicting transitions

Example output:

Verifying state machine OrderLifecycle...
✓ All states reachable from initial state
✓ No deadlocks detected
✓ All invariants preserved across transitions
✓ Guards are satisfiable
✓ 0 warnings

State Machine Statistics:
- States: 8
- Transitions: 12
- Guards: 15
- Effects: 18
- Events: 6

Verification complete: OrderLifecycle is CORRECT ✓

Common Patterns¶

Approval Workflow¶

behavior ApprovalWorkflow for Document {
  initial state Draft

  state Draft {
    on submit -> PendingReview
  }

  state PendingReview {
    on approve -> Approved
      requires approverCount(this) >= 2

    on reject -> Rejected
      effects { recordRejection(this) }

    on requestChanges -> Draft
      effects { notifyAuthor(this) }
  }

  state Approved {
    on publish -> Published
  }

  final state Published
  final state Rejected
}

Multi-Step Form¶

behavior FormWizard for Registration {
  initial state PersonalInfo

  state PersonalInfo {
    on next -> ContactInfo
      requires personalInfoValid(this)
  }

  state ContactInfo {
    on next -> Preferences
      requires contactInfoValid(this)
    on back -> PersonalInfo
  }

  state Preferences {
    on submit -> Processing
    on back -> ContactInfo
  }

  state Processing {
    on success -> Complete
    on failure -> ContactInfo
      effects { showError(this.error) }
  }

  final state Complete
}

What You've Learned¶

✅ State machine modeling with formal semantics
✅ Guards (requires) and effects
✅ Nested states for complex workflows
✅ Time-based transitions
✅ State machine testing
✅ Formal verification of correctness
✅ Common workflow patterns

Exercises¶

Add Return Flow: Extend OrderLifecycle to support returns and refunds
Add Notification States: Create parallel notification states
Implement Retry Logic: Add automatic retry for failed payments
Create Audit Trail: Track all state transitions in an audit log

Next Steps¶

Continue to Tutorial 5: Service Layer to learn how to expose your state machines through APIs.