goat

package module
v0.6.0 Latest Latest
Warning

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

 Go to latest Published: Mar 13, 2026 License: Apache-2.0 Imports: 12 Imported by: 0

README

goat

What is goat

goat is a Design as Code library for Go. You write software design — components, states, behaviors, and interactions — as Go code, not documents.

A goat specification is executable. goat can model check it by exploring every possible execution order and verifying your rules against every reachable state. It can also generate schemas (Protocol Buffers, OpenAPI) from the same specification.

Design written as code doesn't drift from implementation. It lives in your repository and you can verify it by running it.

How goat Models Systems

goat models a system as a composition of state machines that communicate through events.

Every component — a server, a client, a database, a message broker — becomes a state machine with discrete states. A server might be initializing or running. By adding states like crashed or unavailable, you can verify how the rest of the system behaves under failure.

State machines communicate by sending events through queues. Events are asynchronous — the sender doesn't wait for the recipient to process the event. This directly models how distributed systems communicate through HTTP requests, message queues, gRPC calls, and database queries.

Handlers define what a state machine does when it enters a state or receives an event: update its data, transition to another state, or send events to other machines.

Real systems are non-deterministic. For example, a request might return a successful response or an error. goat models this with multiple handlers for the same state and event, one per possible outcome. goat explores every path across all machines.

What goat Checks

goat verifies two kinds of properties:

Safety — "this bad thing never happens." For example, an account balance never goes below zero. In goat, you write this as Always(condition): the condition must hold in every reachable state. If there is a violation, goat can show it as a finite sequence of steps leading to the bad state.

Liveness — "this good thing eventually happens." For example, whenever an order is paid, it is eventually shipped. goat provides temporal rules for this:

  • WheneverPEventuallyQ(p, q) — whenever p becomes true, q must eventually become true.
  • EventuallyAlways(c) — the system eventually reaches a state where c holds permanently.
  • AlwaysEventually(c) — c keeps becoming true repeatedly, forever.

When goat finds a violation, it reports the exact sequence of steps — which machine processed which event in which order — so you can see the concrete scenario your system can hit.

Writing Specifications

A goat specification is written in three steps:

  1. Define state machine and event schemas — What components exist, what states they can be in, and what messages they exchange.
  2. Define rules — What properties the system must satisfy.
  3. Define handlers — How each component behaves. What it does when it enters a state or receives an event.
Defining State Machine and Event Schemas

A state is a struct that embeds goat.State. Fields distinguish one state from another:

type MyState struct {
    goat.State
    Status string
}

var (
    stateA = &MyState{Status: "A"}
    stateB = &MyState{Status: "B"}
)

A state machine is a struct that embeds goat.StateMachine. Add fields for any domain data the component carries:

type Server struct {
    goat.StateMachine
    ConnectionCount int
}

An event is a struct that embeds goat.Event[Sender, Recipient]. The type parameters specify which state machine sends and which receives:

type Request struct {
    goat.Event[*Client, *Server]
    Payload string
}

Create a specification, define the possible states, and set the initial state:

spec := goat.NewStateMachineSpec(&Server{})
spec.DefineStates(stateA, stateB).SetInitialState(stateA)

Create instances from a spec. Each instance is an independent state machine. Every unit of work that can run concurrently needs its own instance — if a server handles two requests in parallel, that is two server instances, even on a single machine:

db, _ := dbSpec.NewInstance()
server1, _ := serverSpec.NewInstance()
server2, _ := serverSpec.NewInstance()
client1, _ := clientSpec.NewInstance()
client2, _ := clientSpec.NewInstance()

The model checker explores every interleaving of events across all instances.

To send an event to another machine with SendTo, the sender needs a reference to the target. Store it as a field and assign it after creating instances:

type Client struct {
    goat.StateMachine
    Server *Server
}

client, _ := clientSpec.NewInstance()
server, _ := serverSpec.NewInstance()
client.Server = server

Pointer fields like Server *Server serve as references to other machines and are not included in state comparison or verification. Do not use pointer fields for domain data. Fields of type int, string, map, slice, and structs work.

Defining Rules

A condition is a named boolean check on one or more state machines. A rule takes a condition and specifies how to verify it — always true, eventually true, and so on.

Conditions on a single machine

NewCondition creates a condition that inspects one state machine. The check function receives the typed machine instance:

