Model-Based Testing with ModelJUnit — A Complete Tutorial¶

This tutorial teaches you model-based testing (MBT) from scratch using ModelJUnit. You will learn how to design finite-state machine models, generate tests automatically, connect models to real code, and interpret coverage metrics — all using examples from this project. No prior MBT experience is required.

Tip: If you want a quick API reference instead, see the Getting Started guide. This tutorial focuses on how to think about model-based testing.

1. What is Model-Based Testing?¶

In traditional testing you write individual test cases by hand: set up some state, call a method, check the result. This works, but it has problems:

You have to imagine every interesting scenario yourself
You tend to test the "happy path" and miss edge cases
When the system changes, you rewrite tests manually

Model-based testing takes a different approach. Instead of writing test cases, you write a model — a simplified description of how your system behaves. Then a tool (ModelJUnit) automatically generates test sequences by exploring the model's state space. The tool can find paths through your system that you would never think to write by hand.

The model is a finite-state machine (FSM): a set of states, a set of transitions (actions) between states, and an initial state. ModelJUnit walks through this machine — randomly, greedily, or systematically — firing actions and measuring how much of the model it has covered.

@startuml
title How Model-Based Testing Works

rectangle "You write" {
  (FSM Model) as model
}

rectangle "ModelJUnit generates" {
  (Test Sequences) as tests
}

rectangle "Measured by" {
  (Coverage Metrics) as coverage
}

model --> tests : "Tester explores\nstate space"
tests --> coverage : "State, transition,\npair coverage"
coverage --> model : "Low coverage?\nImprove model"
@enduml

2. Your First FSM Model — SimpleSet¶

Let's start with the simplest possible model: a set that can contain two elements, s1 and s2. Each element is either present or absent, giving us four states.

The state diagram¶

@startuml
title SimpleSet — 4 states, 16 transitions
hide empty description

state "FF" as FF
state "TF" as TF
state "FT" as FT
state "TT" as TT

[*] --> FF

FF --> TF : addS1
FF --> FT : addS2
FF --> FF : removeS1
FF --> FF : removeS2

TF --> TF : addS1
TF --> TT : addS2
TF --> FF : removeS1
TF --> TF : removeS2

FT --> TT : addS1
FT --> FT : addS2
FT --> FT : removeS1
FT --> FF : removeS2

TT --> TT : addS1
TT --> TT : addS2
TT --> FT : removeS1
TT --> TF : removeS2
@enduml

Each state is a two-character string: the first character is T or F for whether s1 is present, the second for s2. Every action is available in every state (no guards), so there are 4 states × 4 actions = 16 transitions.

The code¶

package nz.ac.waikato.modeljunit.examples;

import nz.ac.waikato.modeljunit.Action;
import nz.ac.waikato.modeljunit.FsmModel;

public class SimpleSet implements FsmModel {
    protected boolean s1, s2;

    public Object getState() {
        return (s1 ? "T" : "F") + (s2 ? "T" : "F");
    }

    public void reset(boolean testing) {
        s1 = false;
        s2 = false;
    }

    @Action public void addS1()    { s1 = true;  }
    @Action public void addS2()    { s2 = true;  }
    @Action public void removeS1() { s1 = false; }
    @Action public void removeS2() { s2 = false; }
}

Source: modeljunit-samples/.../examples/SimpleSet.java

The three contracts¶

Every FsmModel must satisfy three contracts:

getState() — returns an object that identifies the current state. ModelJUnit uses equals() to decide whether two states are the same. Choose a return type that distinguishes the states you care about (strings, enums, or tuples).
reset(boolean testing) — returns the model to its initial state. ModelJUnit calls this before each test sequence and whenever it needs to restart exploration. The testing parameter is true during test generation (you can use it to skip expensive setup that only matters for real SUT connections).
@Action methods — each annotated method represents one transition. ModelJUnit discovers them by reflection. The method name becomes the action name in coverage reports.

Running it¶

import nz.ac.waikato.modeljunit.*;
import nz.ac.waikato.modeljunit.coverage.*;

Tester tester = new GreedyTester(new SimpleSet());
tester.addListener(new VerboseListener());
tester.addCoverageMetric(new TransitionCoverage());
tester.generate(100);
tester.printCoverage();

Output looks like:

reset
addS1  [FF->TF]
addS2  [TF->TT]
removeS1  [TT->FT]
removeS2  [FT->FF]
...
TransitionCoverage: 16/16 (100.0%)

The GreedyTester prefers transitions it hasn't taken yet, so it reaches 100% transition coverage quickly on this small model.

3. Designing Good States¶

The most important decision in model-based testing is what your states represent. Get this wrong and your model either has too few states (tests miss important scenarios) or too many (state explosion makes testing impractical).

A bad design¶

Suppose you're modelling a shopping cart. A naive approach uses the exact cart contents as the state:

State = {item1, item3}     // one state per unique combination

With 20 possible items, that's 2²⁰ = over a million states. ModelJUnit will never explore them all.

A better design¶

Abstract away the details. What matters for testing the cart's behaviour?

State = "EMPTY"       // no items
State = "NON_EMPTY"   // one or more items
State = "CHECKED_OUT" // order placed

@startuml
title Shopping Cart — Abstracted States
hide empty description

[*] --> EMPTY

EMPTY --> NON_EMPTY : addItem
NON_EMPTY --> NON_EMPTY : addItem
NON_EMPTY --> NON_EMPTY : removeItem [size > 1]
NON_EMPTY --> EMPTY : removeItem [size == 1]
NON_EMPTY --> CHECKED_OUT : checkout
CHECKED_OUT --> EMPTY : newOrder
@enduml

Three states, six transitions — easy to explore exhaustively. The model captures the behavioural differences (you can't checkout an empty cart, you can't add items after checkout) without tracking every possible combination of items.

The rule of thumb¶

States should represent behavioural differences — situations where different actions are available or behave differently
Internal variables (like s1, s2 in SimpleSet) track details the model needs, but getState() should only expose what matters for which transitions are possible
If your model has more than ~20–30 states, you probably need more abstraction

4. Guards and Extended FSMs (EFSMs)¶

In SimpleSet, every action is available in every state. Real systems aren't like that — you can't remove an item from an empty cart, you can't log in when you're already logged in. Guards let you express these constraints.

A guard is a method named <actionName>Guard() that returns boolean. When it returns false, ModelJUnit won't fire that action.

Example: a guarded counter¶

@startuml
title Guarded Counter
hide empty description

state "count=0" as S0
state "count=1" as S1
state "count=2" as S2

[*] --> S0

S0 --> S1 : add
S1 --> S2 : add
S1 --> S0 : remove [count > 0]
S2 --> S1 : remove [count > 0]
@enduml

public class Counter implements FsmModel {
    private int count = 0;

    public Object getState() { return count; }
    public void reset(boolean testing) { count = 0; }

    @Action public void add()    { count++; }
    @Action public void remove() { count--; }

    // Guard: remove is only available when count > 0
    public boolean removeGuard() { return count > 0; }
}

The naming convention is strict: for an action called remove, the guard must be called removeGuard. ModelJUnit discovers it by reflection.

FSM vs EFSM¶

A pure FSM has a fixed set of states and no guards — like SimpleSet
An Extended FSM (EFSM) has internal variables and guards that constrain which transitions are available — like the counter above

Most real models are EFSMs. The internal variables let you track richer state without exploding the state space, because getState() can abstract over the details.

The ECinema model — a real EFSM¶

The ECinema example models a web-based cinema ticket booking system. It has an enum for page states, internal variables for the current user and available tickets, and many guards:

@startuml
title ECinema — Page-Based State Machine (Simplified)
hide empty description

state "welcome" as W
state "register" as R
state "displayTickets" as D
state "terminal" as T

[*] --> W

W --> W : login* [state == welcome]
W --> R : gotoRegister [state == welcome]
W --> D : displayTickets [logged in]
W --> W : buyTicket* [logged in, tickets left]
W --> W : logout [logged in]
W --> T : close [all tickets returned]

R --> W : register* [state == register]

D --> W : back
D --> D : deleteTicket* [has tickets]
D --> D : deleteAllTickets* [has tickets]
D --> W : logout [logged in]
@enduml

Key design decisions in this model:

States are web pages, not data states — this keeps the state space small
Multiple login actions (loginEricOk, loginEricBad, loginEmpty, etc.) model different input combinations as separate transitions, so coverage metrics track which login scenarios have been tested
Guards use shared helper methods — e.g. loginGrd() is reused by all login guards
Requirement tags in comments (/*@REQ: CIN_030 @*/) trace model behaviour back to requirements

