refmodel

package
v1.2.2 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Oct 10, 2026 License: MIT Imports: 9 Imported by: 0

Documentation

Overview

Package refmodel is a reference model of nova-sprint's sprint table, written from the TLA+ module tla/SprintTables.tla (its sprint-tables-model branch, at 4bf919875) and docs/SPEC-SPRINT.md, and not from the engine. It is small and plain: one struct for the abstract state, and one function per action of the model, named as the model names it, each returning the next state or a refusal. Where the model leaves a choice open (which member a card is dealt to, which readers are asked, which score a new card takes) the function takes the choice as an argument and refuses a choice the model does not allow, with a *ChoiceError.

Functions marked "from the spec, not yet in the model" cover what the engine does today that tla/SprintTables.tla does not yet say: sentinels, release, the tick's parts, the machine, clear and ci green. They are built from the spec's text alone.

The differential test in internal/sprint/store drives the engine and this model with the same actions and compares Abstract(engine) with the model's state after every step.

The other half of the package is the reference for what today's scanning tick decides, and it is written from the engine, not from the spec: Decide (decide.go) is every move one tick makes on a whole snapshot of the four tables, one function per duty, each calling the engine's own planners, and Equal (moves.go) says two decisions are the same and names the first card that is not. A machine that decides from events and indexes instead of scanning compares its decisions with these at every quiet point.

Index

Constants

View Source 
const (
	DutyStrangers   = "strangers"    // tell of a machine that beats and is no member
	DutyPresence    = "presence"     // a member's status follows its beats
	DutyFriendStall = "friend-stall" // a friend holding cards with no sign of life climbs the stall ladder
	DutyResolve     = "resolve"      // waiting primaries whose needs landed go ready; sentinels are reached
	DutyResume      = "resume"       // a stream stopped on another's card goes on when it landed
	DutyCapDeal     = "cap deal"     // a ready card past its attempt cap is dealt to a frontier or heavy friend with room
	DutyDeal        = "deal"         // ready primaries are dealt to the members up
	DutyRebalance   = "rebalance"    // a card queued behind lanes that all work goes to an idle lane of either side
	DutyLevel       = "level"        // the members' backlogs are evened, at the tick's start
	DutyLevelReads  = "level reads"  // the readers' loads are evened, at the tick's start
	DutyAccept      = "accept"       // primaries in review with two ok reads are accepted and queued to merge
	DutyAsk         = "ask"          // primaries in review are asked the reads they want, one at a time
	DutyCheck       = "check"        // a broken rule and a stall are judgments
	DutyDeadlines   = "deadlines"    // a late card or stream is a judgment
	DutyOverdue     = "overdue"      // a judgment past its due time is marked
	DutyDone        = "done"         // the sprint done is said to the coordinator, and the machine stops
	DutyRemind      = "remind"       // each person due is pushed their goal
)

The duties of today's tick, by name, in the order the machine runs them: the parts of sprint.TickParts in their order (the start's level and level reads, then the four tables' updates: the work pump's resolve, cap deal, deal, rebalance and accept, the readers' ask, the merge's resume, the fleet's presence and friend stall; then the end), the unknown machines it tells of (with the fleet's update), and the reminders. The machine's repair of an operation the fence holds is not one: it decides nothing from the tables (Decide's doc says what is left out).

View Source 
const (
	KindCreate  = "create"  // a card is placed for the first time
	KindRemove  = "remove"  // a card leaves the table, its record kept
	KindMove    = "move"    // a card changes place, and maybe its fields or score
	KindSet     = "set"     // a card changes fields or score where it is
	KindBump    = "bump"    // a counter of a card is raised or lowered
	KindProp    = "prop"    // a table property is set (Card is its name, Set its name=value)
	KindRow     = "row"     // a row is added to a table
	KindOpen    = "open"    // a judgment is opened
	KindNotice  = "notice"  // a notification that needs no decision
	KindDecided = "decided" // a judgment is answered
	KindHold    = "hold"    // an acknowledged condition is kept
	KindClose   = "close"   // an open judgment closes on one subject
	KindUpdate  = "update"  // an open judgment is rewritten with the latest facts
	KindRefuse  = "refuse"  // a card the planner would not move, and why
	KindPush    = "push"    // a reminder is delivered to a person
	KindDue     = "due"     // moves and judgments left past the duty's bounds
)

The kinds of a move: what one decision of a duty does.

View Source 
const (
	Waiting = "waiting"
	Ready   = "ready"
	Working = "working"
	Review  = "review"
	Merging = "merging"
	Landed  = "landed"
	Off     = "off"
)

Work cells: a primary's state (SprintTables.tla WorkCells), and Off for a primary that left the table (the model's dropped set).

View Source 
const (
	FReady     = "ready"
	FWorking   = "working"
	FDone      = "done"
	FWithdrawn = "withdrawn"
	Gone       = ""
)