cond := goat.NewCondition("non-negative", sm, func(sm *MyMachine) bool {
    return sm.Count >= 0
})
Conditions on multiple machines

When a property involves more than one machine, use NewCondition2 or NewCondition3:

goat.NewCondition2("a-b-consistent", smA, smB, func(a *MachineA, b *MachineB) bool {
    return a.Value == b.Value
})

goat.NewCondition3("triple", smA, smB, smC, func(a *MachineA, b *MachineB, c *MachineC) bool {
    return a.Total == b.Total+c.Total
})

For four or more machines, use NewMultiCondition. The check function receives a Machines accessor, and you retrieve each machine with GetMachine:

goat.NewMultiCondition("all-ready", func(machines goat.Machines) bool {
    a, ok := goat.GetMachine(machines, smA)
    if !ok { return false }
    b, ok := goat.GetMachine(machines, smB)
    if !ok { return false }
    c, ok := goat.GetMachine(machines, smC)
    if !ok { return false }
    d, ok := goat.GetMachine(machines, smD)
    if !ok { return false }
    return a.Ready && b.Ready && c.Ready && d.Ready
}, smA, smB, smC, smD)
Building rules from conditions

Pass conditions to a rule constructor to specify what the model checker verifies.

Always — the condition must hold in every reachable state:

goat.Always(nonNegative)

WheneverPEventuallyQ — whenever condition p holds, condition q must eventually hold:

goat.WheneverPEventuallyQ(requested, completed)

EventuallyAlways — the condition must eventually become true and stay true permanently:

goat.EventuallyAlways(stable)

AlwaysEventually — the condition must keep becoming true repeatedly, forever:

goat.AlwaysEventually(ready)
Defining Handlers

Handlers define what a state machine does when it enters a state or receives an event.

Entry handlers

OnEntry registers a handler that runs when a state machine enters a given state:

goat.OnEntry(spec, stateA, func(ctx context.Context, sm *MyMachine) {
    sm.Count = 0
    goat.Goto(ctx, stateB)
})
Event handlers

OnEvent registers a handler that runs when a state machine receives a specific event in a given state:

goat.OnEvent(spec, stateA, func(ctx context.Context, event *MyEvent, sm *MyMachine) {
    sm.Count += event.Amount
    goat.SendTo(ctx, event.Sender(), &MyResponse{Total: sm.Count})
    goat.Goto(ctx, stateB)
})
Actions inside handlers

Handlers use context functions to perform actions:

  • goat.Goto(ctx, state) — transition to another state.
  • goat.SendTo(ctx, target, event) — send an event to another state machine. The target is either a field on the machine (sm.Server) or event.Sender() to reply to whoever sent the event.
  • goat.Halt(ctx, target) — stop a state machine permanently.

Every received event exposes Sender() and Recipient(), typed to the machines declared in Event[Sender, Recipient]. Use event.Sender() to reply without needing a stored reference.

Handlers can also update the state machine's fields directly, as shown above with sm.Count.

Non-determinism

Registering multiple handlers for the same state and event models non-determinism. The model checker explores every handler as a separate execution path:

goat.OnEvent(spec, stateA, func(ctx context.Context, event *Request, sm *MyMachine) {
    goat.SendTo(ctx, event.Sender(), &Response{OK: true})
})
goat.OnEvent(spec, stateA, func(ctx context.Context, event *Request, sm *MyMachine) {
    goat.SendTo(ctx, event.Sender(), &Response{OK: false})
})

This works with any handler type, not just OnEvent. For example, two OnEntry handlers for the same state create two possible paths on entry.

Other handler types
  • goat.OnExit(spec, state, fn) — runs when leaving a state.
  • goat.OnTransition(spec, state, fn) — runs during a transition, after exit and before entry. The callback receives the target state as an additional argument.
  • goat.OnHalt(spec, state, fn) — runs when the state machine is halted.
Running Model Checking

goat.Test runs the model checker. Pass options to specify which state machines to check and which rules to verify:

result, err := goat.Test(
    goat.WithStateMachines(server, client),
    goat.WithRules(
        goat.Always(nonNegative),
        goat.WheneverPEventuallyQ(requested, completed),
    ),
)

WithStateMachines takes the state machine instances to include in the model. WithRules takes the rules defined with Always, WheneverPEventuallyQ, and the other rule constructors.