Source: modeljunit-samples/.../ecinema/ECinema.java

The getState() method returns the page name plus the current user:

public Object getState() {
    return state.toString()
        + ((currentUser == null) ? "" : "_" + currentUser.name);
}

This means "welcome page logged in as ERIC" and "welcome page not logged in" are different states — which is correct, because different actions are available in each.

5. Connecting a Model to Real Code — The Adaptor Pattern¶

A model by itself only tests the model. To test real code, you connect the model to a system under test (SUT) using the adaptor pattern:

Override each @Action method
Call the SUT in the overridden method
Assert that the SUT's state matches the model's state

@startuml
title Adaptor Pattern

rectangle "Model\n(SimpleSet)" as model
rectangle "Adaptor\n(SimpleSetWithAdaptor)" as adaptor
rectangle "SUT\n(StringSet)" as sut

model <|-- adaptor : extends
adaptor --> sut : calls & checks
@enduml

SimpleSetWithAdaptor¶

This adaptor extends the SimpleSet model and connects it to a real Set<String> implementation:

public class SimpleSetWithAdaptor implements FsmModel {
    protected Set<String> sut_;
    protected boolean s1, s2;
    protected String str1 = "some string";
    protected String str2 = "";

    public SimpleSetWithAdaptor(Set<String> sut) {
        sut_ = sut;
    }

    public void reset(boolean testing) {
        s1 = false;
        s2 = false;
        sut_.clear();  // reset the SUT too
    }

    @Action public void addS1() {
        s1 = true;
        sut_.add(str1);     // call the SUT
        checkSUT();          // verify SUT matches model
    }

    @Action public void removeS2() {
        // test the return value of remove()
        assert s2 == sut_.remove(str2);
        s2 = false;
        checkSUT();
    }

    protected void checkSUT() {
        int size = (s1 ? 1 : 0) + (s2 ? 1 : 0);
        assert size == sut_.size();
        assert s1 == sut_.contains(str1);
        assert s2 == sut_.contains(str2);
    }
}

Source: modeljunit-samples/.../examples/SimpleSetWithAdaptor.java

The key insight: the model's boolean variables (s1, s2) are the oracle — they define what the SUT should contain. After every action, checkSUT() compares the SUT's actual state against the model's expected state.

SmartSetAdaptor — state abstraction in adaptors¶

Sometimes you want to test more complex SUT behaviour than the model directly represents. SmartSetAdaptor maps the model's s2 boolean to twelve strings in the SUT:

public class SmartSetAdaptor extends SimpleSet {
    protected final int S2_STRINGS = 12;
    protected Set<String> sut_;

    @Action public void addS2() {
        super.addS2();
        for (int i = 1; i <= S2_STRINGS; i++)
            sut_.add("s" + i);   // add 12 strings at once
        checkSUT();
    }
}

Source: modeljunit-samples/.../examples/SmartSetAdaptor.java

The model stays small (4 states, 16 transitions) but the SUT is exercised with 13 elements — enough to force a HashSet to resize internally. This is state abstraction: the model takes a simplified view of a more complex reality.

6. Choosing a Tester¶

ModelJUnit provides four test generation algorithms. Each explores the model's state space differently:

Tester	Strategy	Best for
`RandomTester`	Uniform random walk	Quick smoke testing, large state spaces
`GreedyTester`	Prefers least-visited transitions	Reaching high coverage quickly
`LookaheadTester`	Greedy with configurable lookahead depth	Models with hard-to-reach states
`QuickTester`	Shortest-path traversal	Minimising test sequence length

@startuml
title Tester Selection Guide

start
if (State space is large\nor unknown?) then (yes)
  :Use **RandomTester**;
  note right: Fast, but may miss\nhard-to-reach states
elseif (Need high coverage\nquickly?) then (yes)
  :Use **GreedyTester**;
  note right: Good default choice\nfor most models
elseif (Model has states that\nrequire specific paths?) then (yes)
  :Use **LookaheadTester**;
  note right: Set depth to 2-5\nfor best results
else (minimal tests)
  :Use **QuickTester**;
  note right: Shortest paths,\nfewest steps
