State machines

An immutable entity whose methods return the next value is a state machine, which is what CsCheck's state-machine engine (Spec<S>) explores. [Constraints] also generates OrderConstraints.Actions (every public method on Order that returns Order and takes zero or one argument) and an OrderConstraints.Instance that carries both:

OrderConstraints.Instance.Spec().Exhaustive();
EntitySpec.For<Order>().Exhaustive();
		

1. companion class
2. when Order declares its own constraints

With nothing else configured, AutoBogus supplies the starting orders (valid ones, one per distinct status) and the values each action is tried with. Override anything:

var spec = OrderConstraints.Instance
    .Spec(Order.New(id))
    .Domain(lineA, lineB)
    .DomainFrom<OrderLine, string>(l => l.Sku)
    .Limit(collections: 3)
    .Key(o => (o.Status, o.Lines.Count));        // what makes two orders "the same state"
		

1. a starting state you care about (Order.New is the example's own factory)
2. values to try for AddLine(OrderLine)
3. ...and for RemoveLine(string): the SKUs just added
4. explore orders up to 3 lines (default 2)

How the constraints become requirements:

• Raw (the default) treats every action as responsible for keeping the entity valid. An action that can break a constraint is reported as a bug. Right for self-guarding entities like Order.Ship().
• .Enforced() models the Apply boundary: an action whose result violates a constraint is rejected and the entity stays as it was. Right for entities with plain methods that rely on the constraints to say no. The proof then says "no reachable state is invalid, and every listed transition is reachable through enforced actions"; the useful parts are the coverage and the diagram of the lifecycle that really exists.

If a raw run reports a bug on something you know Apply would stop, that is the signal to add .Enforced().

• A finite domain is the price of a proof. Each action is tried with each value in its argument type's domain: three AutoBogus values by default (all values of an enum or bool), or what you give .Domain<T>(...). Keep it small.
• The space has to close. The default Key compares public properties structurally (lists element by element), and a state holding more than .Limit(...) items (default 2, or the start's own size if larger) is checked but not expanded. Numbers that only grow need a .Boundary(...). If the space does not close, Exhaustive says so rather than passing: reaching maxStates (default 100,000) proves nothing.
• Time is fixed. Time-aware constraints read a constant clock (.Clock(...)), so exploration is deterministic. An entity that reads DateTime.UtcNow itself makes every step a new state; give it a .Key(...) that ignores the timestamp.
• Methods with two or more parameters are not generated as actions. Add them with .Action("Name", state => ...).

Runnable versions of all of this: AutoTestExamples.cs and the per-domain tests next to it. What did and did not convert cleanly is in AUTOTEST_NOTES.md.

The record-with-methods style above is one way. Every front-end below produces an EntitySpec, so the same one-liners work: Exhaustive, Sample, Mermaid, Snapshot, Faults, Conform, Commutes.

public static readonly StateMachine<TicketStatus, string> Machine = StateMachine
    .Define<TicketStatus, string>(TicketStatus.Open)
    .Permit("Assign",          TicketStatus.Open,              TicketStatus.InProgress)
    .Permit("AwaitCustomer",   TicketStatus.InProgress,        TicketStatus.AwaitingCustomer)
    .Permit("CustomerReplied", TicketStatus.AwaitingCustomer,  TicketStatus.InProgress)
    .Permit("Resolve",         [TicketStatus.InProgress, TicketStatus.AwaitingCustomer], TicketStatus.Resolved)
    .Permit("Close",           TicketStatus.Resolved,          TicketStatus.Closed)
    .After(TimeSpan.FromDays(14), TicketStatus.Resolved, TicketStatus.Closed)
    .Build();

Machine.Spec().Exhaustive();
Machine.ToMermaid();
Machine.AsConstraint<SupportTicket>(t => t.Status);

Machine.ConformTo(Open(), t => t.Status,
    bindings: [("Assign", t => t.Assign("agent-1")), ("Resolve", t => t.Resolve(now)), ("Close", t => t.Close())]);
		

1. by itself, after 14 days
2. every state reachable, every edge taken: a state nothing leads to fails here, by name
3. the diagram, generated rather than drawn
4. the Transitions allow-list, so it cannot drift from the diagram

ConformTo walks the machine and applies the same trigger to your real entity, asserting after each step that the entity is in the state the machine says. It fails in two distinct ways, both useful:

• A trigger with no binding ("the machine declares AwaitCustomer, CustomerReplied, the entity has no way to do them") is reported before any walk. The declared state is one the entity can never reach. Running this on the example domains is how SupportTicket's unreachable AwaitingCustomer and Person's unreachable OnLeave show up at declaration time instead of by a missed coverage edge.
• A divergence ("after Resolve in Open the machine says Open, but the entity is in Resolved"): the entity does something the machine forbids. SupportTicket.Resolve() is unguarded, and only Apply stops it; conformance sees the method, not Apply.

ConformToMutable(create, stateOf, bindings: [(trigger, d => d.Open())]) is the same for a class that changes in place. Timeouts (After) are explored by Spec(); conformance does not test them because that needs a clock (use ManualTimeProvider with a temporal rule).

Mermaid in, machine out:

var machine = StateMachine.FromMermaid("""
    stateDiagram-v2
        [*] --> Trial
        Trial --> Active : Activate
        Trial --> Expired : after 14d
        Active --> Cancelled : Cancel
        Cancelled --> [*]
    """);
		

1. StateMachine<string, string>

// A reducer: each command is an action; constraints on the state apply as usual
EntitySpec.FromReducer(0, (int n, string c) => c == "inc" ? n + 1 : Math.Max(0, n - 1), ["inc", "dec"], nonNegative).Boundary(n => n < 4).Exhaustive();

// Event sourcing: state is the fold of events; temporal rules apply to the events each command emits
var doors = EntitySpec.EventSourced(DoorState.Closed, Decide, Evolve, [Open, Close, Lock, Unlock], stateRules);
doors.Spec.Exhaustive();
doors.Exhaustive(neverOpenedRightAfterLocked);
doors.SampleEvents(neverOpenedRightAfterLocked);

// A mutable class: rebuilt by replaying the actions on a fresh instance, so no clone method is needed
EntitySpec.ForMutable(() => new MutableDoor(), rules.Map<MutableDoor>(d => new Door(d.State)))
    .Do("Open", d => d.Open()).Do("Lock", d => d.Lock())
    .Exhaustive();
		

1. state constraints, proved
2. the same, plus temporal rules over the emitted events, for every command sequence
3. random walks: for rules that cannot be proved by a bounded search

Notes: doors.Spec.Exhaustive() proves the state constraints. doors.Exhaustive(rules) also proves temporal rules over the emitted events: it explores the product of the folded state and each rule's monitor (open obligations, with their deadlines relative to now, are part of the state), advancing a virtual clock by stepInterval per command, so a violation comes with the shortest command sequence. A command that emits nothing still lets time pass, so a bounded-response rule is refuted by the commands that "wait". It supports Never, NeverTwice, Always, Transitions, When and After().Then().Within(); Eventually and Required() only resolve when the stream ends, so they are rejected (not silently skipped) and belong in SampleEvents. Events are told apart by ToString(), so use records. Use Transitions (raw adjacency) rather than Never<A, B> for "A must not directly precede B": Never ignores events of other types in between. A mutable class costs a replay per transition, fine for the bounded searches Exhaustive does, so give it a snapshot that says what makes two states the same (default: public properties, structurally). ConstraintSet.Map(project) lifts constraints written for one type onto another (a wrapper, a projection) while keeping names, guards and edges.