The model checker explores every reachable combination of state machine states and queued events. This combination is called a world. Test checks all rules against every world and returns a *Result.

result.HasViolation() reports whether any rule was violated. result.Violations is a list of Violation, each with Rule (the violated rule), Path and Loop. For safety violations (Always), Path is the sequence of worlds from the initial state to the violating state, and Loop is nil. For other rules, the violating execution is an infinite path that eventually repeats. Path is the non-repeating prefix and Loop is the repeating part. result.Summary contains TotalWorlds (how many worlds were explored) and ExecutionTimeMs.

Test also prints results to stdout. When a violation is found, it prints the path to the violating state — which machine was in which state at each step — so you can trace the exact scenario:

Condition failed. Not Always non-negative.
Path (length = 3):
  [0]
  StateMachines:
    Name: Server, Detail: {Count: 0}, State: idle
  [1]
  StateMachines:
    Name: Server, Detail: {Count: -1}, State: processing  <-- violation here

When no violations are found, Test prints a summary with the total number of explored states and execution time.

Examples

The example directory contains runnable specifications:

Documentation

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func Debug 

func Debug(w io.Writer, opts ...Option) error

Debug performs model checking and outputs detailed JSON results. Unlike Test(), this function provides comprehensive debugging information including all explored worlds and their states in JSON format.

Parameters:

  • w: Writer to output the JSON results to
  • opts: Configuration options including state machines and invariants

Returns an error if model creation, solving, or JSON encoding fails.

Example: 

var buf bytes.Buffer
err := goat.Debug(&buf, goat.WithStateMachines(sm), goat.WithRules(goat.Always(cond)))
fmt.Println(buf.String()) // JSON output

func GetMachine added in v0.2.0 

func GetMachine[T AbstractStateMachine](m Machines, sm T) (T, bool)

GetMachine provides type-safe access to a state machine from Machines.

Parameters:

  • m: Machines accessor provided to the check function
  • sm: A sample instance used to identify the target machine by ID

Returns the typed state machine and true on success. Returns the zero value and false when the machine does not exist or the type does not match.

Example: 

machine, ok := goat.GetMachine(machines, client)
if !ok { return false }
state := machine.currentState().(*ClientState)

func Goto 

func Goto(ctx context.Context, state AbstractState)

Goto triggers a state transition for the current state machine. This function must be called from within event handlers registered with OnEvent, OnEntry, OnExit, OnTransition, or OnHalt functions. It automatically generates the necessary sequence of events (Exit, Transition, Entry).

Parameters:

  • ctx: Context passed to the event handler
  • state: The target state to transition to

Example: 

goat.OnEvent(spec, IdleState{}, func(ctx context.Context, event Event, sm *MyStateMachine) {
    goat.Goto(ctx, &ActiveState{Ready: true})
})

func Halt 

func Halt(ctx context.Context, target AbstractStateMachine)

Halt stops the execution of a specific state machine permanently. This function must be called from within event handlers registered with OnEvent, OnEntry, OnExit, OnTransition, or OnHalt functions. It triggers the haltEvent and any associated cleanup handlers.

Parameters:

  • ctx: Context passed to the event handler
  • target: The state machine to halt

Example: 

goat.OnEvent(spec, ActiveState{}, func(ctx context.Context, event Event, sm *MyStateMachine) {
    goat.Halt(ctx, sm) // Stop this state machine
})

func NewHandlerContext added in v0.5.0 

func NewHandlerContext(sm AbstractStateMachine) context.Context

NewHandlerContext creates a context with a minimal environment for executing handlers. This is used when you need to execute handlers outside of the normal model checking flow.

Parameters:

  • sm: The state machine instance to include in the context

Returns a context that can be used with SendTo, Goto, and other handler functions.

Example: 

instance, _ := spec.NewInstance()
ctx := goat.NewHandlerContext(instance)
response := handler(ctx, input, instance)

func OnEntry 

func OnEntry[SM AbstractStateMachine](
	spec *StateMachineSpec[SM],
	state AbstractState,
	fn EntryHandler[SM],
)

OnEntry registers an entry handler that defines what actions the state machine should perform when entering a specific state. This allows you to specify initialization logic, setup operations, or state-specific preparations.

