Difference between revisions of "State Machine Specification"
(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...") |
m (Kamal moved page State Machine Specifications to State Machine Specification without leaving a redirect) |
Latest revision as of 19:05, 13 July 2026
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.
Contents
Anatomy
A specification is a single .gv file with two sections:
- A
digraphdescribing the machine: one node per state, one edge per transition, edges labeled by the events and conditions that perform them. - A legend after the closing brace defining the parameters, each state's actions, each event, and each condition.
The example
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_quotesfrom S0,orderfrom 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, matchingmatch/caseprecedent. 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.
- 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.
- 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_pricecurrent in every state, and how partial fills accumulate while resting. - 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.
- Sequencing: bodies execute first (in label order), then the transition, then the target state's action, then its conditions.
- 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.
