Java

Install

Java 17 or later. One artifact, io.github.crowecawcaw:snappea, holds both halves:

• io.github.crowecawcaw.snappea.emit: SnappeaEmit.emit(...) and production sinks. JDK only; this is all production code uses.
• io.github.crowecawcaw.snappea: recordings, checks and the JUnit 5 extension. JUnit and opentest4j are optional dependencies that your test framework brings.

The snappea checker comes in a classifier jar of the same artifact, natives-<os>-<arch> (linux-x86_64, linux-aarch64, macos-x86_64, macos-aarch64, windows-x86_64). Add it in test scope, with snappea.version set to a release:

<dependency>
  <groupId>io.github.crowecawcaw</groupId>
  <artifactId>snappea</artifactId>
  <version>${snappea.version}</version>
</dependency>
<dependency>
  <groupId>io.github.crowecawcaw</groupId>
  <artifactId>snappea</artifactId>
  <version>${snappea.version}</version>
  <classifier>${snappea.natives}</classifier>
  <scope>test</scope>
</dependency>

If everyone builds on one platform, write its classifier in place of ${snappea.natives}. Otherwise pick it per platform with profiles:

<profiles>
  <profile><id>snappea-linux-x86_64</id><activation><os><name>linux</name><arch>amd64</arch></os></activation><properties><snappea.natives>natives-linux-x86_64</snappea.natives></properties></profile>
  <profile><id>snappea-linux-aarch64</id><activation><os><name>linux</name><arch>aarch64</arch></os></activation><properties><snappea.natives>natives-linux-aarch64</snappea.natives></properties></profile>
  <profile><id>snappea-macos-x86_64</id><activation><os><family>mac</family><arch>x86_64</arch></os></activation><properties><snappea.natives>natives-macos-x86_64</snappea.natives></properties></profile>
  <profile><id>snappea-macos-aarch64</id><activation><os><family>mac</family><arch>aarch64</arch></os></activation><properties><snappea.natives>natives-macos-aarch64</snappea.natives></properties></profile>
  <profile><id>snappea-windows-x86_64</id><activation><os><family>windows</family><arch>amd64</arch></os></activation><properties><snappea.natives>natives-windows-x86_64</snappea.natives></properties></profile>
</profiles>

Gradle (Kotlin DSL):

val snappeaOs = System.getProperty("os.name").lowercase().let {
    if (it.startsWith("mac")) "macos" else if (it.startsWith("windows")) "windows" else "linux" }
val snappeaArch = if (System.getProperty("os.arch") in setOf("aarch64", "arm64")) "aarch64" else "x86_64"
dependencies {
    implementation("io.github.crowecawcaw:snappea:$snappeaVersion")
    testRuntimeOnly("io.github.crowecawcaw:snappea:$snappeaVersion:natives-$snappeaOs-$snappeaArch")
}

The checker is found from .binary(...), then SNAPPEA_BIN, then the natives jar, then snappea on PATH. The natives jar's binary is copied to a per-version user cache on first use and checked against the SHA-256 in the jar.

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 shop;

import io.github.crowecawcaw.snappea.emit.SnappeaEmit;
import java.util.HashMap;
import java.util.Map;

public final class Inventory {
    private final Map<String, Integer> stock = new HashMap<>();
    private final Map<String, Integer> reservations = new HashMap<>();

    public void addProduct(String sku, int units) {
        stock.put(sku, units);
        SnappeaEmit.emit("eStocked", sku, Map.of("units", units));
    }

    public void reserve(String sku, String order, int units) {
        if (units > stock.get(sku)) throw new IllegalStateException("insufficient stock");
        stock.put(sku, stock.get(sku) - units);
        reservations.put(sku + "/" + order, units);
        SnappeaEmit.emit("eReserved", sku, Map.of("order", order, "units", units)); // after the change
    }
}

Point the helper at the specs and register the extension:

spec_files = specs

package shop;

import io.github.crowecawcaw.snappea.SnappeaExtension;
import org.junit.jupiter.api.Test;
import org.junit.jupiter.api.extension.ExtendWith;

@ExtendWith(SnappeaExtension.class)
class InventoryTest {
    @Test
    void twoOrdersForTheLastUnits() {
        var inventory = new Inventory();
        inventory.addProduct("coffee", 3);
        inventory.reserve("coffee", "order-1", 2);
        try {
            inventory.reserve("coffee", "order-2", 2);
        } catch (IllegalStateException rejected) {
            // rejecting order-2 is fine too
        }
    }
}

mvn 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:

[ERROR] shop.InventoryTest.twoOrdersForTheLastUnits -- Time elapsed: 0.129 s <<< FAILURE!
io.github.crowecawcaw.snappea.SpecViolation:
P spec InventoryCorrect was broken: reservation exceeds available stock

  Events (key "coffee"):
      1  eStocked   units=3                shop/Inventory.java:13
      2  eReserved  units=2 order=order-1  shop/Inventory.java:19
      3  eReserved  units=2 order=order-2  shop/Inventory.java:19  <- broke the spec here

  Spec: specs/inventory.p:27
  snappea output: /tmp/snappea/recording-6629023866151738740

Test setup

Every test: the JUnit 5 extension

Pick one registration:

@ExtendWith(SnappeaExtension.class)                 // settings from snappea.properties
class InventoryTest { ... }

@RegisterExtension                                  // settings in code
static final SnappeaExtension SNAPPEA = SnappeaExtension.builder().specs("InventoryCorrect").build();