Parameters:

  • spec: The state machine specification to register the handler with
  • state: The state for which to register the entry handler
  • fn: The function to call when entering the state

Example: 

goat.OnEntry(spec, ActiveState{}, func(ctx context.Context, sm *MyStateMachine) {
    // Perform initialization when entering active state
    sm.StartTime = time.Now()
})

func OnEvent 

func OnEvent[T AbstractEvent, SM AbstractStateMachine](
	spec *StateMachineSpec[SM],
	state AbstractState,
	fn EventHandler[T, SM],
)

OnEvent registers an event handler that defines how a state machine responds to a specific event when in a particular state. This is the primary way to specify the behavior and reactions of your state machine to events.

Parameters:

  • spec: The state machine specification to register the handler with
  • state: The state in which this handler should be active
  • fn: The function to call when the event occurs

Example: 

goat.OnEvent(spec, IdleState{}, func(ctx context.Context, event Event, sm *MyStateMachine) {
    // Handle start event
    goat.Goto(ctx, &ActiveState{})
})

func OnExit 

func OnExit[SM AbstractStateMachine](
	spec *StateMachineSpec[SM],
	state AbstractState,
	fn ExitHandler[SM],
)

OnExit registers an exit handler that defines what cleanup or finalization actions the state machine should perform when leaving a specific state. This is essential for proper resource management and state transitions.

Parameters:

  • spec: The state machine specification to register the handler with
  • state: The state for which to register the exit handler
  • fn: The function to call when exiting the state

Example: 

goat.OnExit(spec, ActiveState{}, func(ctx context.Context, sm *MyStateMachine) {
    // Perform cleanup when exiting active state
    sm.cleanup()
})

func OnHalt 

func OnHalt[SM AbstractStateMachine](
	spec *StateMachineSpec[SM],
	state AbstractState,
	fn HaltHandler[SM],
)

OnHalt registers a halt handler that defines what final cleanup or shutdown actions the state machine should perform when stopping execution while in a specific state. This ensures proper termination and resource cleanup.

Parameters:

  • spec: The state machine specification to register the handler with
  • state: The state for which to register the halt handler
  • fn: The function to call when the state machine halts

Example: 

goat.OnHalt(spec, ActiveState{}, func(ctx context.Context, sm *MyStateMachine) {
    // Perform final cleanup before halting
    sm.saveState()
})

func OnTransition 

func OnTransition[SM AbstractStateMachine](
	spec *StateMachineSpec[SM],
	state AbstractState,
	fn TransitionHandler[SM],
)

OnTransition registers a transition handler that defines what actions should occur during state transitions from a specific state. This allows you to specify logic that runs between exiting one state and entering another.

Parameters:

  • spec: The state machine specification to register the handler with
  • state: The source state for which to register the transition handler
  • fn: The function to call during transition from this state

Example: 

goat.OnTransition(spec, IdleState{}, func(ctx context.Context, toState AbstractState, sm *MyStateMachine) {
    // Log transition from idle to any other state
    log.Printf("Transitioning from Idle to %T", toState)
})

func SendTo 

func SendTo(ctx context.Context, target AbstractStateMachine, event AbstractEvent)

SendTo sends an event to a specific state machine. This function must be called from within event handlers registered with OnEvent, OnEntry, OnExit, OnTransition, or OnHalt functions.

Parameters:

  • ctx: Context passed to the event handler
  • target: The state machine that should receive the event
  • event: The event to send

Example: 

goat.OnEntry(spec, IdleState{}, func(ctx context.Context, sm *MyStateMachine) {
    goat.SendTo(ctx, otherSM, Event{Name: "NOTIFY"})
})

func WriteDot 

func WriteDot(w io.Writer, opts ...Option) error

WriteDot performs model checking and outputs the state graph in DOT format. The output can be used with Graphviz to visualize the state space and identify paths to invariant violations.

Parameters:

  • w: Writer to output the DOT graph to
  • opts: Configuration options including state machines and invariants

Returns an error if model creation or solving fails.

Example: 

	var file *os.File
	file, err := os.Create("model.dot")
	if err != nil {
	    return err
	}
	defer file.Close()
     err = goat.WriteDot(file, goat.WithStateMachines(sm), goat.WithRules(goat.Always(cond)))

Types

type AbstractEvent 

type AbstractEvent interface {
	// contains filtered or unexported methods
}

