Table of Contents

CLI reference: sek

sek is the SpecExplorerKit command-line tool. Run sek with no arguments (or sek --help) for usage.

sek <command> [options]
Command Purpose
init Scaffold a .specexplorerkit/ project
validate Check the model and Cord line up
explore Explore a machine into a .seexpl graph
view Render a .seexpl graph
test Explore, then replay against the SUT (conformance)
generate Generate an xUnit test project from the exploration
z3 Self-test the Z3 backend
version Print the version

Most commands accept --project <dir> to point at the project directory (the folder containing .specexplorerkit/config.json); it defaults to the current directory.

sek init

Scaffold a new project.

sek init [--project <dir>]

Creates .specexplorerkit/config.json (and an out/ directory) with a starter configuration you then edit to point at your model, Cord, and (optionally) binding.

sek validate

Static checks that the model and Cord agree.

sek validate [--project <dir>]

Reports:

  • the resolved model type, its rules, and accepting-condition count;
  • the number of Cord configs and machines;
  • any Cord action with no matching model rule;
  • any machine that constructs from an unknown config/machine.

Exit code is non-zero if problems are found.

sek explore

Explore a machine into a transition system.

sek explore <machine> [--project <dir>] [--solver z3|enum] [--out <file>]
Option Default Meaning
<machine> — the Cord machine to explore (required)
--project <dir> current dir project directory
--solver z3\|enum z3 parameter solver (Z3 or enumerative)
--out <file> .specexplorerkit/out/<machine>.seexpl output path

Prints a summary (states, transitions, accepting states, and (bound hit) if a bound stopped the search). If the machine has no model program (pure Cord behavior), SEK explores it in behavior mode.

sek view

Render a .seexpl graph.

sek view <file.seexpl> [--format mermaid|dot|html] [--out <file>]
Option Default Meaning
<file.seexpl> — the graph to render (required)
--format mermaid mermaid, dot, or html
--out <file> stdout write to a file instead of stdout

sek test

Explore a machine, then replay every transition against the configured binding and report conformance.

sek test <machine> [--project <dir>] [--solver z3|enum]

Requires a binding block in the project config. Prints transitions replayed, succeeded, failed, actions covered, and a TEST PASSED / TEST FAILED verdict. Exit code is non-zero on failure. sek run is an alias.

sek generate

Generate a runnable xUnit test project from a machine's exploration. SEK selects witness paths that cover the model's transitions (each path starts at the initial state and ends at an accepting state where reachable), then emits a test project whose tests replay each action sequence against the configured SUT binding.

sek generate <machine> [--project <dir>] [--out <dir>] [--namespace <ns>] [--max <n>] [--solver z3|enum]
Option Default Meaning
<machine> — the machine to generate tests for (required)
--project <dir> current dir project directory
--out <dir> .specexplorerkit/out/<machine>Tests output test-project directory
--namespace <ns> <binding-namespace>.Tests namespace for the generated tests
--max <n> 50 maximum number of test paths to emit
--solver z3\|enum z3 parameter solver used during exploration

Requires a binding in the project config (the generated tests drive the SUT). The command writes a <Machine>Tests.csproj and <Machine>Tests.cs, then prints how to run them:

sek generate TpccExploration --project ./MyProject
# Generated 50 xUnit test(s) covering 667/12706 transitions.
# Run with: dotnet test ".../TpccExplorationTests"

The generated project snapshots the built binding and its sibling DLL/.deps.json dependencies under BindingAssets, copies them to test output, and loads that snapshot. There is no SEK_BINDING fallback. Rebuild and regenerate after binding changes.

sek z3

Self-test the Z3 backend; prints SATISFIABLE and a sample model if the native Z3 library loaded correctly.

sek z3

sek version

Print the tool version.

sek version

Running the in-repo build

If you haven't installed the global tool, invoke the freshly built assembly:

dotnet src/Sek.Cli/bin/Debug/net10.0/sek.dll <command> [options]
Edit this page