Fleet places of a work card (FleetCells), Withdrawn for a card withdrawn because no member was up (spec section 5: kept in withdrawn), and Gone for a card that left the table with its record kept (the model's gone set).

View Source 
const (
	Asked   = "asked"
	Reading = "reading"
	OK      = "ok"
	Broken  = "broken"
	Retired = ""
)

Read places of a read card (ReadCells), and Retired ("") for a read card retired with its record kept.

View Source 
const (
	Queued   = "queued"
	Merged   = "merged"
	Stuck    = "stuck"
	Returned = "returned"
)

Merge places of a primary (MergeCells), and Returned for one sent back from merging (spec section 7: the hidden returned column).

View Source 
const (
	SWaiting  = "waiting"
	SMerging  = "merging"
	SStopped  = "stopped"
	SLanded   = "landed"
	CConflict = "conflict"
	CCross    = "cross"
	CRed      = "red"
	CRejected = "rejected"
)

Stream states (the model's sstate) and the causes of a stop (spec section 7: conflict on a card, the branch red, a need of another stream's card, the merge queue rejected).

View Source 
const (
	Up           = "up"
	Down         = "down"
	Running      = "RUNNING"
	Stopped      = "STOPPED"
	KindPrimary  = "primary"
	KindSentinel = "sentinel"
)

Member status, the machine's states, and the kinds of a primary.

View Source 
const (
	JFailed    = "failed"           // work came back failed
	JBroken    = "broken"           // a reader found it broken
	JReads     = "reads"            // reads exhausted
	JStranded  = "stranded"         // stranded in review
	JAccept    = "accept"           // ready to accept
	JReturned  = "returned"         // returned to review
	JBlocked   = "blocked"          // a primary is blocked on something dropped
	JCI        = "ci"               // ci red
	JSkipped   = "skipped"          // repair skipped changes
	JConflict  = "stopped:conflict" // stream stopped: conflict on a card
	JRed       = "stopped:red"      // stream stopped: stream branch red
	JCross     = "stopped:cross"    // stream stopped: needs a card of another stream first
	JRejected  = "stopped:rejected" // stream stopped: the merge queue rejected
	JDone      = "done"             // the sprint is done
	JReached   = "reached"          // sentinel reached
	JNoMember  = "nomember"         // no fleet member is up (the tick's)
	JCannotAsk = "cannotask"        // cannot ask (the tick's)
	JBound     = "bound"            // a card reached its bound (the tick's)
)

Judgment types. The model's own (SprintTables.tla CardNoteTypes and StopNote) are failed, broken, reads, blocked, ci, skipped and the stopped notes; the rest are the spec's (section 8 and section 14).

View Source 
const (
	JBriefWrong     = "briefwrong"
	AttemptsDefault = 4
)

JBriefWrong is a card at its brief's bound: the brief is wrong, not the worker (sprint's AtBriefBound). AttemptsDefault is the attempts one brief may run when neither its stream nor the sprint sets a cap (sprint.AttemptsDefault).

View Source 
const (
	RefusedConflict = "conflict"
	RefusedPaths    = "paths"
	RefusedChecks   = "checks"
	RefusedGate     = "gate"
)

The ways the lander refuses a card's own head (sprint.RefusalWay): "" is a refusal it could not place, which stops the stream.

View Source 
const DealAhead = 2

