Go

Install

go get github.com/crowecawcaw/snappea

Go 1.22 or later. The module has two packages, both standard library only:

• go/snappeaemit: Emit from application code, in tests, in processes tests start, and to production logs. This is all production code imports.
• go/snappeatest: record and check events from tests.

snappeatest runs the snappea checker. It uses SNAPPEA_BIN, else snappea on PATH, else downloads the release binary for the module's version once into the user cache and verifies it against checksums in the module. Offline, or with SNAPPEA_DOWNLOAD=0, install it yourself: cargo install snappea or pip install pysnappea.

Quick start

The examples on every language page check one spec: an inventory where reservations never exceed the stock and releases match reservations.

// The inventory contract, checked against the P model in this folder and against every example application.
event eStocked: (units: int);
event eReserved: (order: string, units: int);
event eReleased: (order: string, units: int);

// Applications give each product its own monitor through emit's key; the P model has one product.
spec InventoryCorrect observes eStocked, eReserved, eReleased {
  var available: int;
  var reservations: map[string, int];

  start state Unstocked {
    on eStocked do (p: (units: int)) {
      assert p.units >= 0, "negative initial stock";
      available = p.units;
      goto Ready;
    }
    on eReserved do { assert false, "reservation before stock setup"; }
    on eReleased do { assert false, "release before stock setup"; }
  }

  state Ready {
    on eStocked do { assert false, "product stocked twice"; }
    on eReserved do (p: (order: string, units: int)) {
      assert p.units > 0, "reservation must be positive";
      assert !(p.order in reservations), "duplicate reservation";
      available = available - p.units;
      assert available >= 0, "reservation exceeds available stock";
      reservations[p.order] = p.units;
    }
    on eReleased do (p: (order: string, units: int)) {
      assert p.order in reservations, "release without a reservation";
      assert p.units == reservations[p.order], "released quantity differs from reservation";
      available = available + p.units;
      reservations -= p.order;
    }
  }
}

The service emits an event after each change:

package inventory

import (
	"errors"

	"github.com/crowecawcaw/snappea/go/snappeaemit"
)

type Inventory struct {
	stock        map[string]int
	reservations map[[2]string]int
}

func New() *Inventory {
	return &Inventory{stock: map[string]int{}, reservations: map[[2]string]int{}}
}

func (i *Inventory) AddProduct(sku string, units int) {
	i.stock[sku] = units
	snappeaemit.Emit("eStocked", sku, map[string]any{"units": units})
}

func (i *Inventory) Reserve(sku, order string, units int) error {
	if units > i.stock[sku] {
		return errors.New("insufficient stock")
	}
	i.stock[sku] -= units
	i.reservations[[2]string{sku, order}] = units
	snappeaemit.Emit("eReserved", sku, map[string]any{"order": order, "units": units}) // after the change
	return nil
}

Start a recording at the top of the test. It checks when the test ends:

package inventory

import (
	"testing"

	"github.com/crowecawcaw/snappea/go/snappeatest"
)

func TestTwoOrdersForTheLastUnits(t *testing.T) {
	snappeatest.Start(t, snappeatest.Config{SpecFiles: []string{"../specs"}})

	inventory := New()
	inventory.AddProduct("coffee", 3)
	if err := inventory.Reserve("coffee", "order-1", 2); err != nil {
		t.Fatal(err)
	}
	_ = inventory.Reserve("coffee", "order-2", 2) // rejecting order-2 is fine too
}

go test ./... passes. Now break the service: delete the stock check from Reserve. The test's own code still passes, because it accepts either outcome for the second order. The spec does not:

--- FAIL: TestTwoOrdersForTheLastUnits (0.01s)
    inventory_test.go:10: P spec InventoryCorrect was broken: reservation exceeds available stock

          Events (key "coffee"):
              1  eStocked   units=3                inventory.go:18
              2  eReserved  order=order-1 units=2  inventory.go:24
              3  eReserved  order=order-2 units=2  inventory.go:24  <- broke the spec here

          Spec: ../specs/inventory.p:27
          snappea output: /tmp/snappeatest-TestTwoOrdersForTheLastUnits-3725067642

Test setup

A recording per test

Go has no global per-test hook, so each test opts in by calling snappeatest.Start. Put it in your existing fixture, next to the shared Config:

func stocked(t *testing.T) *inventory.Inventory {
	t.Helper()
	snappeatest.Start(t, snappeatest.Config{
		SpecFiles: []string{"../specs/inventory.p"},
		Specs:     []string{"InventoryCorrect"},
	})
	app := inventory.New()
	app.AddProduct("coffee", 3)
	return app
}

