Getting Started with ModelJUnit¶

Looking for a full tutorial? See the Model-Based Testing Tutorial for a comprehensive, concept-driven guide with PlantUML diagrams and worked examples.

What is Model-Based Testing?¶

Model-Based Testing (MBT) is an approach where you write a behavioural model of your system under test (SUT) as a finite-state machine (FSM), and then automatically generate and execute test cases by traversing that model's state space.

Instead of writing individual test cases by hand, you describe what the system does in each state, and ModelJUnit explores the model to produce comprehensive test sequences — measuring coverage as it goes.

Benefits: - Tests stay in sync with the model; change the model → tests change automatically - Coverage metrics (state, transition, transition-pair) reveal gaps in test suites - Works with any Java SUT without special instrumentation

Adding ModelJUnit as a Maven Dependency¶

<dependency>
  <groupId>nz.ac.waikato.modeljunit</groupId>
  <artifactId>modeljunit-core</artifactId>
  <version>3.0.0-SNAPSHOT</version>
</dependency>

For test scope only:

<dependency>
  <groupId>nz.ac.waikato.modeljunit</groupId>
  <artifactId>modeljunit-core</artifactId>
  <version>3.0.0-SNAPSHOT</version>
  <scope>test</scope>
</dependency>

Writing Your First FSM Model¶

Every model implements FsmModel (or its convenience subclass AbstractFsmModel) and uses @Action-annotated methods for transitions.

The canonical example — `SimpleSet`¶

The following model (SimpleSet) tracks a set with two boolean members s1 and s2:

package nz.ac.waikato.modeljunit.examples;

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

/** A model of a set with two elements: s1 and s2. */
public class SimpleSet implements FsmModel {

    protected boolean s1, s2;

    /** Returns the current state — ModelJUnit uses equals() to identify states. */
    @Override
    public Object getState() {
        return (s1 ? "T" : "F") + (s2 ? "T" : "F");
    }

    /** Resets the model to its initial state. */
    @Override
    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; }
}

Key contracts: - getState() must return an object whose equals() distinguishes states. - reset(boolean testing) must return the model to its initial state. - Each @Action method represents one FSM transition. - Optional guard methods <actionName>Guard() returning boolean can enable/disable transitions conditionally.

Adding guards¶

private int count = 0;

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

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

Connecting to a real SUT¶

import java.util.HashSet;

public class SimpleSetWithAdaptor extends SimpleSet {
    private final HashSet<String> sut = new HashSet<>();

    @Override
    @Action
    public void addS1() {
        super.addS1();
        sut.add("s1");
        assert sut.contains("s1") : "addS1 postcondition failed";
    }

    // ... override other actions similarly
}

Running Tests¶

Using `RandomTester`¶

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

Tester tester = new RandomTester(new SimpleSet());
tester.addListener(new VerboseListener());                  // prints every step
tester.addCoverageMetric(new TransitionCoverage());         // measure transition coverage
tester.generate(200);                                        // run 200 steps
tester.printCoverage();

Using `AllTransitionCoverage`¶

AllTransitionCoverage drives the traversal to ensure every transition is fired at least once:

Tester tester = new GreedyTester(new SimpleSet());
tester.addCoverageMetric(new TransitionCoverage());
tester.generate(200);
// coverage is printed via printCoverage() or by inspecting the metric

Using `AllStateCoverage`¶

Tester tester = new GreedyTester(new SimpleSet());
tester.addCoverageMetric(new StateCoverage());
tester.generate(200);
tester.printCoverage();

Building the graph without running tests¶

Tester tester = new GreedyTester(new SimpleSet());
tester.buildGraph();   // exhaustively explores all reachable states
tester.printCoverage();

Running with JUnit 5¶

Embed model-based tests inside a standard JUnit 5 test class:

import nz.ac.waikato.modeljunit.*;
import nz.ac.waikato.modeljunit.coverage.*;
import org.junit.jupiter.api.Test;
import static org.junit.jupiter.api.Assertions.*;

class SimpleSetMBTTest {

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

    @Test
    void graphIsConnected() {
        Tester tester = new GreedyTester(new SimpleSet());
        tester.buildGraph();
        // All 4 states (FF, FT, TF, TT) must be reachable
        assertTrue(tester.getGraph().vertexSet().size() >= 4);
    }
}

Run with Maven: mvn test

Reading Test Output / Coverage Reports¶

Console output (VerboseListener)¶

reset
addS1  [FF->TF]
addS2  [TF->TT]
removeS1  [TT->FT]
...
TransitionCoverage: 8/8 (100%)
StateCoverage: 4/4 (100%)

JUnit Surefire XML reports¶

After mvn test, reports appear in target/surefire-reports/TEST-*.xml. CI pipelines pick these up automatically.

JaCoCo coverage¶

After mvn verify, HTML and XML reports are at target/site/jacoco/. Open target/site/jacoco/index.html in a browser.

Maven site¶

mvn site

Opens a full project site with Javadoc, Surefire, JaCoCo, and SpotBugs reports linked together under target/site/index.html.

Available Tester Implementations¶

Class	Strategy
`RandomTester`	Uniform random walk
`GreedyTester`	Random walk, prefers least-visited transitions
`LookaheadTester`	Greedy with configurable lookahead depth
`QuickTester`	Shortest-path traversal

Next Steps¶

See the JavaFX GUI guide for interactive model exploration with screenshots of every panel.
See the ParamEdit guide for combinatorial test data generation.

GUI Quick Look¶

If you prefer a visual tool over the programmatic API, the JavaFX application lets you load models, configure testers, and watch coverage build in real time:

Test Design panel

Coverage chart

See the full JavaFX GUI guide for details.