type AbstractState 

type AbstractState interface {
	// contains filtered or unexported methods
}

AbstractState is the base interface for all states in the state machine. States represent discrete conditions or modes that a state machine can be in.

Implementations should embed the State struct to satisfy this interface.

Example: 

type IdleState struct {
    goat.State
    Timeout int
}

type AbstractStateMachine 

type AbstractStateMachine interface {
	SetInitialState(state AbstractState)
	// contains filtered or unexported methods
}

AbstractStateMachine is the base interface for all state machines. State machines encapsulate behavior and state transitions in response to events.

Implementations must embed the StateMachine struct. Instances are typically created through NewStateMachineSpec and its methods for proper configuration.

Example: 

type MyStateMachine struct {
    goat.StateMachine
    CustomData string
}

// Create via specification
spec := goat.NewStateMachineSpec(&MyStateMachine{})
spec.DefineStates(IdleState{}, ActiveState{}).
     SetInitialState(IdleState{})
instance := spec.NewInstance()

type Condition added in v0.3.0 

type Condition interface {
	Name() ConditionName
	Evaluate(w world) bool
}

Condition represents a named predicate evaluated against a world. Implementations must return true when the condition holds for the provided world, and false otherwise.

func BoolCondition added in v0.3.0 

func BoolCondition(name string, b bool) Condition

BoolCondition creates a condition from a constant boolean value. This is useful for creating conditions that always pass (true) or always fail (false), typically used for testing or as placeholder conditions.

Parameters:

  • name: The name of this condition
  • b: The boolean value that this condition will always return

Returns a Condition that can be used with Test() (for example via WithRules(Always(...))).

Example: 

alwaysPass := goat.BoolCondition("pass", true)
alwaysFail := goat.BoolCondition("fail", false)

func NewCondition added in v0.3.0 

func NewCondition[T AbstractStateMachine](name string, sm T, check func(T) bool) Condition

NewCondition creates a condition for a specific state machine instance. It allows checking properties of that particular state machine during model exploration and testing.

Parameters:

  • name: The condition name
  • sm: The state machine instance to create a condition for
  • check: A predicate function that returns true if the condition holds

Returns a Condition that can be used with Test() (for example via WithRules(Always(...))).

Example: 

serverCond := goat.NewCondition("conn-limit", serverSM, func(sm *ServerStateMachine) bool {
    return sm.ConnectionCount <= sm.MaxConnections
})

func NewCondition2 added in v0.3.0 

func NewCondition2[T1, T2 AbstractStateMachine](name string, sm1 T1, sm2 T2, check func(T1, T2) bool) Condition

NewCondition2 creates a condition that references two state machines.

Parameters:

  • name: The condition name
  • sm1, sm2: The state machines to reference
  • check: A predicate function that returns true if the condition holds

Returns a Condition that can be used with Test() (for example via WithRules(Always(...))).

Example: 

cond := goat.NewCondition2("pair", client, server, func(c *Client, s *Server) bool {
    return true
})

func NewCondition3 added in v0.3.0 

func NewCondition3[T1, T2, T3 AbstractStateMachine](name string, sm1 T1, sm2 T2, sm3 T3, check func(T1, T2, T3) bool) Condition

NewCondition3 creates a condition that references three state machines.

Parameters:

  • name: The condition name
  • sm1, sm2, sm3: The state machines to reference
  • check: A predicate function that returns true if the condition holds

Returns a Condition that can be used with Test() (for example via WithRules(Always(...))).

Example: 

cond := goat.NewCondition3("triple", client, server, db, func(c *Client, s *Server, d *Database) bool {
    return true
})

func NewMultiCondition added in v0.3.0 

func NewMultiCondition(name string, checkFunc func(Machines) bool, sms ...AbstractStateMachine) Condition

NewMultiCondition creates a condition that can reference multiple state machines. The provided check function receives a Machines accessor.

Parameters:

  • name: The condition name
  • checkFunc: Predicate that inspects one or more state machines
  • sms: State machines referenced by the condition

Returns a Condition that can be used with Test() (for example via WithRules(Always(...))).

Example: 