DealAhead is how many widths of work cards a member holds, ready and working together: its width working and as many again ready behind them, so a member is dealt at most twice its width ahead (the engine's sprint.DealAhead).

View Source 
const MaxRedeals = 3

MaxRedeals is the spec's redeal bound (section 2): an attempt's work card is dealt again at most this many times after a take of it ended without a finish, its member down while it was working; a card that was ready keeps its count (sprint.MaxRedeals, tla/DirtyTick.tla RedealsAreEndedTakes).

View Source 
const Room = DealAhead * Width

Room is the most work cards a placement leaves on a member, ready and working together: DealAhead times its Width.

View Source 
const SprintSubject = "sprint:done"

Subjects that are not a primary.

View Source 
const Width = 64

Width is every member's width, the engine's default (sprint.DefaultWidth): the most work cards, ready and working together, the tick deals a member.

Variables

View Source 
var Duties = []Duty{
	{DutyLevel, LevelMoves},
	{DutyLevelReads, LevelReadsMoves},
	{DutyResolve, ResolveMoves},
	{DutyCapDeal, CapDealMoves},
	{DutyDeal, DealMoves},
	{DutyRebalance, RebalanceMoves},
	{DutyAccept, AcceptMoves},
	{DutyAsk, AskMoves},
	{DutyResume, ResumeMoves},
	{DutyStrangers, StrangerMoves},
	{DutyPresence, PresenceMoves},
	{DutyFriendStall, FriendStallMoves},
	{DutyCheck, CheckMoves},
	{DutyDeadlines, DeadlineMoves},
	{DutyOverdue, OverdueMoves},
	{DutyDone, DoneMoves},
	{DutyRemind, RemindMoves},
}

Duties is every duty of today's tick in the order the machine runs them.

Functions

func DefaultScore 

func DefaultScore(s State, a AddArgs, k int, prev float64) float64

DefaultScore is a score the model allows for the k-th id of an add: after every card of its stream, or between the neighbours of --before/--after.

func Equal 

func Equal(a, b []Move) (ok bool, diff string)

Equal says the two decisions are the same set of moves, whatever order they were given in, and if they are not, names the first card that differs: the first in canonical order, by the duty that decided it, with the moves each of the two has for it.

func Join 

func Join(xs []string) string

Join is a sorted list as one comma string, for printing.

func JudgmentType 

func JudgmentType(t string) string

JudgmentType is the model's name of an engine judgment type; a type the model has no name for is "other:" and the engine's words.

func Keys 

func Keys[V any](m map[string]V) []string

Keys lists a map's keys, sorted.

func RC 

func RC(p string, a int, r string) string

RC is a read card's id.

func StreamSubject 

func StreamSubject(s string) string

StreamSubject is a stream's subject.

func WC 

func WC(p string, a int) string

WC is a work card's id.

Types

type AddArgs 

type AddArgs struct {
	Stream        string
	IDs           []string
	Needs         []string
	Sentinel      bool
	Before, After string
}

AddArgs is add's arguments: new ids of one stream, the needs they name, whether the one id is a sentinel, and --before or --after a card.

type ChoiceError 

type ChoiceError struct{ Why string }

ChoiceError is a choice the caller made for an open choice of the model that the model does not allow (a card dealt to a member that is not the next round the fleet, a read asked of a reader that is not the next round the readers).

func (*ChoiceError) Error 

func (c *ChoiceError) Error() string

type Difference 

type Difference struct {
	Table  string // primary, work, read, merge, stream, member, open, acked, machine, epoch, pending
	ID     string
	Field  string
	Engine string
	Model  string
}

Difference is one field where the engine's abstract state and the model's differ.

func Compare 

func Compare(e, m State) []Difference

Compare lists every field where e (the engine, abstracted) and m (the model) differ, in a fixed order.

func (Difference) Sig 

func (d Difference) Sig() string

Sig is the difference without its ids: the table and the field, for grouping differences of one kind.

func (Difference) String 

func (d Difference) String() string

type Duty 

type Duty struct {
	Name string
	// Moves is the moves the duty makes on the snapshot at the time given,
	// in canonical order, none when the machine is STOPPED. It decides on a
	// clone: the snapshot is not changed.
	Moves func(s Snapshot, now time.Time) []Move
}

Duty is one duty of the tick: its name and the function that decides it.

type Judgment 

type Judgment struct {
	Type    string
	Subject string
}

Judgment is one open judgment on one subject: a primary, a stream (StreamSubject) or the sprint (SprintSubject).

func (Judgment) String 

func (j Judgment) String() string

type MergeCard 

type MergeCard struct {
	Place string // Queued, Merged, Stuck, Returned, or Gone
	Need  string
}

MergeCard is one primary's merge place, and a stuck card's cross-stream need (the model's need[p], D6).

type Move 

type Move struct {
	// Duty is the duty that decided it (Duties).
	Duty string
	Kind string
	// Table is the logical table of a change to a card, empty for the rest,
	// and Card is that card. For a note (an update too), Card is the card it
	// is about where it names one; for a close, the note's id; for a
	// reminder, the person; for a refusal, the card refused.
	Table string
	Card  string
	// From and To are the place of the card before and after, row:col, for
	// a change of place; From alone for a change in place. Score is the
	// score the change gives it, where it gives one.
	From, To string
	Score    string
	// Set and Unset are the fields a change sets (field=value) and unsets,
	// in name order; a bump is one Set entry (field+1).
	Set, Unset []string
	// Type, Stream, Subjects, Decisions, Attrs and Words are a note's: its
	// type, its stream, the cards (or the stream, or the sprint) it is open
	// on in name order, the decisions offered in the order given, the rest
	// of its fields (attr=value, in name order), and its words. An update
	// is a note's move with the id of the judgment it rewrites in its
	// attrs (id=). A refusal and a reminder use Words for theirs, and a
	// change to a card uses it for the one line of what moved. A note's id
	// (the store gives each its own) and its time (the time Decide is
	// given) are not carried.
	Type      string
	Stream    string
	Subjects  []string
	Decisions []string
	Attrs     []string
	Words     string
}

Move is one decision of one duty as data: a change to one card, a notification, an open judgment closing, a reminder, a count left due. Every field is text or a list of text, in a fixed form, so two moves are the same exactly when their String is. A field a kind does not use is empty.

func AcceptMoves 

func AcceptMoves(s Snapshot, now time.Time) []Move

AcceptMoves is the primaries in review with ok reads from two different readers moved to merging and queued to merge, in stream turns, and the note to the coordinator for each stream that got some: accept is mechanical, the merge is the coordinator's.

func AskMoves 

func AskMoves(s Snapshot, now time.Time) []Move

AskMoves is the primaries in review asked of two different readers, and the judgment for one that cannot be (T2).

func CapDealMoves 

func CapDealMoves(s Snapshot, now time.Time) []Move

CapDealMoves is the attempt cap's default answer: each machine's primary ready and past its stream's attempt cap dealt as a friend's card to the frontier or heavy friend up with the most room (Snapshot.Friends), her row's work card created in working and the brief gaining her WHO line; a card no such friend has room for is the deal's.

func CheckMoves 

func CheckMoves(s Snapshot, now time.Time) []Move

CheckMoves is a judgment for each rule that does not hold and each stall nothing holds, and the close of one whose rule holds again (T6).

func DeadlineMoves 

func DeadlineMoves(s Snapshot, now time.Time) []Move

DeadlineMoves is a judgment for each work card, read card and stream past its deadline in running time, and the close of one whose cause is gone (T5).

func DealMoves 

func DealMoves(s Snapshot, now time.Time) []Move

DealMoves is the ready primaries dealt, oldest first, to the members up with room, and the judgments for no member up and for a card at its redeal bound (T3).

func Decide 

func Decide(s Snapshot, now time.Time) []Move

Decide is every move one tick of today's scanning machine would make on the snapshot at the time given, in canonical order (duty, table, card, kind): the moves of each duty in Duties, each decided on the same snapshot. A tick runs its duties one after another, each on a fresh read that shows what the ones before it moved; Decide shows what each would do first, on the state as it stands, which is what a machine that finds every rule quiet compares with.

The snapshot is not changed, and the same snapshot at the same time gives the same moves. It is copied once, and every duty decides on that copy: the planners the duties call do not write to what they read. Each duty is held to the bounds of the tick (the units and judgments one part makes, the rest a KindDue move) and to what the store applies of a plan (sprint.Applied). What is decided from what the tick does, not from the tables, is left out: the repair of an operation the fence holds, the reminder's delivery and its outcome, and the display cells of the fleet.

func DoneMoves 

func DoneMoves(s Snapshot, now time.Time) []Move

DoneMoves is the note "the sprint is done", addressed to the coordinator, on a sprint with nothing open and a card landed or dropped, the condition the tick's judgment tickDone answers to. The machine's stop that goes with it is no move of the tables: the model's Tick has it (State.Machine), and the binding writes it on the machine's record.

func FriendStallMoves 

func FriendStallMoves(s Snapshot, now time.Time) []Move

FriendStallMoves is the friend stall ladder: each friend holding cards on her fleet row with no sign of life (session activity, a progress stamp, a deal) for the stall bound climbs one rung a step (two wake turns, a judgment for the coordinator, her unstarted cards taken back, marked down), every rung a notice and her rung a fleet property; a sign of life puts her back at rung 0, and session activity releases her when down.

func LevelMoves 

func LevelMoves(s Snapshot, now time.Time) []Move

LevelMoves is the newest ready cards moved from the largest backlog round the fleet while two backlogs differ by more than one, at the tick's start (T4).

func LevelReadsMoves 

func LevelReadsMoves(s Snapshot, now time.Time) []Move

LevelReadsMoves is the newest asked reads moved from the reader with the largest load round the readers while two loads differ by more than one, at the tick's start.

func OverdueMoves 

func OverdueMoves(s Snapshot, now time.Time) []Move

OverdueMoves is one overdue line and one hold for each judgment past its due time, and the close of a hold whose judgment closed.

func PlanMoves 

func PlanMoves(duty string, s *sprint.Snapshot, p sprint.Plan) []Move

PlanMoves is the moves of the plan p that the duty planned on the state s: the plan as data, in canonical order, converted as it is given. Decide's moves are those of plans held to what the store applies (sprint.Applied), so a machine that plans with the same planners as today's tick applies that to its plans first, and then converts them with this to compare them with Decide's.

func PresenceMoves 

func PresenceMoves(s Snapshot, now time.Time) []Move

PresenceMoves is the change of one member's status the beats call for (T0): a member that beats comes up and the ready queues are levelled, or one that does not goes down and its unfinished work cards are dealt to the members up or withdrawn.

func RebalanceMoves 

func RebalanceMoves(s Snapshot, now time.Time) []Move

RebalanceMoves is the rebalance after the deal: each work card dealt and not started, queued on a friend or a member whose lanes all work, moved to a unit of either side with an idle lane whose tiers and side's set admit it, the cheapest first (sprint.Rebalance).

func RemindMoves 

func RemindMoves(s Snapshot, now time.Time) []Move

RemindMoves is a push for each person whose reminder is due, and the judgments the failing routes call for or no longer call for. Whether a push arrives is the delivery's, not the decision's, so the judgments are those of the routes as the record has them.

func ResolveMoves 

func ResolveMoves(s Snapshot, now time.Time) []Move

ResolveMoves is the waiting primaries whose needs have all landed moved to ready, the sentinels whose needs have landed reached, and the judgments for a need dropped or missing (T1).

func ResumeMoves 

func ResumeMoves(s Snapshot, now time.Time) []Move

ResumeMoves is the streams stopped only on another stream's card, resumed once that card has landed (T7).

func Shape 

func Shape(ms []Move) []Move

Shape is the moves without their words: a machine that says the same in other words decides the same. What it does to the tables and to the judgments (the cards, places, fields, types, subjects and decisions) stays.

func StrangerMoves 

func StrangerMoves(s Snapshot, now time.Time) []Move

StrangerMoves is the notifications the coordinator is owed of the machines that beat and are no member of the fleet: told once each.

func (Move) String 

func (m Move) String() string

String is the move in one canonical line: the same moves give the same line, and two lines are equal exactly when the moves are.

type Observed 

type Observed struct {
	Snap    *sprint.Snapshot
	Pending string
	Machine string
}

Observed is what the engine's store holds, as read: the four tables (with the unplaced records of every card to be compared), the open judgments and the acknowledged conditions, the verb of the operation the fence holds, and the machine's state.

type Primary 

type Primary struct {
	Stream  string
	Kind    string   // primary or sentinel
	State   string   // a work cell, or Off
	Needs   []string // sorted
	Waived  []string // sorted: the dropped needs the coordinator waived
	Score   float64
	Attempt int      // the attempt of its current or next work card, from 1
	Head    int      // the attempt whose finished work is its head; 0 before
	Pair    []string // sorted: the readers of the reads that stand at its attempt (the work table's asked field)
	Reached bool     // a sentinel whose needs have all landed or been waived
	// CI and CIHead are its last CI observation: "", "red" or "green", and
	// the attempt whose head it was for (0: no head yet).
	CI     string
	CIHead int
	// ReturnedAt is the attempt at which the coordinator last returned it to
	// review, 0 when never (sprint.FieldReturnedAttempt).
	ReturnedAt int
	// Finder is the reader whose finding its last rework sent back and
	// FindingAttempt that attempt (sprint.FieldFindingReader, FieldFindingAttempt):
	// the next attempt's first read is asked of the finder, out of turn (Ask).
	Finder         string
	FindingAttempt int
	// BriefAt is its attempt when its brief was last replaced, 0 for the brief add gave it
	// (sprint.FieldBriefAttempt); Refused is the way the landing last refused its head when its
	// finding is that refusal (sprint.LandRefusedFinding), "" otherwise.
	BriefAt int
	Refused string
}

Primary is one primary's abstract record.

type ReadCard 

type ReadCard struct {
	Primary string
	Attempt int
	Reader  string
	Place   string // Asked, Reading, OK, Broken, Retired
	Verdict string // "", "ok" or "broken"
	Finder  bool   // asked of the finder out of turn: the level leaves it (sprint.FieldFinderRead)
}

ReadCard is one read card: <primary>.r<attempt>.<reader>.

type Refusal 

type Refusal struct{ Why string }

Refusal is an action the model does not allow in the state: the action's guard is false.

func (*Refusal) Error 

func (r *Refusal) Error() string

type Snapshot 

type Snapshot struct {
	// Tables is the four tables (unplaced records of the needs of waiting
	// primaries included, as the tick loads them), the open judgments and
	// the acknowledged conditions, the coordinator and the epoch. Its Now is
	// not read: the time is an argument of Decide.
	Tables *sprint.Snapshot
	// Running says the machine is RUNNING. A STOPPED machine moves nothing.
	Running bool
	// Since is when the machine last started: the first tick after it pushes
	// every reminder.
	Since time.Time
	// Stopped is the spans the machine was STOPPED: a deadline compares
	// running time, which leaves them out.
	Stopped []sprint.Span
	// Beats is each fleet member's last beat record; a member that never
	// beat has none. nil is none read, and the presence duty does nothing.
	Beats map[string]sprint.Beat
	// Goals is the sprint's people, their goals and routes.
	Goals sprint.Goals
	// Untold is the unknown machines that beat and whom the coordinator was
	// not told of yet.
	Untold []string
	// Friends is the friends' seats as the roster has them (name, width, status,
	// class): whom the cap deal and the deal give a friend's card. nil is none
	// read, and no friend is dealt a card; the friend stall reads her fleet row.
	Friends []sprint.FriendSeat
}

Snapshot is the whole state one tick of the scanning machine decides from: the four tables and the judgments open on them, and the few facts the tick reads beside them, which the store keeps outside the tables. It holds what the tick reads and nothing it writes, so a snapshot is the machine's whole input, and equal snapshots are decided alike.

func (Snapshot) Clone 

func (s Snapshot) Clone() Snapshot

Clone is a copy of the snapshot that shares nothing with it, so what is done to one is never seen in the other. Every duty decides on a clone, which is why deciding leaves the caller's snapshot as it was, whatever the planners do to what they read.

type State 

type State struct {
	Primaries map[string]Primary
	Work      map[string]WorkCard
	Reads     map[string]ReadCard
	Merge     map[string]MergeCard
	Streams   map[string]Stream
	Members   map[string]string // member -> Up or Down
	Order     []string          // the fleet's members in row order
	Readers   []string          // the readers in row order
	Open      map[Judgment]bool // the open judgments (D7)
	Acked     map[Judgment]bool // the tick's conditions acknowledged while they hold
	Machine   string
	Epoch     uint64
	Pending   string // the verb of the pending operation (D1), "" when none
	// Coordinator is the one actor who releases sentinels.
	Coordinator string
	// Cap is the sprint's attempt cap, 0 for none (sprint.PropAttempts).
	Cap int
	// DealLast and AskLast are the rolling indexes of the deal and the ask
	// (tla/SprintEvents.tla dcur and acur): each a
	// counter, as the table's property holds it (a decimal uint64 from 0 this
	// epoch, up by one with every placement and by one for every name passed
	// over, roundPast). The next member is the first up with room from
	// DealLast modulo the members in name order, wrapping; the next readers
	// the first able from AskLast modulo the readers.
	DealLast, AskLast string
	// Reserved is each reader's finder reads the tick's ask has placed in advance
	// (sprint.askFinders): counted in the reader's load (NextReaders) until the
	// primary's own Ask places the read, as the engine takes every finder's read
	// off its room before any other read of the step. nil outside the tick's ask.
	Reserved map[string]int
	// StreamLast, AskStreamLast and AcceptStreamLast are the work table's
	// stream indexes of the deal, the ask and the accept (sprint.PropStreamIndex,
	// PropAskStreamIndex, PropAcceptStreamIndex):
	// the stream of the last primary each took. Each takes the streams in
	// turn from the first past its own, in name order, wrapping, a stream with
	// nothing to take skipped.
	StreamLast, AskStreamLast, AcceptStreamLast string
}

State is the abstract state of one sprint.

func Abstract 

func Abstract(o Observed) State

Abstract maps what the engine's store holds to the model's state, and nothing more: each field of State from the one record that holds it.

The mapping's conventions: a primary's attempt is its work card's attempt, 1 before its first card is cut (the model's attempt starts at 1), and the next one while it is ready or waiting after its card was finished (rework with no member up); its head is the attempt of the work card its head names (the differential test finishes with no head of its own, so the head is the card); an unplaced record is a primary off the table, a work card gone, a read card retired, a merge place gone; a stream's cause is read only while it is stopped; the tick's no-member judgment is on the subject "fleet"; overdue holds are the clock's and are left out.

func Accept 

func Accept(s State, set []string) (State, error)

Accept is SprintTables.tla Accept(S) (line 436): named, all or nothing (D4): review -> merging and into merge queued; refused unless every one has two different readers ok at its head. Its asked and reading read cards retire (F1); a stream not stopped becomes merging (G4); its card judgments close.

func Ack 

func Ack(s State, typ string, subjects []string, waive []string) (State, error)

Ack is SprintTables.tla Ack(n) (line 667) on every subject of one notification: the coordinator looked and nothing is to be done; refused for a stopped stream's judgment while the stream is stopped (F3). The ack that leaves a primary in review with no judgment writes its exhausted or stranded judgment (G3), unless it acknowledged that judgment itself.

ack answers only a judgment whose own decisions list it (section 8's table): ci red, blocked (the ack waives the dropped needs), and repair skipped; every other is refused. The tick's conditions are held by wait.

waive is, for a blocked judgment, the dropped needs its notification names: the ack waives those (Waive, line 298), and the blocked judgment closes only when no dropped need of the primary is left unwaived.

func Add 

func Add(s State, a AddArgs, scores map[string]float64) (State, error)

Add is SprintTables.tla Add(p) (line 276) for each id in order: admitted waiting if a need is not met, else ready; refused when the needs make a cycle (NoNeedCycle); the blocked judgment when a need was dropped. scores is the choice of each new id's score (the model's Score0, a constant there).

Sentinels by position, add --before/--after, a sentinel pulling ready cards back to waiting are from the spec (section 16), not yet in the model. An add opens no sprint-done judgment to close: the sprint done is the tick's judgment tickDone, fired when nothing remains open and a card has landed or dropped — an add neither lands nor drops a card.

func Ask 

func Ask(s State, p string, readers []string) (State, error)

Ask is SprintTables.tla Ask(p) (line 375) with the reads asked one at a time and by room (spec section 6; tla/ReadsByRoom.tla): a primary in review whose work did not fail is dealt the reads it wants now (ReadsWanted: its first read alone while none stands, the second once the first came back ok, none while one is outstanding or found it broken) to the readers AskChoice names: the finder first on a rework's next attempt, out of turn, the rolling index not moved for it; else the least loaded readers (NextReaders, the engine's room for readers with no width), the index moved past them. Reworked work is asked the same way, at its new attempt, with no reader of an earlier attempt preferred, the finder aside, and none skipped for it. Its pair is the readers of the reads that stand. It closes stranded in review.