Or every test class, with junit.jupiter.extensions.autodetection.enabled=true in junit-platform.properties. An autodetected extension steps aside in classes that register their own.

• A recording starts before @BeforeEach and is checked after @AfterEach, so fixtures are checked too.
• A test that already failed keeps its failure; the check's result is attached as suppressed.
• Inject the recording as a Recording parameter when code needs it explicitly.
• In marked mode only tests or classes annotated @Snappea are checked.
• A recording with no events and strict off passes without running the checker.
• Several extensions on one class need .name("billing") and @SnappeaRecording("billing") Recording parameters.

Per-test options:

@Test @Snappea(skip = Snappea.ALL) void notChecked() { ... }
@Test @Snappea(skip = "SmallOrders") void notThisSpec() { ... }
@Test @Snappea(checkHot = true) void everyReservationShips() { ... }

Explicit checks

var observer = SnappeaObserver.builder().build(); // settings from snappea.properties

try (var recording = observer.recording("reserve then release")) {
    var inventory = new Inventory();              // emits through SnappeaEmit
    inventory.addProduct("coffee", 3);
    inventory.reserve("coffee", "order-1", 2);
}                                                 // checked here

Closing checks once and throws SpecViolation or SetupError. The manual form is observer.start(label), then recording.stop() and recording.check(). recording.emit(...) and emitAt(...) write to that recording only, for code that takes an injected sink. Join worker threads and child processes before the check: an event emitted after the check throws.

Negative controls

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

var violation = Recording.expectViolation("InventoryCorrect", "exceeds available stock", () -> {
    try (var recording = observer.recording("oversell")) { ... }
});

It fails if the check passes or another spec is violated. Enclosing recordings, such as the extension's, ignore that spec for the rest of the test.

Property tests

Jupiter callbacks do not wrap jqwik tries: open observer.recording(...) inside each @Property method, with a CoverageCollector closed in @AfterContainer.

Emitting events

SnappeaEmit.emit("eReserved", sku, Map.of("order", order, "units", units)); // event, key, payload
SnappeaEmit.emit("eClosed", sku);                                            // no payload
SnappeaEmit.emitAt(commitTime, "eReserved", sku, payload);                   // when it happened

• Payload: a Map or record for a P named tuple, a single value, or none. Enums go by name, collections and arrays as lists.
• 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, at the same place production code would publish it.
• Each line records the call site, a per-process sequence number and a wall-clock time that never goes backwards.

Where an event goes, in order:

1. A recording in this JVM: the one the current thread (or the thread that started it) opened.
2. SNAPPEA_EVENTS_DIR, when a test started this process.
3. The production sink, if set.
4. Nowhere: two volatile reads. SnappeaEmit.enabled() skips building an expensive payload.

In production

SnappeaEmit.setSink(Sink.file(Path.of("/var/log/app/events/inventory.jsonl")));
// or Sink.stdout(), Sink.writer(out), Sink.callback(line -> ...)
// ... at shutdown:
SnappeaEmit.close(); // writes what is queued

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

A background thread writes the lines. emit never throws or waits: drops (full queue, I/O error, bad payload) are counted in SnappeaEmit.dropped(). SnappeaEmit.flush(timeout) waits for the queue.

Other processes

var worker = new ProcessBuilder("java", "-cp", classpath, "example.Worker");
worker.environment().putAll(recording.environment()); // adds SNAPPEA_EVENTS_DIR
worker.start().waitFor();                             // join before the check

recording.addEventsDir(Path.of("volumes/events"));     // a folder this recording did not create
recording.addLog(Path.of("app-events.jsonl"));         // JSON event lines
recording.addLog(Path.of("server.log"), line -> ...);  // returns a LogEvent, or null to skip

recording.eventsDir() is the folder itself, for containers or other services writing event lines. Events are ordered by timestamp per key; equal times keep this process's events first.

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. SpecViolation is an AssertionFailedError, so JUnit and jqwik treat it as an ordinary failure. Its fields: spec(), key(), message(), location(), events() (each with event(), payload(), src()), liveness() and others(). Anything else is a SetupError whose kind() is:

Both keep their artifacts folder (artifacts()) and the checker's report (report()). Assert on fields, not message text.

Reference

Settings

Set in snappea.properties (searched from the working directory upwards, then the classpath), or as snappea.* keys in junit-platform.properties. Paths resolve against the file's folder. The builders (SnappeaObserver.builder(), SnappeaExtension.builder()) have a method per key in camel case: .specFiles(...), .checkHot(...), and so on. Precedence: builder, environment variable, file, default. Unknown keys are an error.

spec_files = specs/*.p          # paths, folders (every .p) or globs; comma-separated
specs = InventoryCorrect        # default: every spec in spec_files
strict = true                   # default: true when specs is set, else false
unknown_events = error          # ignore | warn | error
timeout = 30s
artifacts = target/snappea      # default: <tmp>/snappea; kept only for failed checks
coverage = target/coverage/monitor.json
mode = auto                     # auto | marked | off

Environment variables

Suite coverage

When the run ends, the extension prints the P spec states, handlers, statements and branches all checks reached, and lists what no check reached. It writes no file. Set coverage (or SNAPPEA_COVERAGE) to a path to also keep it as JSON; SNAPPEA_COVERAGE=off (or coverage = off) turns it off. Outside JUnit, observer.coverage() gives a collector to pass to observer.recording(label, collector); closing it prints the summary and writes the configured path, if any. Collectors merge into an existing file under a lock, so forks share one path; delete it before a run.

API

• io.github.crowecawcaw:snappea on javadoc.io

Runnable projects: Java examples.