• Start checks in a t.Cleanup. Register cleanups that stop workers after Start, so they run first. A test that already failed is not checked.
• Each test, subtest and fuzz callback needs its own recording. Emitting after the check fails it.
• snappeatest.New plus r.Check(t) checks where you call it; r.Verify(ctx) returns (Result, error) instead.
• SNAPPEA_MODE=off makes recordings inert.

Parallel tests

The global snappeaemit.Emit cannot tell parallel tests apart: with several recordings active, it fails them all with a config error. For t.Parallel() tests, inject the recording's r.Emit into the application, or pass a context: snappeaemit.EmitCtx(ctx, ...) with ctx := r.Context(context.Background()).

Negative controls

Prove the spec catches the bug it is meant to catch:

v := r.ExpectViolation(t, "InventoryCorrect", "exceeds available")
if v.Key != "coffee" {
	t.Errorf("violation on %q", v.Key)
}

It checks now and fails the test unless that spec, and only it, is broken with a message matching the regular expression. Later checks of r ignore that spec.

Fuzzing

Call Start inside the f.Fuzz callback with its t, so each input gets a fresh recording.

Emitting events

snappeaemit.Emit("eReserved", sku, map[string]any{"order": order, "units": units})
snappeaemit.EmitAt(row.CommitTime, "eReserved", sku, payload) // when it happened, not when logged

• Payload: a struct or map whose JSON names match the P named tuple, a single value, a slice for a tuple, or nil. It is encoded at once.
• Key splits events into independent streams, such as one per product. Each stream gets its own instance of every spec.
• Emit after the change commits, or specs see states that never existed.
• The call site is recorded for failure reports.

In production

sink, err := snappeaemit.File("/var/log/app/events/inventory.jsonl") // or Stdout(), Writer(w), Callback(f)
if err != nil {
	log.Fatal(err)
}
snappeaemit.SetSink(sink)
defer snappeaemit.Close() // writes what is queued, closes the file

snappea observe specs/inventory.p '/var/log/app/events/*.jsonl' --spec InventoryCorrect

Emit never panics or blocks: a line that cannot be encoded or written, or that finds 4096 lines already queued, is dropped and counted by snappeaemit.Dropped(). Flush(timeout) waits for the queue; SetSink(nil) turns it off. In a process a test started, SetSink does nothing: events go to the test.

Other processes

Start a child with r.Env(), the environment plus SNAPPEA_EVENTS_DIR. If it uses snappeaemit, its events join the check. Wait for it before the check.

cmd := exec.Command(workerBinary)
cmd.Env = r.Env()
if err := cmd.Run(); err != nil {
	t.Fatal(err)
}

• r.EventsDir() is the folder, for anything that writes the event lines itself.
• r.AddEventsDir(path) adds a folder the recording did not create, such as a container volume.
• r.AddLog(path, parse) adds a log; parse(line) (snappeatest.Event, bool) returns an event with Time set, or false to skip the line. nil reads JSON lines as they are.

Failures

A failure shows the spec's assert message, the events of the key that broke it with where each was emitted, the assert in the P file, and the folder that keeps the events and the checker's output. Check reports it with t.Errorf; Verify returns it:

var v *snappeatest.SpecViolation
if errors.As(err, &v) && v.Key == "coffee" { ... }

*SpecViolation has Spec, Key, Message, Location (the P assert), Events (each with Event, Payload, Src), Liveness, Others and ArtifactsDir. Anything else is a *snappeatest.SetupError whose Kind is:

Reference

Settings

Go has no config file: settings are snappeatest.Config fields, with paths relative to WorkDir (default: the package folder). Environment variables override fields, except SNAPPEA_BIN, which Binary overrides. Strict is a *bool: use snappeatest.Bool(false). AllowUnobserved and ArtifactRoot are deprecated aliases for Strict: snappeatest.Bool(false) and Artifacts.

Environment variables

Suite coverage

Add func TestMain(m *testing.M) { snappeatest.Main(m) }. After the tests, Main prints the P spec states, handlers, statements and branches the checks reached together, and lists what no check reached. It writes no file. Set Config.Coverage (or SNAPPEA_COVERAGE) to a path to also keep it as JSON: the file is merged under a lock, so go test ./... packages can share it; delete a stale file before a run. Without Main, nothing is printed and checks with a path merge into it as each completes. SNAPPEA_COVERAGE=off (or Coverage: "off") turns suite coverage off.

API

• snappeatest on pkg.go.dev
• snappeaemit on pkg.go.dev

Runnable projects: Go examples.