func AskAnother 

func AskAnother(s State, p, r string) (State, error)

AskAnother is SprintTables.tla AskAnother(p, r) (line 397): one more reader for a primary in review (free, F1, FreeCoordinator); it answers a broken read and reads exhausted. Refused for work that came back failed and for a primary not asked yet at its attempt: the spec's section 6 ("work that came back failed is not read"; "ask --another deals a primary already asked to one more reader"), which the model's AskAnother does not guard.

func CiGreen 

func CiGreen(s State, p string) (State, error)

CiGreen is the spec's green observation (section 8): a happened note; on the current head it resolves a red one, and when that closes the primary's last judgment in review the exhausted or stranded judgment is written (section 6). From the spec, not yet in the model.

func CiRed 

func CiRed(s State, p string) (State, error)

CiRed is SprintTables.tla CiRed(p) (line 654): a red CI observation on a placed primary in any state opens the ci judgment and moves nothing.

func Clear 

func Clear(s State) (State, error)

Clear is the spec's clear (section 13): the machine STOPPED, the epoch advanced once; at the new epoch every table is empty with the same rows, every stream waiting, every member with its status and no work; the judgments and the fence are the new epoch's own, empty. The coordinator is the sprint's and is kept. From the spec, not yet in the model.

func Crash 

func Crash(pre, post State, verb string) State