func NewConditionClientServer(client *Client, server *Server, check func(*Client, *Server) bool) goat.Condition {
    return goat.NewMultiCondition("client-server", func(machines goat.Machines) bool {
        c, ok1 := goat.GetMachine(machines, client)
        if !ok1 { return false }
        s, ok2 := goat.GetMachine(machines, server)
        if !ok2 { return false }

        return check(c, s)
    }, client, server)
}

// Usage
cond := NewConditionClientServer(client, server, func(c *Client, s *Server) bool {
    // business logic referencing both machines
    return c.Server != nil && s != nil
})

type ConditionName added in v0.3.0 

type ConditionName string

ConditionName represents the identifier for a condition.

func (ConditionName) String added in v0.4.0 

func (c ConditionName) String() string

type EntryHandler 

type EntryHandler[SM AbstractStateMachine] func(ctx context.Context, sm SM)

EntryHandler is a function type for handling state entry events. It is called when a state machine enters a new state.

type Event 

type Event[Sender AbstractStateMachine, Recipient AbstractStateMachine] struct {
	// contains filtered or unexported fields
}

Event is the base struct that should be embedded in all event implementations. It provides the required methods to satisfy the AbstractEvent interface and ensures events are properly copyable for the state machine system.

Example: 

type MyCustomEvent struct {
	goat.Event[*ProducerStateMachine, *ConsumerStateMachine]
	Payload string
}

func (*Event[Sender, Recipient]) Recipient added in v0.3.0 

func (e *Event[Sender, Recipient]) Recipient() Recipient

Recipient returns the recipient using the concrete type specified by the event's type parameters. If the actual recipient does not match the requested type, the zero value for Recipient is returned.

Parameters:

  • e: The event whose recipient should be retrieved.

Example: 

var event goat.Event[*ProducerStateMachine, *ConsumerStateMachine]
typedRecipient := event.Recipient()
if typedRecipient != nil {
    // Use the strongly typed recipient
}

func (*Event[Sender, Recipient]) Sender added in v0.3.0 

func (e *Event[Sender, Recipient]) Sender() Sender

Sender returns the sender using the concrete type specified by the event's type parameters. If the actual sender does not match the requested type, the zero value for Sender is returned.

Parameters:

  • e: The event whose sender should be retrieved.

Example: 

var event goat.Event[*ProducerStateMachine, *ConsumerStateMachine]
typedSender := event.Sender()
if typedSender != nil {
    // Use the strongly typed sender
}

type EventHandler 

type EventHandler[T AbstractEvent, SM AbstractStateMachine] func(ctx context.Context, event T, sm SM)

EventHandler is a function type for handling generic events in a state machine. It receives the event, the state machine instance, and a context for interacting with other state machines via SendTo, Goto, or Halt functions.

type EventSnapshot added in v0.6.0 

type EventSnapshot struct {
	TargetMachine string
	EventName     string
	Details       string
}

EventSnapshot is a snapshot of a queued event.

type ExitHandler 

type ExitHandler[SM AbstractStateMachine] func(ctx context.Context, sm SM)

ExitHandler is a function type for handling state exit events. It is called when a state machine exits its current state.

type HaltHandler 

type HaltHandler[SM AbstractStateMachine] func(ctx context.Context, sm SM)

HaltHandler is a function type for handling halt events. It is called when a state machine is about to stop permanently.

type Machines added in v0.2.0 

type Machines interface {
	Get(sm AbstractStateMachine) (AbstractStateMachine, bool)
}

Machines provides type-safe access to state machines during condition evaluation. It is used inside check functions to reference multiple state machines.

Implementations return false when the requested state machine does not exist in the current world.

type Option 

type Option interface {
	// contains filtered or unexported methods
}

Option is a configuration option for model checking operations. Options are used with Test() and Debug() functions to configure state machines, conditions, invariants, and other testing parameters.

Use the provided helper functions like WithStateMachines(), WithRules() to create options.

Example: 

result, err := goat.Test(
    goat.WithStateMachines(sm1, sm2),
    goat.WithRules(goat.Always(cond1)),
)

func WithRules added in v0.3.0 

func WithRules(rs ...Rule) Option

WithRules returns an Option that registers the provided rules during model checking.

Parameters:

  • rs: Rules created with helpers such as Always or WheneverPEventuallyQ

Returns an Option that can be supplied to Test.

Example: 

result, err := goat.Test(
	goat.WithStateMachines(node),
	goat.WithRules(
		goat.Always(consistency),
		goat.WheneverPEventuallyQ(requested, responded),
	),
)

