gsm

package module

v0.1.5 Latest Latest Go to latest Published: Feb 20, 2026 License: MIT Imports: 4 Imported by: 0

Details

Valid go.mod file
Redistributable license
Tagged version
Stable version
Learn more about best practices

Repository

github.com/blackwell-systems/gsm

Links

Open Source Insights

README ¶

gsm — Governed State Machines

Build event-driven systems with mathematical convergence guarantees.

gsm is a Go library for constructing state machines where events may arrive out of order and violate business rules, but automatic compensation ensures all replicas converge to the same valid state. Convergence is verified at build time via exhaustive state-space enumeration. Runtime event application is O(1) table lookup with zero compensation overhead.

Based on: Normalization Confluence in Federated Registry Networks (Blackwell, 2026)

Quick Example

package main

import (
    "fmt"
    "github.com/blackwell-systems/gsm"
)

func main() {
    r := gsm.NewRegistry("order_system")

    // State variables (finite domains)
    status := r.Enum("status", "pending", "paid", "shipped")
    paid := r.Bool("paid")

    // Business rule: can't ship unpaid orders
    r.Invariant("no_ship_unpaid").
        Watches(status, paid).
        Holds(func(s gsm.State) bool {
            return s.Get(status) != "shipped" || s.GetBool(paid)
        }).
        Repair(func(s gsm.State) gsm.State {
            return s.Set(status, "pending") // Roll back
        }).
        Add()

    // Events
    r.Event("pay").
        Writes(status, paid).
        Apply(func(s gsm.State) gsm.State {
            return s.Set(status, "paid").SetBool(paid, true)
        }).
        Add()

    r.Event("ship").
        Writes(status).
        Apply(func(s gsm.State) gsm.State {
            return s.Set(status, "shipped")
        }).
        Add()

    // Build with verification
    machine, report, err := r.Build()
    if err != nil {
        panic(fmt.Sprintf("convergence not guaranteed: %v\n%s", err, report))
    }

    fmt.Printf("%s", report)
    // Machine: order_system
    //   Variables: 2
    //   States: 6
    //   Events: 2
    //   WFC: PASS (max repair depth: 1)
    //   CC (Compensation Commutativity): PASS (1 pairs: 1 disjoint, 0 brute-force)
    //   Convergence: GUARANTEED

    // Runtime usage (O(1) lookups)
    s := machine.NewState()
    s = machine.Apply(s, "ship") // Arrives before payment
    s = machine.Apply(s, "pay")  // Arrives after shipment

    fmt.Printf("Final: %s\n", s) // {status=paid, paid=true}
    // Compensation fired automatically - shipment was rolled back
}

New to convergent systems? See CONCEPTS.md for foundational definitions, theory explanations, and a glossary mapping paper terms to code.

Want rigorous mathematical foundations? See THEORY.md for formal definitions, proofs, and connections to rewriting theory.

How It Works

Build Time (Verification)

When you call registry.Build():

Enumerate state space - All combinations of variable values (must be finite)
Compute normal forms - For every state, apply compensation until valid
Verify WFC - Compensation terminates and reaches valid states
Build step table - For every (event, state) pair, precompute the normal form after applying the event
Verify CC - Different event orderings reach the same normal form (with footprint optimization)

If verification passes, you get an immutable Machine with precomputed lookup tables.

If verification fails, you get a detailed report showing:

Which events violate CC
At which state the violation occurs
The divergent traces (order 1 vs order 2)

Runtime (O(1) Execution)

machine.Apply(state, "ship_item")

This does one table lookup: step[event_index][state_id] returns the precomputed normal form.

No compensation logic runs at runtime. All the complexity is resolved at build time.

Core Concepts

Invariants

An invariant is a property that must always hold on valid states. Each invariant has three parts:

Watches(vars...): Declares which variables the invariant depends on (its "footprint"). The repair function can only modify these variables.
Holds(func): The boolean condition that must be true. When this returns false, compensation fires.
Repair(func): How to fix states where the invariant is violated. This is the compensation function.

r.Invariant("no_overdraft").
    Watches(balance).
    Holds(func(s gsm.State) bool {
        return s.GetInt(balance) >= 0
    }).
    Repair(func(s gsm.State) gsm.State {
        return s.SetInt(balance, 0)  // Prevent negative balance
    }).
    Add()