Crash is SprintTables.tla Crash (line 687): the process writing a step over more than one table is cut before its last write, the work table; the operation stays pending. The state it leaves is the step's (post) but for the work table, which holds every primary's record, and the judgments, which open and close at the release.

func Drop 

func Drop(s State, p string) (State, error)

Drop is SprintTables.tla Drop(p) (line 478): off the table. Its unfinished work card is withdrawn, its outstanding read cards retire, its merge place goes (the returned place too, spec section 7); work last. A waiting primary that needs it makes the drop refused, naming the dependants: the real Drop without Cascade refuses for that card, and this model matches it (docs/SPEC-SPRINT.md section 11). Every judgment on it closes. A sprint it finishes, by dropping the last open card, is found done by the tick's judgment tickDone: with nothing open and a card dropped, the sprint is done.

func Finish 

func Finish(s State, m, c string, gen int, ok bool) (State, error)

Finish is SprintTables.tla Finish(m, c, g, v) (line 340), and FinishRefused (line 364) when the generation is not live: accepted only for the live generation in its member's working cell (D3); the card to done, its primary to review at the head the card produced; failed opens the failed judgment. ok asks no reader: one path asks (the engine's commit 255180e2), the machine's Ask, which asks round the readers.

func FleetDown 

func FleetDown(s State, m string, dest map[string]string) (State, error)

