Samples

To demonstrate fidelity to Spec Explorer, the original Spec Explorer 2010 sample suite has been ported to SEK and validated. Each sample lives under samples/<name> in the repository; their original source and byte-identical Cord fixtures are preserved under samples-source/<name> for comparison; legacy project and build artifacts are intentionally omitted.

Sample	What it demonstrates	Result
Operators	every implemented Cord operator in supported root forms	18 machines explore (e.g. Party 6/6/3)
ParameterGeneration	Z3 combination strategies + predicate pruning	Product 27, Pairwise 11, Constraint 21
Account	dynamic reachable-object domains	10 states / 58 transitions
PubSub	pub/sub object model, message queues	500 states (bound hit)
atsvc	task-scheduler protocol	10 states / 42 transitions
chat	request/response chat protocol	1000 states (bound hit)
SMB2	session/tree/file lifecycle	17 states / 32 transitions
Sailboat	stateful model + pairwise + state-dependent domains	4000 states (bound hit)
RequirementReport	post-processing/reporting	HTML reports via sek view
TPC-C	large model + full conformance	2,446 / 12,706; conformance PASSED

Reproduce

From the repository root:

dotnet build Sek.slnx
pwsh scripts/validate.ps1     # builds each sample model and explores it

Or run one:

sek explore <Machine> --project samples/<Name>

Note

Some models (chat, PubSub, Sailboat) have intentionally unbounded state spaces; exploration reports (bound hit) when a StateBound/StepBound truncates the search — matching the classic samples' own bounds.