endif
stop
@enduml

Practical guidance¶

Start with GreedyTester — it's the best default. It reaches high coverage quickly because it prefers transitions it hasn't taken yet.
Switch to RandomTester if your model is very large (hundreds of states) and you just want to exercise it broadly.
Use LookaheadTester when GreedyTester gets stuck — some models have states that require a specific sequence of actions to reach. Lookahead depth of 2–3 usually helps.
Use QuickTester when you want the shortest possible test sequences (e.g. for regression test suites).

Example: comparing testers¶

FsmModel model = new ECinema();

// Random: may take thousands of steps to cover everything
Tester random = new RandomTester(model);
random.addCoverageMetric(new TransitionCoverage());
random.generate(10000);
random.printCoverage();

// Greedy: typically covers the same ground in fewer steps
model.reset(true);
Tester greedy = new GreedyTester(model);
greedy.addCoverageMetric(new TransitionCoverage());
greedy.generate(10000);
greedy.printCoverage();

7. Understanding Coverage Metrics¶

Coverage metrics tell you how thoroughly ModelJUnit has explored your model. They are the primary feedback mechanism for improving your model and your tests.

The three main metrics¶

Metric	What it measures	What low coverage means
`StateCoverage`	% of distinct states visited	Some states are unreachable — check your guards and reset
`TransitionCoverage`	% of distinct transitions fired	Some transitions are guarded too tightly or require specific state sequences
`TransitionPairCoverage`	% of consecutive transition pairs exercised	The tester isn't exploring diverse paths — try `LookaheadTester` or more steps

Reading the output¶

StateCoverage: 4/4 (100.0%)
TransitionCoverage: 14/16 (87.5%)
TransitionPairCoverage: 45/64 (70.3%)

This tells you: - All 4 states were visited ✓ - 2 transitions were never fired — find out which ones and check their guards - Only 70% of transition pairs were covered — the tester is taking repetitive paths

What to do when coverage is low¶

@startuml
title Improving Coverage

start
:Run tester, check coverage;

if (State coverage < 100%?) then (yes)
  :Some states are unreachable;
  :Check guards — are they too restrictive?;
  :Check reset() — does it reach the right initial state?;
elseif (Transition coverage < 100%?) then (yes)
  :Some transitions never fire;
  :Check guards on the missing transitions;
  :Try LookaheadTester with depth 2-3;
  :Increase step count;
elseif (Transition pair coverage low?) then (yes)
  :Tester is taking repetitive paths;
  :Increase step count;
  :Try LookaheadTester;
  :Consider if model needs more states;
else (all good)
  :Coverage is satisfactory;
endif
stop
@enduml

Using coverage in JUnit 5¶

@Test
void fullTransitionCoverage() {
    Tester tester = new GreedyTester(new SimpleSet());
    TransitionCoverage tc = new TransitionCoverage();
    tester.addCoverageMetric(tc);
    tester.generate(500);
    assertEquals(1.0, tc.getCoverage(), 0.01,
        "Expected 100% transition coverage");
}

This makes coverage a pass/fail criterion in your CI pipeline. If the model can't achieve full transition coverage, either the model has unreachable transitions (a modelling bug) or the tester needs more steps.

8. A Complete Walkthrough — ECinema¶

Let's put everything together with a real-world example. The ECinema model represents a web-based cinema ticket booking system with user registration, login, ticket purchase, and ticket management.

The domain¶

@startuml
title ECinema Domain Model

class User {
  name : String
  password : String
  tickets : Set<String>
}

class Showtime {
  movie : String
  dateTime : int
  tickets : Set<String>
  ticketsLeft : int
  buyButtonActive : boolean
  clearAllButtonActive : boolean
}

class ECinema {
  state : State
  currentUser : User
  allUsers : Map<String, User>
  showtimes : Showtime[2]
}

ECinema --> "0..1" User : currentUser
ECinema --> "*" User : allUsers
ECinema --> "2" Showtime : showtimes
User --> "*" Showtime : tickets (via String refs)
@enduml

State design decisions¶

The model uses page states (welcome, register, displayTickets, terminal) as the primary state dimension, combined with the current user identity:

public Object getState() {
    return state.toString()
        + ((currentUser == null) ? "" : "_" + currentUser.name);
}