FleetDown is SprintTables.tla FleetDown(m) (line 603): the member goes down; its unfinished work cards are dealt to up members at a new generation; with no member up they are withdrawn (a new generation) and their primaries return to ready. dest is the choice, card to member: each card, in work order, must go to the next member round the fleet at that moment (PlaceOn: every placement moves the index).

func FleetUp 

func FleetUp(s State, m string, moves map[string]string) (State, error)

FleetUp is SprintTables.tla FleetUp(m) (line 637): the member comes up and the ready queues are levelled in one call; the newest cards move at a new generation. moves is the choice, card to member; Level holds it to the spec's rule (section 14, T4). The model's FleetUp is enabled only for a member that is down; the spec says nothing of up for a member that is up, and here it is the levelling alone (as fleet level).

func Level 

func Level(s State, moves map[string]string) (State, error)

Level is the fleet verb level and the tick's T4 (spec section 14): the up members' ready queues are evened when two differ by more than one, the newest cards going round the fleet (levelRound). From the spec, not yet in the model (whose FleetUp moves half of the longest queue).

func MergeGreen 

func MergeGreen(s State, stream string, batch int) (State, error)

MergeGreen is SprintTables.tla MergeGreen(s, B) (line 532), given the fact green: the batch is the first n of the stream's queued cards in score order (a prefix: section 7, 1), and lands. The same step moves every waiting primary whose needs have all landed to ready and marks reached every sentinel whose needs have all landed (spec section 7). A sprint it finishes, by landing the last open card, is found done by the tick's judgment tickDone: with nothing open and a card landed, the sprint is done.

func MergeRed 

func MergeRed(s State, stream string, rejected bool) (State, error)

MergeRed is SprintTables.tla MergeRed(s) (line 569): the branch red or the merge queue rejected the batch; the stream stops, no card moves, the coordinator is told.

func MergeRefused 

func MergeRefused(s State, stream string, batch int, p, way string) (State, error)

MergeRefused is a conflict fact on card p of the batch (the first n queued), the landing's refusal of its head the way way (sprint.RefusalWay, sprint's landRefused). A way the lander could not place ("") is its own failure and stops the stream (MergeStop). Any other is the card's own and never stops the stream: the card leaves merge, returned at its attempt, every judgment on it closing, and the stream's state follows (G4). Files outside its PATHS (RefusedPaths) go back to review under returned to review, for the widen rule; at its brief's bound (AtBriefBound) the card goes back to review with the bound's judgment; else its read cards retire and its next attempt waits ready, the way its finding.

func MergeStop 

func MergeStop(s State, stream string, batch int, p, cause, q string) (State, error)

MergeStop is SprintTables.tla MergeStop(s, p, why, q) (line 551): a fact on card p of the batch (the first n queued) stops the stream: a conflict, or its need of card q of another stream first (D6), refused unless q is placed, in another stream and not landed (F4). The card goes to stuck, the stream stops, the coordinator is told.

func New 

func New(readers, members []string, coordinator string) State

New is an empty sprint with its readers and members, every member down, the machine STOPPED.

func Rank 

func Rank(s State, p string, score float64) (State, error)

