State Machine Specification

From Spire Trading Inc.
Revision as of 18:08, 13 July 2026 by Kamal (talk | contribs) (Created page with " Every strategy and order type begins as a state machine specification, a GraphViz file containing the machine's graph and a formal legend defining its parameters, states, eve...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Every strategy and order type begins as a state machine specification, a GraphViz file containing the machine's graph and a formal legend defining its parameters, states, events, and conditions. The specification is designed and reviewed before any code is written, and the Python implementation is a mechanical, one-to-one transcription of it. If a behavior can't be pointed to in the specification, it doesn't belong in the implementation.

This article defines the specification format and its semantics. The running example is PeggedOrder, an order that trades passively at a price pegged to the BBO quote's price, repricing as the BBO quote moves away and honoring the order's limit price.

Anatomy

A specification is a single .gv file with two sections:

  1. A digraph describing the machine: one node per state, one edge per transition, edges labeled by the events and conditions that perform them.
  2. A legend after the closing brace defining the parameters, each state's actions, each event, and each condition.

The example

The PeggedOrder state machine.
digraph PeggedOrder {
  rankdir = LR;
  node [shape = circle];

  S0 [color = green, fontcolor = green];
  S3 [color = red, fontcolor = red];
  S6 [color = blue, fontcolor = blue];

  S0 -> S1 [label = "E0", weight = 100];
  S0 -> S6 [label = "E5"];
  S1 -> S6 [label = "C0"];
  S1 -> S2 [label = "ε", weight = 100];
  S2 -> S3 [label = "E2"];
  S2 -> S4 [label = "E3", weight = 100];
  S2 -> S7 [label = "E5"];
  S4 -> S4 [label = "E0"];
  S4 -> S5 [label = "C1"];
  S4 -> S1 [label = "E4"];
  S4 -> S8 [label = "E5"];
  S5 -> S1 [label = "E4"];
  S5 -> S8 [label = "E5"];
  S7 -> S8 [label = "E3"];
  S7 -> S6 [label = "E4"];
  S8 -> S6 [label = "E4"];
}

Parameters:
  clients (Clients): The clients used to access Nexus services.
  order_fields (OrderFields): The specification of the order to execute.
  peg_difference (Money): The difference applied to the pegged price.

S0:
  filled_quantity = 0
  bbo_quotes = clients.market_data_client.query_bbo_quotes(
    make_current_query(order_fields.ticker))
S2:
  submission_price = peg_price
  fields = OrderFields(order_fields)
  fields.type = OrderType.LIMIT
  fields.price = submission_price
  fields.quantity = order_fields.quantity - filled_quantity
  order = clients.order_execution_client.submit(fields)
S5:
  clients.order_execution_client.cancel(order)
S8:
  clients.order_execution_client.cancel(order)

E0 - bbo_quotes.pop(quote):
  bbo = quote
  peg_price = pick(order_fields.side, bbo.ask.price, bbo.bid.price) -
    direction(order_fields.side) * peg_difference
  if order_fields.price != 0:
    peg_price = pick(order_fields.side,
      max(peg_price, order_fields.price),
      min(peg_price, order_fields.price))
E1 - order.execution_report(report):
  filled_quantity = filled_quantity + report.last_quantity
E2 - E1 if report.status == OrderStatus.REJECTED
E3 - E1 if report.status == OrderStatus.NEW
E4 - E1 if is_terminal(report.status)
E5 - cancel()

C0 - filled_quantity == order_fields.quantity
C1 - pick(order_fields.side, submission_price > peg_price,
    submission_price < peg_price)

Reading it end to end: S0 subscribes to the BBO and waits for the first quote. S1 decides between done (C0) and submitting (ε). S2 submits a limit order at the pegged price. S4 rests, repricing through S5 whenever the market moves away (C1). Any terminal report returns to S1, which resubmits the remainder or finishes. S3 is the rejected terminal, S6 the normal terminal, and S7/S8 handle cancellation, including waiting out an order that is still pending acceptance.

The graph

States are circles named S0, S1, ... and numbered in flow order: the first place the machine goes gets the first number. The start state is green. Red marks a terminal state reached through an actual error, ie. a rejection, and blue marks a completed state. Cancels are orderly outcomes, not errors and should typically transition to a blue state.

Edges are labeled with the conditions and events that perform the transition. When two or more of them share the same source and target, they share one edge with a comma label. Conditions should be labeled before events, and each in numeric order ("C1, E0"). Merging is purely notational.

The graph should render the way the machine runs, the start state is the left-most node and the machine's natural progression reads from left to right, with the default path sitting together on a single row. Deviations from the main path sit above or below it, with the expectation that they eventually loop back into the main path or reach a terminal state. Use the various graphviz/dot notation to tune the rendering with attributes such as weight and constraint to keep states level.

Parameters

The legend begins with a Parameters section listing every parameter as name (Type): description. Descriptions state the parameter's role, refrain from restating a description of the type itself.

States

Each state with an action gets a legend entry: a bare S#: header followed by two-space-indented lines of Python-like pseudocode. Only actions and updates appear, refrain from no prose titles or explanatory notes. States without actions have no entry.

Actions should be written using Python-like API syntax to the extent possible: free functions as free functions (load_ticker_info(clients.market_data_client, ticker)), methods as methods (clients.make_timer(period)), enum constants fully qualified (OrderStatus.REJECTED), access paths written in full through clients, and module prefixes omitted. The formal syntax is not obligated to mirror Python exactly, you can omit various plumbing and boilerplate code and focus on the idealized semantics of the state machine. For example the PeggedOrder's S0 subscription binds its stream as a value:

bbo_quotes = clients.market_data_client.query_bbo_quotes(
    make_current_query(order_fields.ticker))

rather than the literal declare-a-queue-and-pass-it-in shape of the binding.

Variables

Variables are snake_case, never containing whitespace, and every one is defined explicitly and initialized in the start state's action, derived by formula, or updated in the body of the event that changes them. A derived variable that must track a stream is computed in that stream's event body, peg_price is recomputed on every quote in E0, so the submit state and the reprice condition read one variable and can never disagree about the cap.

Events

An event is declared as:

E<n> - <source>.<occurrence>(<binding>) [if <guard>] [:<body>]
  • Source — an expression evaluating to an object that publishes events (ie. bbo_quotes from S0, order from S2). An event's source must be bound before any state with an edge on that event. Sources may be rebound; the event follows the variable.
  • Occurrence — the name of the event being published (pop, execution_report, expired). The occurrence names what arrived.
  • Binding — The event's payload, one or more names that capture the data associated with the event ((report), (quote)). If the payload is unused, name it _. Empty payloads are represented as ().
  • Guard — a Python expression that can be used to match only a subset of events. Introduced with an if, matching match/case precedent. Position disambiguates it from a body conditional.
  • Body — updates and actions, same pseudocode rules as states. Events may perform actions (restart a timer), but always as precise pseudocode, never prose.

A refinement E<m> - E<n> [if <guard>] is its base restricted: it inherits the base's source and binding, and guards conjoin. When a refined event happens its base has happened as well — every REJECTED report is an execution report — so the base's body executes too. Refinements kill repeated signatures, which are an opportunity for errors, and they force the base to be declared before its specializations.

A global event has no source object: E5 - cancel() is the order's own cancel request, delivered through the same serialized queue as everything else.

The generic-event pattern: an update that applies to every occurrence of an event gets its own numbered event rather than a prose note — E1 carries filled_quantity and appears on no edge at all. Numbering it before its specializations guarantees the accounting applies before any specialized event transitions.

For composite orders, a child's completion is observed as its orders publisher closing: E<n> - child.orders.close() for normal completion and E<n> - child.orders.close(failure) for a failure — the failure travels in the completion channel, and the parent never inspects the child's report statuses to detect it.

Typical events include an order publishing an execution report, a timer expiring, and a queue publishing a value:

order.execution_report(report)
timer.expired(state)
queue.pop(value)

Conditions

Conditions are numbered formulas over machine variables:

C0 - filled_quantity == order_fields.quantity

They are evaluated synchronously, in label order, immediately after a state's action; the first condition that holds performs the transition, and if none does the machine waits in the state for events. In-state ordering is load-bearing — list the condition that must win first. When a state's conditions are exhaustive, the final branch is written as ε rather than a vacuous always-true condition.

C1 shows a directional formula: the peg cancels and resubmits only when the resting price is more passive than the peg formula — the market moved away. A symmetric != would make the order retreat ahead of an approaching market and never fill.

Execution semantics

These rules define precisely how a specification runs.

  1. Entering a state: carry out its action, then evaluate its outgoing conditions in label order. The first true condition transitions. If none holds and the state has an ε edge, the ε transition fires. Only when there is no true condition and no ε edge does the machine wait in the state for events.
  2. Handling an event: when an event happens, its body executes. Any refined events derived from it also have their bodies execute afterwards in label order. This is how E0 keeps peg_price current in every state, and how partial fills accumulate while resting.
  3. Transitioning on an event: at most one transition is performed per event by the first event in label order that happened and labels an out-edge of the current state. If no such event exists, the machine remains in its state.
  4. Sequencing: bodies execute first (in label order), then the transition, then the target state's action, then its conditions.
  5. Label order resolves guard overlaps. A REJECTED report is also terminal; E2 before E4 routes it to the rejected terminal from S2, while in S7 — which has no E2 edge — the transition is E4's and the machine ends normally, since there is nothing left to cancel.

Rule 5's S7 behavior is a general principle: any terminal during a user-initiated cancellation is an orderly ending. The machine was asked to stop; however the working order resolved, it stopped.

Recurring patterns

  • The evaluator hub. One state (S1) owns the done-or-continue decision, and every path that might end or continue funnels through it: the first quote, an order's terminal report, a reprice-cancel completing. Without it, each of those sources duplicates the check. Hubs also erase cancel intent: a reprice cancel and any other cancel can share one cancelling state when the hub derives the follow-up from the machine's variables rather than from remembering why the cancel was issued.
  • The pending-acceptance wait. An order in PENDING_NEW cannot be cancelled. A cancel arriving while a submission awaits acceptance parks in an actionless wait state (S7): NEW proceeds to the cancel (S8), any terminal means there is nothing to cancel.
  • The cancellation lanes. From a state with no live order, cancel() goes directly to the blue terminal. From a state with a live order, it goes to a cancelling state whose action cancels the order and whose only exits are terminal reports. Re-entering a cancelling state on a second cancel is harmless; a fill winning the race against the cancel still ends the machine normally.
  • The persistent-order loop. S4 → S1 → S2 resubmits the remainder after any terminal that isn't the machine's own ending — venue cancellations don't kill the order, they re-peg it.