Invariants fire in declaration order (priority). If multiple invariants are violated, the first one repairs first, then the next, until all hold.

Compensation

Compensation is the automatic repair process that fires when events violate invariants:

Event modifies state (e.g., "withdraw $100")
Invariant check fails (e.g., balance becomes -50)
Repair function fires (e.g., set balance to 0)
Repeat until all invariants hold

For convergence, compensation must be:

Well-Founded (WFC): Repairs must eventually terminate (no infinite loops)
Commutative (CC): Event order shouldn't matter after compensation runs

The library verifies both properties at build time by exhaustively checking all possible states and event orderings.

Events

Events are operations that modify state. Each event declares:

Writes(vars...): Which variables this event modifies
Guard(func): Optional precondition - if false, event is a no-op
Apply(func): The effect function that transforms the state

r.Event("withdraw").
    Writes(balance).
    Guard(func(s gsm.State) bool {
        return s.GetInt(balance) >= amount  // Can't withdraw if insufficient
    }).
    Apply(func(s gsm.State) gsm.State {
        return s.SetInt(balance, s.GetInt(balance) - amount)
    }).
    Add()

Events can arrive in any order. The library verifies that different orderings converge to the same final state.

Independence Declarations

By default, gsm checks all event pairs for commutativity. For large systems, you can optimize by declaring which pairs are independent:

// Calling Independent() automatically switches to declared-only mode
r.Independent("deposit", "send_notification")
r.Independent("withdraw", "send_notification")