Rank is SprintTables.tla Rank(p) (line 501): ranks a card first, refused for a landed primary (G6). score is the choice: below every other primary of its stream on the table (the spec's "first": ahead of every primary of its stream).

func Read 

func Read(s State, r, c string, ok bool) (State, error)

Read is SprintTables.tla Read(r, c, v) (line 418): a reader records ok or broken; a report against a retired card is refused. Broken opens the broken judgment; the read that leaves the reads exhausted opens reads exhausted (G3). A report on a card still asked is the begin and the report in one step, and the read that completes two different readers' ok at the head opens ready to accept only for a primary the pump holds (AcceptHeld); the tick accepts the rest, RUNNING or STOPPED (at the first pump after start): both the spec's (section 6), not the model's.

func ReadStart 

func ReadStart(s State, r, c string) (State, error)

ReadStart is SprintTables.tla ReadStart(r, c) (line 408): a reader moves its own read card asked -> reading.

func Release 

func Release(s State, ids []string, who string) (State, error)

Release is the spec's release (section 16): the coordinator alone lands reached sentinels (waiting -> landed, the only step that may), and in the same step moves every waiting primary whose needs are all met to ready and marks reached every sentinel now due; it closes the judgments open on each sentinel; the stream's state follows (section 7: landed when every primary of it on the table has landed). From the spec, not yet in the model.

func Repair 

func Repair(post State) State

Repair is SprintTables.tla Repair (line 695) after Crash: the work-table write is applied from the operation record, where its expectation holds, and the operation releases. Continue (line 679) is the same write by the same process; a step that is not cut is Continue at once, so the action functions above return the state after Continue.

func Resolve 

func Resolve(s State, p string) (State, error)

Resolve is SprintTables.tla Resolve(p) (line 288): waiting -> ready where every need has landed or was waived. A sentinel never moves (spec section 16). The blocked judgment for a dropped need is the spec's (section 8, "Resolve ... a need that was dropped is a judgment, once"), not in the model's Resolve.

func Resume 

func Resume(s State, stream, did string) (State, error)

Resume is SprintTables.tla Resume(s) (line 585) with what was done (--did): refused while a stuck card's cross-stream need has not landed (D6), and after a red branch without --did (spec section 7). The stuck cards go back to queued; the stream's state follows; the stream's judgment closes (D5).

func Return 

func Return(s State, p string) (State, error)

Return is SprintTables.tla Return(p) (line 513): merging -> review; the card leaves merge queued or stuck, into returned (spec section 7), with its need; the stream's state follows (G4); it answers the card's red CI and a skipped repair (F3), and opens returned to review (spec section 7, not in the model); the primary is marked returned at its attempt, which the machine's accept holds (AcceptHeld).

func Rework 

func Rework(s State, p, m string) (State, error)

Rework is SprintTables.tla Rework(p) (line 456): the primary's read cards retire; with a member up the next work card is cut into m, which must be the next member round the fleet (ReworkChoice: the member of the attempt's work card avoided unless no other has room; the index moved past it), and the primary goes review -> working; with none up (m is "") review -> ready; its card judgments close.

func SetMachine 

func SetMachine(s State, running bool) (State, error)

SetMachine is start and stop (spec section 14): the machine's state; the state it has already changes nothing. From the spec, not yet in the model.

func Start 

func Start(s State, p, m string, limit int) (State, error)

Start is SprintTables.tla Start(p) (line 310): ready -> working; the work card of the attempt is dealt to m, which must be the next member round the fleet (NextMember; the rolling index moved past it): a new work card is cut at generation 1, or, when the card was withdrawn by a member going down or a levelling, the same card is dealt again at a new generation. limit, when above zero, is the tick's Width: only members holding fewer work cards, ready and working, are dealt to.

func Take 

func Take(s State, m, c string, gen int) (State, error)

Take is SprintTables.tla Take(m, c) (line 326): the worker on an up member moves a work card ready -> working at its generation (F2: a take by id names the generation; a stale one is refused).

func Tick 

func Tick(s State, ch TickChoices) (State, error)

