Tutorials
Guided walk-throughs of Semantifyr. The Traffic Light series builds a small state machine from scratch and progressively introduces the language constructs you will need to read and write real semantic libraries.
If you are new to Semantifyr, start with Direct Modeling. The Traffic Light tutorials run in your browser with no setup: every step opens in a live editor embedded in the page.
Traffic Light series
| Tutorial | Description |
|---|---|
| Direct Modeling | Build a basic traffic light and intersection directly, with no reusable abstractions. Discover and fix a safety bug. Introduces classes, transitions, properties, choice/assume, containment, @VerificationCase, AG/EF. |
| Building a Library | Refactor the traffic light into a small Statechart library with first-class State and Transition classes. Introduces inheritance, container/opposite, subsets, feature-typed variables, nothing, inline for choice, and the init-chain pattern. |
| Advanced Tutorial | Extend the small library with patterns from real semantic libraries: hierarchical states, entry actions, and events with triggers, then pre-empt the lights with a global emergency override. Introduces composite states, inline if, State subclasses, redefine contains, havoc for modeling the environment, and global features. |
SysML v2
| Tutorial | Description |
|---|---|
| Verifying SysML v2 Models | Model a switch and a lamp in SysML v2, verify requirements in the live editor, and read a counterexample. |