func WithStateMachines 

func WithStateMachines(sms ...AbstractStateMachine) Option

WithStateMachines configures the test with the specified state machines. These state machines will be included in the model checking process.

Parameters:

  • sms: The state machines to include in the test

Returns an Option that can be passed to Test() or Debug().

Example: 

goat.WithStateMachines(serverSM, clientSM, proxysSM)

type Result added in v0.6.0 

type Result struct {
	Violations []Violation
	Summary    Summary
}

Result holds the outcome of a model checking run.

func Test 

func Test(opts ...Option) (*Result, error)

Test performs model checking on state machines with the provided options. It creates a Kripke model, explores all reachable states, checks invariants and temporal properties, and returns the results.

Parameters:

  • opts: Configuration options including state machines and rules

Returns:

  • *Result: verification results (violations, path information, summary)
  • error: if model creation or solving fails

Example: 

result, err := goat.Test(
    goat.WithStateMachines(serverSM, clientSM),
    goat.WithRules(goat.Always(cond)),
)
if err != nil {
    log.Fatal(err)
}
// result is automatically printed to stdout

func (*Result) HasViolation added in v0.6.0 

func (r *Result) HasViolation() bool

HasViolation reports whether any violations were found.

func (*Result) String added in v0.6.0 

func (r *Result) String() string

String returns a human-readable report of the model checking results.

type Rule added in v0.3.0 

type Rule interface {
	// contains filtered or unexported methods
}

Rule represents a property that can be enforced during model checking. Rules register additional checks that run while exploring the state space.

func Always added in v0.3.0 

func Always(c Condition) Rule

Always returns a rule that ensures c holds in every explored world.

Parameters:

  • c: Condition that must remain true in all explored states

Returns a Rule that can be supplied to WithRules.

Example: 

result, err := goat.Test(
	goat.WithStateMachines(node),
	goat.WithRules(
		goat.Always(healthy),
	),
)

func AlwaysEventually added in v0.3.0 

func AlwaysEventually(c Condition) Rule

AlwaysEventually returns a rule enforcing that c holds infinitely often.

Parameters:

  • c: Condition that must recur indefinitely

Returns a Rule that can be registered with WithRules.

Example: 

result, err := goat.Test(
	goat.WithStateMachines(node),
	goat.WithRules(
		goat.AlwaysEventually(heartbeat),
	),
)

func EventuallyAlways added in v0.3.0 

func EventuallyAlways(c Condition) Rule

EventuallyAlways returns a rule enforcing that c eventually holds forever.

Parameters:

  • c: Condition that must eventually remain true

Returns a Rule that can be registered with WithRules.

Example: 

result, err := goat.Test(
	goat.WithStateMachines(nodes...),
	goat.WithRules(
		goat.EventuallyAlways(stable),
	),
)

func WheneverPEventuallyQ added in v0.3.0 

func WheneverPEventuallyQ(p, q Condition) Rule

WheneverPEventuallyQ returns a rule enforcing that whenever p holds, q eventually holds.

Parameters:

  • p: Condition that triggers the obligation
  • q: Condition that must eventually become true

Returns a Rule that can be registered with WithRules.

Example: 

result, err := goat.Test(
	goat.WithStateMachines(primary, replica),
	goat.WithRules(
		goat.WheneverPEventuallyQ(write, replicated),
	),
)

type State 

type State struct {
	// contains filtered or unexported fields
}

State is the base struct that should be embedded in all state implementations. It provides the required methods to satisfy the AbstractState interface and ensures states are properly copyable for the state machine system.

Example: 

type MyState struct {
    goat.State
    CustomField int
}

type StateMachine 

type StateMachine struct {
	EventHandlers   map[AbstractState][]handlerInfo
	HandlerBuilders map[AbstractState][]handlerBuilderInfo

	State AbstractState
	// contains filtered or unexported fields
}

StateMachine provides the core infrastructure for state machine behavior. It must be embedded in concrete state machine implementations to provide state management, event handling, and transition capabilities.

Do not instantiate directly; instead embed in your state machine types and use NewStateMachineSpec to create properly configured instances.

Example: 

type MyStateMachine struct {
    goat.StateMachine
    Data string
}

func (*StateMachine) SetInitialState 