Tick is one tick of the machine (spec section 14): a STOPPED machine moves nothing; a RUNNING one runs its parts in order, each on the state the one before left: the start, the fleet's level (T4) and the readers' (levelReads), once; then the four tables' updates in the owner's order: the work pump's resolve (T1), deal (T3) and accept (mechanical: the machine applies the rule, no judgment), the readers' ask (T2), the merge's resume (T7); and then done, which stops the machine on a done sprint. The tables the updates dirty are updated again until none is; the model's parts dirty no earlier table, so one pass is the fixpoint. The check, deadline and overdue parts write nothing while the rules hold and no clock deadline passes, which the differential test keeps so. From the spec, not yet in the model (the model's Resolve, Start, FleetUp and Ask happen one at a time, in any order).

func Waive 

func Waive(s State, p string, qs []string) (State, error)

Waive is SprintTables.tla Waive(p, q) (line 298) for every dropped need of p the blocked judgment names: the need counts as met. The model closes the blocked judgment when no dropped need is left unwaived. In the spec the coordinator waives by ack of the blocked judgment (section 8); Ack calls it.

func (State) AcceptHeld 

func (s State) AcceptHeld(p string) string

AcceptHeld is why the machine's accept leaves an acceptable primary in review for the coordinator (sprint.AcceptHeld): its CI red at its head, or returned to review at its attempt; "" when the machine accepts it.

func (State) Acceptable 

func (s State) Acceptable(p string) bool

Acceptable is SprintTables.tla Acceptable(p) (Broken = "none").

func (State) AskChoice 

func (s State) AskChoice(p string) (readers []string, finder bool)

AskChoice is the readers the ask asks p of now (ReadsWanted), and whether the first is the finder out of turn (sprint.finderFirst, sprint.askPicks): p's first read goes to the reader whose finding the attempt's fix answers when that reader has no card at the attempt (the model's readers have no width, so the finder always has room); every other read to the least loaded reader without a card at the attempt (NextReaders). The finder's read counts in its load (Load) like any read, and in the tick's ask from the step's start (Reserved), so no turn is kept for it.

func (State) AskID 

func (s State) AskID(p string, a int, r string) (string, bool)

AskID is the read card the ask cuts for reader r of p at attempt a, and whether r may be asked (sprint.ReadCardForAsk, the interim rule of 2026-10-06): the plain id while none is made; the second identity (.g1) once the plain card is retired without a verdict and no second is made; else r has read it.

func (State) AskedLen 

func (s State) AskedLen(r string) int

AskedLen is SprintTables.tla AskedLen(r).

func (State) AskedNow 

func (s State) AskedNow(p string) bool

AskedNow is SprintTables.tla AskedNow(p): a read card of p's attempt was made (placed or retired).

func (State) AtBound 

func (s State) AtBound(p string) string

AtBound is the primary's withdrawn work card when it is at its redeal bound, "" when it is not.

func (State) AtBriefBound 

func (s State) AtBriefBound(p, way string) bool

AtBriefBound says the landing's refusal of the primary's head the way way is at its brief's bound (sprint.AtBriefBound): the same refusal as the one its last rework answered, at an attempt since its brief was replaced, or its stream's attempt cap counted from that brief.

func (State) AttemptsCap 

func (s State) AttemptsCap(stream string) int

AttemptsCap is how many attempts one brief may run in the stream (sprint's AttemptsCap): the stream's cap, else the sprint's, else AttemptsDefault.

func (State) Backlog 

func (s State) Backlog(m string) int

Backlog is a member's work cards held, ready and working, less its Width: below zero it has lanes its ready cards do not fill, above zero it holds ready cards it cannot start.

func (State) Clone 

func (s State) Clone() State

Clone is a deep copy.

func (State) DroppedNeeds 

func (s State) DroppedNeeds(p string) []string

DroppedNeeds is the needs of p that were dropped and are not waived.

func (State) Failed 

func (s State) Failed(p string) bool

Failed is SprintTables.tla Failed(p).

func (State) HasBefore 

func (s State) HasBefore(p string) bool

HasBefore says sentinel p has something to be reached after (spec section 16): a need it names, or a primary of its stream on the table, landed or not, that sorts before it. One with nothing before it is reached only when no other work is in flight (Reachable).

func (State) Held 

func (s State) Held(m string) int

Held is the member's work cards held against its width: ready and working.

func (State) InWork 

func (s State) InWork(p, c string) bool

InWork is SprintTables.tla InWork(p, c).

func (State) LiveReadsOf 

func (s State) LiveReadsOf(p string) []string

LiveReadsOf is p's read cards on the table in any cell (SprintTables.tla LiveReads restricted to p).

func (State) Load 

func (s State) Load(r string) int

Load is a reader's reads asked and reading together, the engine's readerLoad.

func (State) MergeCell 

func (s State) MergeCell(stream, place string) []string

MergeCell is the stream's primaries in a merge place, in work order.

func (State) NeedsMet 

func (s State) NeedsMet(p string) bool

NeedsMet is SprintTables.tla NeedsMet(p): every need has landed, or was dropped and waived.

func (State) NextMember 

func (s State) NextMember(set []string) string

NextMember is the deal's choice (SprintEvents.tla RoundAssign): the first of the members, in name order from just past DealLast, wrapping, that is in set; "" when none is.

func (State) NextReaders 

func (s State) NextReaders(p string, k int) []string

NextReaders is the ask's choice of k readers for p at its attempt: the reader with the most free room among those without a read card at the attempt, a tie going to the first from just past AskLast, in name order, wrapping (SprintEvents.tla RoundTwo), then the one with the most room left past it, and so on. The model's readers have no width (none is named for a fleet row), so the room is unbounded and ordered by the load alone, reads asked and reading (Load), the engine's readerRooms and round.pickByRoom.

func (State) OkReaders 

func (s State) OkReaders(p string) []string

OkReaders is SprintTables.tla OkReaders(p): the readers with an ok read card at p's head.

func (State) OpenOn 

func (s State) OpenOn(subject string) bool

OpenOn says a judgment is open on the subject.

func (State) OutOf 

func (s State) OutOf(p string) []string

OutOf is SprintTables.tla OutOf(p): p's read cards asked or reading.

func (State) PlaceOn 

func (s State) PlaceOn(set []string, avoid string) string

PlaceOn is the member a card placed on the fleet goes to (every placement, first attempts and redeals and levelling alike, goes round the fleet and moves the index; the engine's round.next): the next member round the fleet among set holding fewer work cards, ready and working, than its Room (DealAhead), avoid only when no other has room; with none having room, the next of set, avoid only when it is the only one. "" when set is empty.

func (State) Placedp 

func (s State) Placedp(p string) bool

Placedp is SprintTables.tla Placedp(p): admitted and not dropped.

func (State) PositionWaits 

func (s State) PositionWaits(p string) []string

PositionWaits is what p waits for by its place in its stream's order (spec section 16): a sentinel, every primary before it on the table that has not landed; a waiting primary, the latest unlanded sentinel before it. Nothing of it is stored as a need.

func (State) RL 

func (s State) RL(m string) int

RL is SprintTables.tla RL(m): the member's ready queue length.

func (State) Reachable 

func (s State) Reachable(p string) bool

Reachable says sentinel p, its needs met, is reached now (spec section 16): something came before it, or no other work of the sprint is in flight.

func (State) ReaderLoad 

func (s State) ReaderLoad(r string) int

ReaderLoad is a reader's reads asked and reading.

func (State) ReadsWanted 

func (s State) ReadsWanted(p string) int

ReadsWanted is how many reads the ask places on p now (sprint.ReadsWanted, reads together, the interim rule of 2026-10-06: "send out multiple consumer cards in ||"): the rest of the two it needs, an outstanding read counted among them, none while one found it broken.

func (State) ReworkChoice 

func (s State) ReworkChoice(p string) string

ReworkChoice is the member a rework of p deals its next attempt to (PlaceOn over the members up, avoiding the member of the attempt's work card); "" when no member is up.

func (State) StreamNames 

func (s State) StreamNames() []string

Streams is the streams in name order.

func (State) StreamOrder 

func (s State) StreamOrder(stream string) []string

StreamOrder is the stream's primaries on the table, in work order (score, then id).

func (State) Up 

func (s State) Up() []string

Up is SprintTables.tla Up, in row order.

type Stream 

type Stream struct {
	State string
	Cause string
	Cap   int // its attempt cap, 0 for none (sprint.FieldAttempts)
}

Stream is one stream's merge state and the cause of its stop.

type TickChoices 

type TickChoices struct {
	Deal  map[string]string
	Level map[string]string
	Ask   map[string][]string
}

TickChoices is the choices a tick makes: the member each primary is dealt to, the member each levelled card moves to, and the two readers each primary is asked of. A primary the choices do not name is dealt or asked by the first allowed choice in row order.

type WorkCard 

type WorkCard struct {
	Primary string
	Attempt int
	Member  string
	Place   string // FReady, FWorking, FDone, FWithdrawn, Gone
	Gen     int
	OK      string // "", "ok" or "failed"
	// Redeals is how many times the attempt was dealt again after a take of
	// it ended without a finish (spec section 2): a working card whose member
	// goes down at MaxRedeals stays withdrawn and the bound's judgment names
	// its primary. TakeEnded marks a card withdrawn after such a take: the
	// deal that places it again counts it (sprint.FieldTakeEnded).
	Redeals   int
	TakeEnded bool
	// Refusers is the members that refused the card at staging
	// (sprint.StagingRefusers): the level never moves it onto one.
	Refusers []string
}

WorkCard is one work card: <primary>.w<attempt>.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.