atsvc
Demonstrates: a protocol state machine — the AT Service task scheduler — modeled as a job lifecycle.
- Project:
samples/atsvc - Model:
ATSvc.Model.AtsvcModel
What it covers
AddJob(command, time) creates a job; GetJobInfo(Job) observes one; DeleteJob(Job)
removes one. The Job parameters range over reachable jobs; command/time come
from Cord Condition.In, and a Condition.IsTrue predicate rejects invalid
combinations — mirroring the classic sample's parameter slicing.
Result: 10 states / 42 transitions / 10 accepting.
Run it
dotnet build samples/atsvc/Model/atsvc.Model.csproj
sek explore ModelProgramWithConfigParameters --project samples/atsvc
sek explore ModelProgramWithTwoJobsPattern --project samples/atsvc
Scenario slicing
ModelProgramWithTwoJobsPattern slices the model with AddTwoJobsPattern via ||.
The direct model explores to 10 states / 42 transitions / 10 accepting states; the
sliced product explores to 35 states / 72 transitions / 10 accepting states. See
Writing Cord → Scenario slicing.
Porting note
The classic sample used a JobInfo struct and MapContainer state. In the SEK
port the struct is flattened into value parameters (which the Z3 solver handles
directly) and the map becomes a List<Job>; the protocol shape is preserved. See
Migrating from Spec Explorer.