Independent events can arrive in either order (they're not causally related). Only declared pairs will be checked for commutativity.

Tip: Events with disjoint Writes() sets and non-overlapping invariant footprints are automatically proved commutative via footprint analysis (no exhaustive checking needed).

When to Use gsm

Use gsm when:

Building event-sourced systems with out-of-order events
Operations can violate invariants (need compensation/repair)
State space is finite and enumerable (< ~1M states)
You want mathematical convergence guarantees
You're using Go

Don't use gsm when:

Operations already commute (use CRDTs instead)
Operations preserve invariants in all orderings (use invariant confluence)
State space is unbounded or infinite
Real-time latency requirements conflict with build-time verification cost

API Overview

Building Machines

r := gsm.NewRegistry("machine_name")

// Declare state variables (finite domains required)
status := r.Enum("status", "draft", "active", "archived")
count := r.Int("count", 0, 100)           // range [0, 100] inclusive
enabled := r.Bool("enabled")

// Declare invariants with compensation
r.Invariant("count_positive").
    Watches(count).                        // Footprint: which vars this watches
    Holds(func(s gsm.State) bool {
        return s.GetInt(count) >= 0
    }).
    Repair(func(s gsm.State) gsm.State {
        return s.SetInt(count, 0)         // Clamp to zero
    }).
    Add()

// Declare events
r.Event("increment").
    Writes(count).                         // Which vars this modifies
    Guard(func(s gsm.State) bool {        // Optional precondition
        return s.GetInt(count) < 100
    }).
    Apply(func(s gsm.State) gsm.State {
        return s.SetInt(count, s.GetInt(count)+1)
    }).
    Add()

// Optional: declare which event pairs are independent
// (if omitted, all pairs are checked)
// Calling Independent() automatically switches to declared-only mode
r.Independent("increment", "enable")
r.Independent("increment", "disable")

// Build with verification
machine, report, err := r.Build()

Using Machines

// Create initial state (all variables at min/first value)
s := machine.NewState()

// Apply events (returns new state, original unchanged)
s = machine.Apply(s, "increment")
s = machine.Apply(s, "increment")

// Check validity
if machine.IsValid(s) {
    fmt.Println("State satisfies all invariants")
}

// Manually normalize (usually not needed - Apply does this)
s = machine.Normalize(s)

// Get event list
events := machine.Events() // ["increment", "enable", "disable"]

Reading State

// Enum variables
status := s.Get(statusVar)           // returns string

// Bool variables
enabled := s.GetBool(enabledVar)     // returns bool

// Int variables
count := s.GetInt(countVar)          // returns int (adjusted for min offset)

Writing State

// Enum
s = s.Set(statusVar, "active")

// Bool
s = s.SetBool(enabledVar, true)

// Int (automatically clamped to declared range)
s = s.SetInt(countVar, 42)

Verification Report

The Report returned by Build() shows:

Machine: order_fulfillment
  Variables: 3
  States: 48
  Events: 5

  WFC: PASS (max repair depth: 1)
  CC (Compensation Commutativity): PASS (3 pairs: 3 disjoint, 0 brute-force)

  Convergence: GUARANTEED
Checked in: 234µs

WFC (Well-Founded Compensation): Compensation terminates from every state. The report shows the maximum number of repair steps needed.

CC (Compensation Commutativity): Different event orderings converge to the same normal form. The report shows:

Disjoint pairs - Proved by footprint analysis (no exhaustive check needed)
Brute-force pairs - Checked by testing all states

If verification fails, you get a counterexample:

CC (Compensation Commutativity): FAIL
  Events: (grant_read, grant_write)
  State:  {can_read=false, can_write=false}
  grant_read→grant_write: {can_read=true, can_write=true}
  grant_write→grant_read: {can_read=true, can_write=false}

This shows the exact state and event pair where CC fails, plus the divergent traces.

Performance

Build Time

Verification cost depends on state space size:

States	Variables	Build Time	Notes
6	2 bools	< 1ms	Instant
48	1 enum(5) + 1 bool + 1 int[0..5]	< 1ms	Instant
1,024	10 bools	~5ms	Very fast
1M	~20 bits total	~500ms	Acceptable

State space grows as the product of variable domains: 5 enums × 100 ints = 500 states.

Default limit: 2²⁰ ≈ 1M states. Configurable but exhaustive verification becomes slow beyond this.

Runtime

Event application: O(1) - single array lookup, no computation.

Memory: One uint64 per state for normal form table, plus one uint64 per (event, state) pair for step table. For 1M states × 10 events = ~80MB.

Relationship to the Paper

This library implements the single-registry governance model from Section 3 of the paper:

Registry = the machine definition (variables, invariants, compensation, events)
WFC (Definition 4.1) = well-founded measure on compensation depth
CC (Definition 4.3) = compensation commutativity (CC1 + CC2)
Theorem 5.1 = WFC + CC ⟹ unique normal forms (proven via Newman's Lemma)
Section 9 = verification calculus with footprint optimization (implemented in verify.go)

The paper proves: if WFC and CC hold, all processors consuming the same events converge to the same valid state regardless of application order.

This library verifies: does your machine satisfy WFC and CC?

Example: Order Fulfillment

Full example from the paper (see gsm_test.go):

r := gsm.NewRegistry("order_fulfillment")

status := r.Enum("status", "pending", "paid", "shipped", "cancelled")
paid := r.Bool("paid")
inventory := r.Int("inventory", 0, 5)

// Invariant: can't ship unpaid orders
r.Invariant("no_ship_unpaid").
    Watches(status, paid).
    Holds(func(s gsm.State) bool {
        return s.Get(status) != "shipped" || s.GetBool(paid)
    }).
    Repair(func(s gsm.State) gsm.State {
        return s.Set(status, "pending")
    }).
    Add()

// Invariant: inventory can't go negative
r.Invariant("stock_non_negative").
    Watches(inventory).
    Holds(func(s gsm.State) bool {
        return s.GetInt(inventory) >= 0
    }).
    Repair(func(s gsm.State) gsm.State {
        return s.SetInt(inventory, 0)
    }).
    Add()

r.Event("process_payment").
    Writes(status, paid).
    Guard(func(s gsm.State) bool {
        return s.Get(status) == "pending"
    }).
    Apply(func(s gsm.State) gsm.State {
        return s.Set(status, "paid").SetBool(paid, true)
    }).
    Add()

r.Event("ship_item").
    Writes(status, inventory).
    Guard(func(s gsm.State) bool {
        return s.Get(status) == "paid" && s.GetInt(inventory) > 0
    }).
    Apply(func(s gsm.State) gsm.State {
        return s.Set(status, "shipped").SetInt(inventory, s.GetInt(inventory)-1)
    }).
    Add()

r.Event("restock").
    Writes(inventory).
    Apply(func(s gsm.State) gsm.State {
        return s.SetInt(inventory, s.GetInt(inventory)+1)
    }).
    Add()

// Only check independent pairs (restock comes from different source)
// Calling Independent() automatically switches to declared-only mode
r.Independent("process_payment", "restock")
r.Independent("ship_item", "restock")

machine, report, err := r.Build()
// Convergence: GUARANTEED

Limitations

Finite state spaces only - Cannot model unbounded domains (arbitrary strings, lists)
Build-time cost - Large state spaces (> 1M states) verification becomes slow
Verification requires Go - Runtime portable via JSON export, but verification engine is Go-only
Single-registry - Federation (Section 7 of paper) not yet implemented
No runtime monitoring - Once built, machine is immutable (cannot add events/invariants dynamically)

Multi-Language Support

While verification requires Go, runtime is portable to any language. Use Machine.Export() to serialize the verified machine to JSON:

machine, _, err := registry.Build()
if err != nil {
    log.Fatal(err)
}

machine.Export("order.gsm.json")

The exported JSON contains:

Variable definitions (types, domains)
Event names (ordered)
Normal form table: nf[stateID] → normalized stateID
Step table: step[eventID][stateID] → normalized result stateID

Runtime Implementation (Python Example)

import json

class Machine:
    def __init__(self, path):
        with open(path) as f:
            d = json.load(f)
        self.events = {n: i for i, n in enumerate(d['events'])}
        self.step = d['step']
        self.nf = d['nf']

    def apply(self, state, event):
        """O(1) event application via table lookup"""
        return self.step[self.events[event]][state]

    def normalize(self, state):
        return self.nf[state]

# Use it
m = Machine('order.gsm.json')
s = 0
s = m.apply(s, 'ship_item')
s = m.apply(s, 'process_payment')

That's it - ~20 lines of code for a complete runtime. The same pattern works in JavaScript, Rust, Java, or any language that can:

Load JSON
Index arrays

Verification complexity stays in Go. Runtime simplicity is universal.

Installation

go get github.com/blackwell-systems/gsm

Testing

go test -v

Tests cover:

WFC verification (termination, cycles, depth)
CC verification (disjoint footprints, brute force, failures)
Event order independence
Compensation behavior
State encoding/decoding

License

MIT License - see LICENSE file

Citation

@techreport{blackwell2026nc,
  author = {Blackwell, Dayna},
  title = {Normalization Confluence in Federated Registry Networks},
  year = {2026},
  publisher = {Zenodo},
  doi = {10.5281/zenodo.18677400},
  url = {https://doi.org/10.5281/zenodo.18677400}
}

nccheck - YAML-based verifier for registry specs (reference implementation from the paper)
gsm (this library) - Go library for building verified convergent state machines

Documentation ¶

Overview ¶

Package gsm implements governed state machines: finite state machines whose states live in a registry that enforces invariants via compensation. Events are applied in any order; the registry guarantees convergence to the same valid state regardless of ordering.

Example ¶

Example demonstrates the complete workflow: define state variables, invariants, and events, then verify convergence guarantees at build time. Runtime event application is O(1) table lookup with zero overhead.

package main

import (
	"fmt"

	"github.com/blackwell-systems/gsm"
)

func main() {
	b := gsm.NewRegistry("counter")

	// State variable with bounded domain
	count := b.Int("count", 0, 10)

	// Business rule: count cannot exceed maximum
	b.Invariant("cap_at_10").
		Watches(count).
		Holds(func(s gsm.State) bool {
			return s.GetInt(count) <= 10
		}).
		Repair(func(s gsm.State) gsm.State {
			return s.SetInt(count, 10) // Clamp to maximum
		}).
		Add()

	// Event: increment counter
	b.Event("increment").
		Writes(count).
		Apply(func(s gsm.State) gsm.State {
			return s.SetInt(count, s.GetInt(count)+1)
		}).
		Add()

	// Build with verification
	machine, report, err := b.Build()
	if err != nil {
		panic(fmt.Sprintf("convergence not guaranteed: %v\n%s", err, report))
	}

	fmt.Printf("Convergence: %v\n", report.WFC && report.CC)

	// Runtime usage - increment beyond limit
	s := machine.NewState()
	for i := 0; i < 15; i++ {
		s = machine.Apply(s, "increment")
	}

	fmt.Printf("Count: %d\n", s.GetInt(count))
}

Output:

Convergence: true
Count: 10

Index ¶

type CCFailure
type CheckFunc
type EffectFunc
type EventBuilder
type InvariantBuilder
type Machine
type Registry
- func NewRegistry(name string) *Registry
type Report
- func (r *Report) String() string
type State
type Var
- func (v Var) Name() string
type VarKind

Constants ¶

This section is empty.

Variables ¶

This section is empty.

Functions ¶

This section is empty.

Types ¶

type CCFailure ¶

type CCFailure struct {
	Event1  string
	Event2  string
	State   State
	Result1 State // apply e1 then e2
	Result2 State // apply e2 then e1
}

CCFailure describes a specific CC violation.

type CheckFunc ¶

type CheckFunc func(State) bool

CheckFunc is a predicate over State.

type EffectFunc ¶

type EffectFunc func(State) State

EffectFunc transforms a State.

type EventBuilder ¶

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

EventBuilder provides a fluent API for declaring an event.

func (*EventBuilder) Add ¶

func (eb *EventBuilder) Add()

Add registers the event with the registry.

func (*EventBuilder) Apply ¶

func (eb *EventBuilder) Apply(fn EffectFunc) *EventBuilder

Apply sets the event's effect function.

func (*EventBuilder) Guard ¶

func (eb *EventBuilder) Guard(fn CheckFunc) *EventBuilder

Guard sets an optional precondition. If the guard returns false, the event is a no-op in that state.

func (*EventBuilder) Writes ¶

func (eb *EventBuilder) Writes(vars ...Var) *EventBuilder

Writes declares which variables this event modifies.

type InvariantBuilder ¶

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

InvariantBuilder provides a fluent API for declaring an invariant.

func (*InvariantBuilder) Add ¶

func (ib *InvariantBuilder) Add()

Add registers the invariant with the registry.

func (*InvariantBuilder) Holds ¶ added in v0.1.2

func (ib *InvariantBuilder) Holds(fn CheckFunc) *InvariantBuilder

Holds sets the invariant predicate. Returns true if the invariant holds.

func (*InvariantBuilder) Repair ¶

func (ib *InvariantBuilder) Repair(fn EffectFunc) *InvariantBuilder

Repair sets the compensation function. Called when Check returns false. Must only modify variables declared in Over().

func (*InvariantBuilder) Watches ¶ added in v0.1.2

func (ib *InvariantBuilder) Watches(vars ...Var) *InvariantBuilder

Watches declares the invariant's footprint — which variables it constrains and which its repair may modify.

type Machine ¶

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

Machine is an immutable, verified governed state machine. Created by Builder.Build() after WFC and CC verification passes. All operations are table lookups — no computation at runtime.

func (*Machine) Apply ¶

func (m *Machine) Apply(s State, event string) State

Apply processes an event, returning the unique normal form. This is a single table lookup — O(1). Panics if the event name is unknown.

Example ¶

ExampleMachine_Apply demonstrates O(1) event application at runtime. All compensation is precomputed during Build() - no runtime overhead.

package main

import (
	"fmt"

	"github.com/blackwell-systems/gsm"
)

func main() {
	b := gsm.NewRegistry("light")

	// State machine: off -> on -> off
	power := b.Bool("power")

	b.Event("toggle").
		Writes(power).
		Apply(func(s gsm.State) gsm.State {
			return s.SetBool(power, !s.GetBool(power))
		}).
		Add()

	machine, _, err := b.Build()
	if err != nil {
		panic(err)
	}

	s := machine.NewState()
	fmt.Printf("Initial: power=%v\n", s.GetBool(power))

	s = machine.Apply(s, "toggle")
	fmt.Printf("After toggle: power=%v\n", s.GetBool(power))

	s = machine.Apply(s, "toggle")
	fmt.Printf("After toggle: power=%v\n", s.GetBool(power))

}

Output:

Initial: power=false
After toggle: power=true
After toggle: power=false

func (*Machine) Events ¶

func (m *Machine) Events() []string

Events returns the names of all declared events.

func (*Machine) Export ¶

func (m *Machine) Export(path string) error

Export writes the verified machine to a portable JSON format. The exported file can be loaded by runtime implementations in any language, enabling O(1) event application without reimplementing verification.

The format contains:

State variable definitions (types, domains)
Event names (ordered)
Normal form table: nf[stateID] → normalized stateID
Step table: step[eventID][stateID] → normalized result stateID
Verification metadata (WFC/CC results, state count, etc.)

Runtime libraries only need to:

Load the JSON
Implement Apply(state, event) as step[events[event]][state]

Example runtime (Python):

import json
class Machine:
    def __init__(self, path):
        with open(path) as f:
            d = json.load(f)
        self.events = {n: i for i, n in enumerate(d['events'])}
        self.step = d['step']
    def apply(self, state, event):
        return self.step[self.events[event]][state]

Example ¶

ExampleMachine_Export demonstrates JSON export for multi-language runtimes.

package main

import (
	"fmt"
	"os"
	"runtime"

	"github.com/blackwell-systems/gsm"
)

func main() {
	b := gsm.NewRegistry("simple")
	state := b.Bool("state")

	b.Event("toggle").
		Writes(state).
		Apply(func(s gsm.State) gsm.State {
			return s.SetBool(state, !s.GetBool(state))
		}).
		Add()

	machine, _, err := b.Build()
	if err != nil {
		panic(err)
	}

	// Export to JSON (verification tables + metadata)
	tmpDir := "/tmp"
	if runtime.GOOS == "windows" {
		tmpDir = os.Getenv("TEMP")
	}
	path := fmt.Sprintf("%s/simple.json", tmpDir)
	err = machine.Export(path)
	if err != nil {
		panic(err)
	}

	fmt.Println("Machine exported successfully")
}

Output:

Machine exported successfully

func (*Machine) IsValid ¶

func (m *Machine) IsValid(s State) bool

IsValid returns true if all invariants hold for the state.

func (*Machine) Name ¶

func (m *Machine) Name() string

Name returns the machine's name.

func (*Machine) NewState ¶

func (m *Machine) NewState() State

NewState returns the zero state (all variables at their minimum/first value).

func (*Machine) Normalize ¶

func (m *Machine) Normalize(s State) State

Normalize returns the normal form of a state. If the state is already valid, returns it unchanged.

type Registry ¶ added in v0.1.3

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

Registry holds the rules that govern state machines: variables, invariants, compensation functions, and events. After declaring these, call Build() to verify convergence properties and produce an immutable Machine.

The registry is the central authority that defines what states are valid and how to repair invalid states through compensation.

func NewRegistry ¶ added in v0.1.3

func NewRegistry(name string) *Registry

NewRegistry creates a Registry for a named state machine. By default, all event pairs are checked for CC. Use Independent() to restrict checking to specific pairs.

func (*Registry) Bool ¶ added in v0.1.3

func (r *Registry) Bool(name string) Var

Bool declares a boolean state variable.

func (*Registry) Build ¶ added in v0.1.3

func (r *Registry) Build() (*Machine, *Report, error)

Build verifies WFC and CC, then returns an immutable Machine.

Example ¶

ExampleRegistry_Build shows the verification process and report output. The registry exhaustively enumerates the state space and verifies WFC (well-founded compensation) and CC (compensation commutativity).

package main

import (
	"fmt"

	"github.com/blackwell-systems/gsm"
)

func main() {
	b := gsm.NewRegistry("counter")

	// Single integer variable
	count := b.Int("count", 0, 10)

	// Invariant: count must stay <= 10
	b.Invariant("cap_at_10").
		Watches(count).
		Holds(func(s gsm.State) bool {
			return s.GetInt(count) <= 10
		}).
		Repair(func(s gsm.State) gsm.State {
			return s.SetInt(count, 10) // Clamp to max
		}).
		Add()

	// Increment event
	b.Event("increment").
		Writes(count).
		Apply(func(s gsm.State) gsm.State {
			return s.SetInt(count, s.GetInt(count)+1)
		}).
		Add()

	machine, report, err := b.Build()
	if err != nil {
		panic(err)
	}

	fmt.Printf("States verified: %d\n", report.StateCount)
	fmt.Printf("WFC: %v\n", report.WFC)
	fmt.Printf("CC: %v\n", report.CC)

	// Test the machine
	s := machine.NewState()
	for i := 0; i < 15; i++ {
		s = machine.Apply(s, "increment")
	}
	fmt.Printf("Count after 15 increments: %d\n", s.GetInt(count))

}

Output:

States verified: 11
WFC: true
CC: true
Count after 15 increments: 10

func (*Registry) Enum ¶ added in v0.1.3

func (r *Registry) Enum(name string, values ...string) Var

Enum declares an enumerated state variable.

func (*Registry) Event ¶ added in v0.1.3

func (r *Registry) Event(name string) *EventBuilder

Event begins declaring a named event.

func (*Registry) Independent ¶ added in v0.1.3

func (r *Registry) Independent(e1name, e2name string) *Registry

Independent declares that two events may arrive in either order (they are not causally related). Compensation Commutativity (CC) will be checked for this pair.

Calling Independent() automatically switches to declared-only mode: only explicitly declared pairs will be verified. This avoids checking all O(n²) event pairs when most are causally ordered.

func (*Registry) Int ¶ added in v0.1.3

func (r *Registry) Int(name string, min, max int) Var

Int declares a bounded integer state variable.

func (*Registry) Invariant ¶ added in v0.1.3

func (r *Registry) Invariant(name string) *InvariantBuilder

Invariant begins declaring a named invariant.

Example ¶

ExampleRegistry_Invariant demonstrates the priority-ordered compensation system. When multiple invariants are violated, repairs fire in declaration order.

package main

import (
	"fmt"

	"github.com/blackwell-systems/gsm"
)

func main() {
	b := gsm.NewRegistry("stock")

	qty := b.Int("qty", 0, 100)
	reserved := b.Int("reserved", 0, 100)

	// Invariant 1: reserved cannot exceed quantity (higher priority)
	b.Invariant("reserved_lte_qty").
		Watches(qty, reserved).
		Holds(func(s gsm.State) bool {
			return s.GetInt(reserved) <= s.GetInt(qty)
		}).
		Repair(func(s gsm.State) gsm.State {
			return s.SetInt(reserved, s.GetInt(qty))
		}).
		Add()

	// Invariant 2: quantity cannot be negative (lower priority)
	b.Invariant("qty_gte_zero").
		Watches(qty).
		Holds(func(s gsm.State) bool {
			return s.GetInt(qty) >= 0
		}).
		Repair(func(s gsm.State) gsm.State {
			return s.SetInt(qty, 0)
		}).
		Add()

	b.Event("reduce").
		Writes(qty).
		Apply(func(s gsm.State) gsm.State {
			return s.SetInt(qty, s.GetInt(qty)-10)
		}).
		Add()

	machine, _, err := b.Build()
	if err != nil {
		panic(err)
	}

	s := machine.NewState()
	s = s.SetInt(qty, 5)
	s = s.SetInt(reserved, 3)

	s = machine.Apply(s, "reduce") // qty becomes -5, triggers compensation

	fmt.Printf("qty=%d, reserved=%d\n", s.GetInt(qty), s.GetInt(reserved))
}

Output:

qty=0, reserved=0

func (*Registry) OnlyDeclaredPairs ¶ added in v0.1.3

func (r *Registry) OnlyDeclaredPairs() *Registry

OnlyDeclaredPairs explicitly switches Compensation Commutativity (CC) checking to only the event pairs declared via Independent(). This is now automatic when you call Independent(), but this method remains for explicitness and backward compatibility.

type Report ¶

type Report struct {
	Name       string
	StateCount int
	VarCount   int
	EventCount int

	// WFC results
	WFC          bool
	MaxRepairLen int // longest compensation chain

	// CC results
	CC            bool
	PairsTotal    int
	PairsDisjoint int        // proved by footprint disjointness
	PairsBrute    int        // proved by exhaustive check
	CCFailure     *CCFailure // non-nil if CC failed
}

Report contains the results of build-time verification.

func (*Report) String ¶

func (r *Report) String() string

type State ¶

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

State is a compact, immutable representation of all variable values. Internally it is a bitpacked uint64, enabling use as a table index for precomputed normal forms.

func (State) Get ¶

func (s State) Get(v Var) string

Get returns the string value of an enum variable.

func (State) GetBool ¶

func (s State) GetBool(v Var) bool

GetBool returns the value of a bool variable.

func (State) GetInt ¶

func (s State) GetInt(v Var) int

GetInt returns the value of an int variable (adjusted for min offset).

func (State) ID ¶

func (s State) ID() uint64

ID returns the packed integer, usable as a table index.

func (State) Set ¶

func (s State) Set(v Var, val string) State

Set returns a new State with an enum variable set to the named value.

func (State) SetBool ¶

func (s State) SetBool(v Var, val bool) State

SetBool returns a new State with a bool variable set.

func (State) SetInt ¶

func (s State) SetInt(v Var, val int) State

SetInt returns a new State with an int variable set. Value is clamped to the variable's declared range.

func (State) String ¶

func (s State) String() string

String returns a human-readable representation.

Example ¶

ExampleState_String shows the human-readable state representation.

package main

import (
	"fmt"

	"github.com/blackwell-systems/gsm"
)

func main() {
	b := gsm.NewRegistry("example")

	status := b.Enum("status", "pending", "active", "done")
	count := b.Int("count", 0, 100)
	enabled := b.Bool("enabled")

	machine, _, err := b.Build()
	if err != nil {
		panic(err)
	}

	s := machine.NewState()
	s = s.Set(status, "active")
	s = s.SetInt(count, 42)
	s = s.SetBool(enabled, true)

	fmt.Println(s)
}

Output:

{status=active, count=42, enabled=true}

type Var ¶

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

Var is a handle to a declared state variable. Users receive Vars from the Builder and pass them to State accessors.

func (Var) Name ¶

func (v Var) Name() string

Name returns the variable's declared name.

type VarKind ¶

type VarKind int

VarKind distinguishes variable types.

const (
	BoolKind VarKind = iota
	EnumKind
	IntKind
)

Source Files ¶

View all Source files

?	: This menu
/	: Search site
f or F	: Jump to
y or Y	: Canonical URL

README ¶

gsm — Governed State Machines

Quick Example

How It Works

Build Time (Verification)

Runtime (O(1) Execution)

Core Concepts

Invariants

Compensation

Events

Independence Declarations

When to Use gsm

API Overview

Building Machines

Using Machines

Reading State

Writing State

Verification Report

Performance

Build Time

Runtime

Relationship to the Paper

Example: Order Fulfillment

Limitations

Multi-Language Support

Runtime Implementation (Python Example)

Installation

Testing

License

Citation

Related Tools

Further Reading

Documentation ¶

Overview ¶

Index ¶

Examples ¶

Constants ¶

Variables ¶

Functions ¶

Types ¶

type CCFailure ¶

type CheckFunc ¶

type EffectFunc ¶

type EventBuilder ¶

func (*EventBuilder) Add ¶

func (*EventBuilder) Apply ¶

func (*EventBuilder) Guard ¶

func (*EventBuilder) Writes ¶

type InvariantBuilder ¶

func (*InvariantBuilder) Add ¶

func (*InvariantBuilder) Holds ¶ added in v0.1.2

func (*InvariantBuilder) Repair ¶

func (*InvariantBuilder) Watches ¶ added in v0.1.2

type Machine ¶

func (*Machine) Apply ¶

func (*Machine) Events ¶

func (*Machine) Export ¶

func (*Machine) IsValid ¶

func (*Machine) Name ¶

func (*Machine) NewState ¶

func (*Machine) Normalize ¶

type Registry ¶ added in v0.1.3

func NewRegistry ¶ added in v0.1.3

func (*Registry) Bool ¶ added in v0.1.3

func (*Registry) Build ¶ added in v0.1.3

func (*Registry) Enum ¶ added in v0.1.3

func (*Registry) Event ¶ added in v0.1.3

func (*Registry) Independent ¶ added in v0.1.3

func (*Registry) Int ¶ added in v0.1.3

func (*Registry) Invariant ¶ added in v0.1.3

func (*Registry) OnlyDeclaredPairs ¶ added in v0.1.3

type Report ¶

func (*Report) String ¶

type State ¶

func (State) Get ¶

func (State) GetBool ¶

func (State) GetInt ¶

func (State) ID ¶

func (State) Set ¶

func (State) SetBool ¶