ModelJUnit Examples Catalogue

An annotated guide to every example model in modeljunit-samples/. Examples are grouped by difficulty — start at the top and work down.

---

Beginner — Start Here

These examples teach the core concepts with minimal complexity.

Class	Package	What it demonstrates
SimpleSet	examples	The canonical first model. A set with two boolean elements, 4 states, 16 transitions. No guards. Teaches FsmModel, getState(), reset(), @Action.
FSM	examples	A minimal 3-state FSM with explicit state variable. Good for seeing the simplest possible model structure.
SpecialFSM	examples	A small FSM with self-loops. Useful for understanding how self-transitions appear in coverage metrics.
SpecialFSMNoLoops	examples	Same as SpecialFSM but with guards that prevent self-loops. Shows how guards change the state graph.

---

Intermediate — Adaptors, Guards, and SUTs

These examples introduce connecting models to real code and using guards.

Class	Package	What it demonstrates
SimpleSetWithAdaptor	examples	Adaptor pattern: connects the SimpleSet model to a real Set<String> SUT. Shows assertion-based oracles via checkSUT().
SmartSetAdaptor	examples	State abstraction in adaptors: maps one model boolean to 12 SUT strings. Shows how to test complex SUT behaviour with a simple model.
StringSet	examples	A real Set<String> implementation (the SUT). Not a model itself — used as the system under test by the adaptor examples.
StringSetBuggy	examples	A deliberately buggy Set<String> implementation. Use with SimpleSetWithAdaptor to see how MBT finds bugs automatically.
LargeSet	examples	A model with a larger state space. Useful for experimenting with how different testers handle scale.
SizeExperiments	examples	Utility for running coverage experiments across different model sizes and tester configurations.

---

Advanced — Real-World Models

These examples model realistic systems with complex state spaces, multiple interacting variables, and rich guard logic.

Class	Package	What it demonstrates
ECinema	examples.ecinema	Web-based cinema booking system. Enum page states, user registration/login, ticket purchase/deletion. Shows requirement traceability tags, shared guard methods, and multiple actions per input combination. The most detailed example in the project.
Showtime	examples.ecinema	Domain object for ECinema — movie showtime with ticket inventory.
User	examples.ecinema	Domain object for ECinema — registered user with credentials and tickets.
QuiDonc	examples	France Telecom directory service protocol. A real-world case study from Utting & Legeard's textbook. Complex guard logic and protocol state machine.
SimCard	examples.gsm	GSM 11-11 SIM card protocol model. Multi-level authentication (PIN/PUK), file system navigation, and security lockout.
GSM11Impl	examples.gsm	SUT implementation for the GSM SIM card model.
SimCardAdaptor	examples.gsm	Adaptor connecting the SimCard model to the GSM11Impl SUT.
SimFile	examples.gsm	Domain object for the GSM model — SIM card file system entry.

---

Timing Models

These examples demonstrate ModelJUnit's timed/real-time FSM extensions.

Class	Package	What it demonstrates
SimpleTimedLight	timing.examples	Simplest timed model — a light with time-based transitions.
TrafficLight	timing.examples	Traffic light with timed phase changes.
AlarmClock	timing.examples	Alarm clock with set/snooze/dismiss actions and timeouts.
PhoneModel	timing.examples	Phone call model with ringing timeouts and call duration.

---

Suggested Learning Path

1. Read the MBT Tutorial first
2. Study SimpleSet → SimpleSetWithAdaptor → SmartSetAdaptor (adaptor progression)
3. Try running SimpleSetWithAdaptor with StringSetBuggy to see bug detection in action
4. Study ECinema for a real-world EFSM with complex guards
5. Explore SimCard / GSM11Impl for a protocol-level model with security states
6. Look at the timing examples if your system has time-dependent behaviour