This gives states like welcome, welcome_ERIC, register, displayTickets_ERIC. The state space stays manageable because we don't include ticket counts or showtime details in the state — those are internal variables that affect guards but don't define distinct behavioural states.

Guard design¶

The model uses shared guard methods to avoid repetition:

// All login actions share the same guard
public boolean loginEmptyGuard()      { return loginGrd(); }
public boolean loginEricOkGuard()     { return loginGrd(); }
public boolean loginEricBadGuard()    { return loginGrd(); }

private boolean loginGrd() { return state == State.welcome; }

Each concrete login action (loginEricOk, loginEricBad, loginEmpty) represents a different input combination. This is a deliberate design choice: by making each combination a separate action, transition coverage tells you which login scenarios have been tested.

Multiple actions for input combinations¶

@Action public void loginEmpty()       { login("", "ETO"); }
@Action public void loginEricOk()      { login("ERIC", "ETO"); }
@Action public void loginEricBad()     { login("ERIC", "ACH"); }
@Action public void loginAmandineOk()  { login("AMANDINE", "ACH"); }

The shared login() method contains the actual logic with requirement traceability tags:

public void login(String userName, String userPassword) {
    if (userName.equals("")) {
        message = "EMPTY_USERNAME";           /*@REQ: CIN_031 @*/
    } else if (userPassword.equals("")) {
        message = "EMPTY_PASSWORD";           /*@REQ: CIN_032 @*/
    } else if (!allUsers.containsKey(userName)) {
        message = "UNKNOWN_USER_NAME_PASSWORD"; /*@REQ: CIN_033 @*/
    } else {
        User user_found = allUsers.get(userName);
        if (user_found.password.equals(userPassword)) {
            currentUser = user_found;
            message = "WELCOME";              /*@REQ: CIN_030 @*/
        } else {
            message = "WRONG_PASSWORD";       /*@REQ: CIN_034 @*/
        }
    }
}

Running the ECinema model¶

Tester tester = new RandomTester(new ECinema());
GraphListener graph = tester.buildGraph(100000);
tester.addCoverageMetric(new TransitionCoverage());
tester.addCoverageMetric(new StateCoverage());
tester.addCoverageMetric(new ActionCoverage());
tester.generate(10000);
tester.printCoverage();

The buildGraph(100000) call explores up to 100,000 steps to discover the full state graph. This is necessary because the ECinema model has complex guards that make some states hard to reach.

Lessons from ECinema¶

Use enum states for page/screen-based systems — each page is a natural state
Combine enum state with key context (like current user) in getState() to distinguish behaviourally different situations
Create separate actions for each input combination you want coverage to track
Use shared guard/action methods to keep the code DRY
Tag requirements in comments so you can trace coverage back to specifications

Source: modeljunit-samples/.../ecinema/ECinema.java

9. Summary — The MBT Workflow¶

@startuml
title The Model-Based Testing Workflow

|Design|
start
:Identify the system's key states;
:Decide on state granularity\n(abstract enough to be tractable);
:List the actions (transitions);
:Add guards for conditional transitions;

|Implement|
:Write FsmModel class;
:Implement getState(), reset(), @Action methods;
:Add guard methods;

|Test the Model|
:Run GreedyTester with coverage metrics;
:Check state coverage = 100%;
:Check transition coverage = 100%;
if (Coverage < 100%?) then (yes)
  :Fix guards or add missing transitions;
  :back to Run;
else (no)
endif

|Connect to SUT|
:Write adaptor (extend model or wrap it);
:Override @Action methods to call SUT;
:Add assertions in checkSUT();

|Run in CI|
:Embed in JUnit 5 @Test method;
:Assert coverage thresholds;
:Run with mvn test;
stop
@enduml

Design — identify states, actions, and guards. Keep states abstract.
Implement — write the FsmModel class with getState(), reset(), and @Action methods.
Test the model — run a GreedyTester and check coverage. Fix the model until coverage is 100%.
Connect to SUT — write an adaptor that calls real code and asserts postconditions.
Run in CI — embed in JUnit 5 tests with coverage assertions.

Next Steps¶

See the Examples Catalogue for an annotated guide to every example model in this project
See the Further Reading for external resources that go deeper
See the JavaFX GUI guide for interactive model exploration
See the ParamEdit guide for combinatorial test data generation