func (sm *StateMachine) SetInitialState(state AbstractState)

SetInitialState sets the starting state for this state machine instance. This can only be called once per instance, typically during initialization.

Parameters:

  • state: The state this state machine should start in

Panics if the initial state has already been set.

Example: 

sm.SetInitialState(&IdleState{})

type StateMachineSnapshot added in v0.6.0 

type StateMachineSnapshot struct {
	Name    string
	State   string
	Details string
}

StateMachineSnapshot is a snapshot of a single state machine.

type StateMachineSpec 

type StateMachineSpec[T AbstractStateMachine] struct {
	// contains filtered or unexported fields
}

StateMachineSpec defines the specification for a state machine type. It serves as a template for creating multiple instances of the same state machine with consistent behavior and state definitions.

Use NewStateMachineSpec to create a specification, then configure it with DefineStates and SetInitialState before creating instances.

func NewStateMachineSpec 

func NewStateMachineSpec[T AbstractStateMachine](prototype T) *StateMachineSpec[T]

NewStateMachineSpec creates a new state machine specification with the given prototype. The prototype defines the structure and behavior that all instances created from this spec will share.

Parameters:

  • prototype: An instance of the state machine type to use as template

Returns a specification that can be configured with states and handlers.

Example: 

spec := goat.NewStateMachineSpec(&MyStateMachine{})
spec.DefineStates(StateA{}, StateB{}).
     SetInitialState(StateA{})

func (*StateMachineSpec[T]) DefineStates 

func (spec *StateMachineSpec[T]) DefineStates(states ...AbstractState) *StateMachineSpec[T]

DefineStates sets the valid states for this state machine specification. It configures all provided states and sets up default handlers for each.

Parameters:

  • states: All valid states that this state machine can be in

Returns the spec for method chaining.

Example: 

spec.DefineStates(IdleState{}, ActiveState{}, ErrorState{})

func (*StateMachineSpec[T]) NewInstance 

func (spec *StateMachineSpec[T]) NewInstance() (T, error)

NewInstance creates a new state machine instance based on this specification. Each instance is independent and starts in the initial state defined by SetInitialState with all handlers configured.

Returns a fully configured state machine instance and any validation error.

Example: 

instance1, err := spec.NewInstance()
if err != nil {
	return err
}
instance2, err := spec.NewInstance() // Independent instance

func (*StateMachineSpec[T]) SetInitialState 

func (spec *StateMachineSpec[T]) SetInitialState(state AbstractState) *StateMachineSpec[T]

SetInitialState defines which state new instances will start in. The provided state must be one of the states defined in DefineStates.

Parameters:

  • state: The state that new instances should start in

Returns the spec for method chaining.

Example: 

spec.SetInitialState(IdleState{})

type Summary added in v0.6.0 

type Summary struct {
	// TotalWorlds is the number of distinct worlds (unique combinations of
	// state machine states and queued events) explored during model checking.
	TotalWorlds     int
	ExecutionTimeMs int64
}

Summary contains statistics about the model checking run.

type TransitionHandler 

type TransitionHandler[SM AbstractStateMachine] func(ctx context.Context, toState AbstractState, sm SM)

TransitionHandler is a function type for handling state transitions. It receives information about the target state and the state machine.

type UnTypedEvent added in v0.3.0 

type UnTypedEvent = Event[AbstractStateMachine, AbstractStateMachine]

UnTypedEvent is a convenience alias for an Event that does not specify concrete sender or recipient types.

type Violation added in v0.6.0 

type Violation struct {
	Rule string
	Path []WorldSnapshot
	Loop []WorldSnapshot
}

Violation represents a single property violation found during model checking.

type WorldSnapshot added in v0.6.0 

type WorldSnapshot struct {
	StateMachines []StateMachineSnapshot
	QueuedEvents  []EventSnapshot
}

WorldSnapshot represents a world — the combination of every state machine's current state and all queued events at a single point in time. A violation path is a sequence of worlds that leads to the violation.

Source Files

View all Source files

Directories

Path Synopsis
example
client-server command
meeting-room-reservation/with-exclusion command
meeting-room-reservation/without-exclusion command
simple-halt command
simple-non-deterministic command
simple-transition command
temporal-rule command
temporal-rule-violation command
internal
e2egen
strcase
typeutil
example command
example command

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.