Formal model says: these states and transitions are allowed.
Implementation says: this code handles commands.
Model-based test asks: for generated command traces, do both behave the same?

state machine
workflow lifecycle
idempotency
retry behavior
cache consistency
order/payment lifecycle
case management
approval process
quota/counter
reservation system
saga/compensation

Model            -> representasi sederhana dari expected behavior
System Under Test -> implementasi Java nyata
Trace            -> urutan command/event yang dijalankan ke keduanya

100 commands -> 12 commands -> 4 commands -> minimal reproduction

lebih kecil
lebih abstrak
lebih deterministic
lebih lambat tidak masalah
lebih jelas daripada production code

repository
locking
transaction
outbox
event publishing
DTO mapping
validation layer
audit
metrics
framework annotations

Map<Id, State>
Set<ProcessedCommand>
List<Event>
small enum state
pure transition function

banyak state
banyak command
urutan command penting
edge case muncul dari kombinasi
manual examples cepat meledak
bug sering berupa illegal transition
idempotency/retry penting
concurrency/eventual consistency penting
formal model sudah ada

mapper trivial
simple CRUD tanpa lifecycle
pure one-shot calculation yang cukup property test biasa
controller glue
formatting sederhana

Jika correctness bergantung pada urutan kejadian, pertimbangkan model-based testing.

DRAFT -> SUBMITTED -> UNDER_REVIEW -> APPROVED -> CLOSED
DRAFT -> CANCELLED
SUBMITTED -> REJECTED
UNDER_REVIEW -> REJECTED

record CaseModel(CaseStatus status, long version) {
    CaseModel submit() {
        if (status != CaseStatus.DRAFT) return this;
        return new CaseModel(CaseStatus.SUBMITTED, version + 1);
    }

    CaseModel startReview() {
        if (status != CaseStatus.SUBMITTED) return this;
        return new CaseModel(CaseStatus.UNDER_REVIEW, version + 1);
    }

    CaseModel approve() {
        if (status != CaseStatus.UNDER_REVIEW) return this;
        return new CaseModel(CaseStatus.APPROVED, version + 1);
    }
}

CaseRecord sut = CaseRecord.draft();

sealed interface CaseCommand permits Submit, StartReview, Approve {
    CaseModel applyToModel(CaseModel model);
    void applyToSut(CaseRecord sut);
}

record Submit() implements CaseCommand {
    public CaseModel applyToModel(CaseModel model) { return model.submit(); }
    public void applyToSut(CaseRecord sut) { sut.submit(); }
}

@Property
void implementationFollowsModel(@ForAll("caseTraces") List<CaseCommand> commands) {
    CaseModel model = new CaseModel(CaseStatus.DRAFT, 0);
    CaseRecord sut = CaseRecord.draft();

    for (CaseCommand command : commands) {
        model = command.applyToModel(model);
        command.applyToSut(sut);

        assertThat(sut.status()).isEqualTo(model.status());
        assertThat(sut.version()).isEqualTo(model.version());
    }
}

CaseModel approve() {
    if (status != UNDER_REVIEW) return this;
    return new CaseModel(APPROVED, version + 1);
}

record TransitionOutcome(CaseModel model, ExpectedResult result) {}

record CaseModel(CaseStatus status, long version) {
    TransitionOutcome approve() {
        if (status != CaseStatus.UNDER_REVIEW) {
            return new TransitionOutcome(this, ExpectedResult.rejected("invalid state"));
        }
        return new TransitionOutcome(
            new CaseModel(CaseStatus.APPROVED, version + 1),
            ExpectedResult.accepted()
        );
    }
}

ExpectedResult actual = sut.approve(actor, now);
assertThat(actual.kind()).isEqualTo(expected.result().kind());

Model harus mencakup success dan rejection, bukan hanya happy path.

Arbitraries.of(new Submit(), new Approve(), new Close()).list()

mostly valid traces
invalid transition traces
duplicate command traces
retry traces
boundary traces
long random traces
known counterexample traces

@Provide
Arbitrary<List<CaseCommand>> caseTraces() {
    Arbitrary<CaseCommand> command = Arbitraries.oneOf(
        Arbitraries.just(new Submit()),
        Arbitraries.just(new StartReview()),
        Arbitraries.just(new Approve()),
        Arbitraries.just(new Reject()),
        Arbitraries.just(new Close()),
        Arbitraries.just(new Cancel())
    );

    return command.list().ofMinSize(0).ofMaxSize(50);
}

@Provide
Arbitrary<List<CaseCommand>> duplicateSensitiveTraces() {
    return Arbitraries.of(
        List.of(new Submit(), new Submit()),
        List.of(new Submit(), new StartReview(), new StartReview()),
        List.of(new Submit(), new StartReview(), new Approve(), new Approve())
    );
}

internal list order jika domain tidak peduli order
private cache size jika tidak observable
repository call count jika bukan contract
exact exception class jika boundary contract memakai domain result

Apa yang user/system lain boleh andalkan?

1. WorkerA reads command C as NEW
2. WorkerB reads command C as NEW
3. WorkerA writes APPROVED
4. WorkerB writes APPROVED again
5. Two outbox events exist

@Test
void duplicateWorkersMustNotPublishTwoApprovedEvents() throws Exception {
    CommandId commandId = CommandId.random();
    CaseId caseId = createSubmittedCase();

    CountDownLatch bothRead = new CountDownLatch(2);
    CountDownLatch allowWrite = new CountDownLatch(1);

    processor.installHook(new ProcessorHook() {
        @Override
        public void afterRead(Command command) {
            if (command.id().equals(commandId)) {
                bothRead.countDown();
                await(allowWrite);
            }
        }
    });

    Future<?> a = executor.submit(() -> processor.process(commandId));
    Future<?> b = executor.submit(() -> processor.process(commandId));

    assertThat(bothRead.await(5, TimeUnit.SECONDS)).isTrue();
    allowWrite.countDown();

    a.get();
    b.get();

    assertThat(outbox.findByCaseId(caseId, EventType.CASE_APPROVED)).hasSize(1);
}

Every formal counterexample that represents a real bug should become an executable regression test.

Case C is CLOSED
Task T belongs to C
Task T is OPEN

@Test
void closedCaseCannotHaveOpenTasks() {
    CaseRecord c = CaseRecord.closed();
    Task t = Task.openFor(c.id());

    assertThatThrownBy(() -> invariantChecker.validate(c, List.of(t)))
        .isInstanceOf(InvariantViolation.class)
        .hasMessageContaining("closed case cannot have open task");
}

@Property
void closedCasesRejectOpenTasks(@ForAll CaseId caseId,
                                @ForAll("openTasks") List<Task> tasks) {
    CaseRecord c = CaseRecord.closed(caseId);

    assertThat(invariantChecker.validate(c, tasks))
        .isEqualTo(ValidationResult.invalid("closed case cannot have open task"));
}

//@ requires amount >= 0;
//@ requires basisPoints >= 0 && basisPoints <= 10000;
//@ ensures 0 <= 
esult && 
esult <= amount;

@Property
void percentageResultIsWithinInput(@ForAll @LongRange(min = 0, max = 1_000_000_000L) long amount,
                                   @ForAll @IntRange(min = 0, max = 10_000) int basisPoints) {
    Percentage p = new Percentage(basisPoints);

    long result = p.applyTo(amount);

    assertThat(result).isBetween(0L, amount);
}

@Property
void approveDoesNotChangeOwner(@ForAll("underReviewCases") CaseRecord c,
                               @ForAll("reviewers") UserId reviewer) {
    UserId ownerBefore = c.owner();

    c.approve(reviewer, fixedNow);

    assertThat(c.owner()).isEqualTo(ownerBefore);
}

@Property
void caseAggregateMaintainsInvariants(@ForAll("caseCommandTraces") List<CaseCommand> commands) {
    CaseRecord sut = CaseRecord.draft();
    CaseModel model = CaseModel.draft();

    for (CaseCommand command : commands) {
        ExpectedStep expected = model.step(command);
        ActualStep actual = command.applyTo(sut);

        assertStep(expected, actual);
        assertInvariants(sut);

        model = expected.nextModel();
    }
}

private void assertInvariants(CaseRecord c) {
    assertThat(c.status()).isNotNull();
    assertThat(c.version()).isGreaterThanOrEqualTo(0);

    if (c.status() == CaseStatus.APPROVED) {
        assertThat(c.approvedBy()).isPresent();
        assertThat(c.approvedAt()).isPresent();
    }

    if (c.status().isTerminal()) {
        assertThat(c.hasOpenInternalTransition()).isFalse();
    }
}

same key + same command hash after success returns same result
same key + different command hash is conflict
failed validation does not complete key
technical failure may leave key pending
completed key cannot be overwritten
side effect occurs at most once

record IdempotencyModel(Map<Key, RecordState> records,
                        int sideEffectCount) {

    StepResult handle(Key key, CommandHash hash, CommandValidity validity) {
        RecordState existing = records.get(key);

        if (existing instanceof Completed c) {
            if (!c.commandHash().equals(hash)) {
                return StepResult.conflict(this);
            }
            return StepResult.replayed(this, c.result());
        }

        if (!validity.valid()) {
            return StepResult.rejected(this);
        }

        ResultHash result = ResultHash.of(key, hash);
        Map<Key, RecordState> next = new HashMap<>(records);
        next.put(key, new Completed(hash, result));

        return StepResult.accepted(new IdempotencyModel(next, sideEffectCount + 1), result);
    }
}

@Property
void idempotencyImplementationFollowsModel(@ForAll("idempotencyCommands") List<IdempotencyCommand> commands) {
    IdempotencyModel model = IdempotencyModel.empty();
    IdempotencyService sut = newInMemoryService();

    for (IdempotencyCommand command : commands) {
        StepResult expected = model.handle(command.key(), command.hash(), command.validity());
        ActualResult actual = sut.handle(command.toRequest());

        assertEquivalent(expected, actual);
        assertThat(sut.sideEffectCount()).isEqualTo(expected.nextModel().sideEffectCount());

        model = expected.nextModel();
    }
}

invalid command stores completed key
conflict overwrites old result
retry executes side effect again
same key with different payload returns stale success

record WorkflowModel(CaseStatus caseStatus,
                     Set<Task> openTasks,
                     Set<EventType> emittedEvents) {

    WorkflowModel submit() {
        if (caseStatus != DRAFT) return this;
        return new WorkflowModel(
            SUBMITTED,
            Set.of(Task.review()),
            plus(emittedEvents, CASE_SUBMITTED)
        );
    }

    WorkflowModel approve() {
        if (caseStatus != UNDER_REVIEW) return this;
        return new WorkflowModel(
            APPROVED,
            closeReviewTasks(openTasks),
            plus(emittedEvents, CASE_APPROVED)
        );
    }

    boolean invariantHolds() {
        return !(caseStatus.isTerminal() && hasOpenBlockingTask());
    }
}

case table
task table
outbox table
audit table
workflow engine API

WorkflowProjection actual = projectionReader.read(caseId);
assertThat(actual.caseStatus()).isEqualTo(model.caseStatus());
assertThat(actual.openTaskTypes()).isEqualTo(model.openTaskTypes());
assertThat(actual.emittedEventTypes()).containsAll(model.emittedEvents());

fast
pure JVM
good for aggregate/domain service
runs often

Postgres/Testcontainers
Kafka/Testcontainers
real transaction/repository
slower
catches mapping/locking/serialization bug

Run model-based unit properties on every PR.
Run smaller model-based integration traces on CI verify/nightly.
Run known counterexample traces always.

case lifecycle model, max trace 50, in-memory -> PR
case lifecycle model, max trace 15, Postgres -> PR verify
case lifecycle model, max trace 100, Postgres+Kafka -> nightly

random seed
shrunk command trace
initial state
clock instants
generated IDs
thread schedule hints if any
SUT version/build hash

{
  "seed": "774219331",
  "initial": { "status": "DRAFT", "version": 0 },
  "commands": [
    { "type": "SUBMIT" },
    { "type": "START_REVIEW" },
    { "type": "APPROVE", "actor": "assignee" }
  ],
  "expected": { "result": "REJECTED", "status": "UNDER_REVIEW" },
  "actual": { "result": "ACCEPTED", "status": "APPROVED" }
}

@Test
void assigneeCannotApproveOwnCase_counterexample774219331() {
    replay(List.of(
        new Submit(),
        new StartReview(),
        new Approve(ASSIGNEE)
    ));
}

review model like production code
trace model rules back to requirements/spec
compare with TLA+/Alloy/JML where available
seed model with known historical bugs
write example tests for model itself
keep model small enough to inspect

state coverage
transition coverage
invalid transition coverage
pairwise transition coverage
terminal state coverage
retry/duplicate coverage
boundary value coverage
exception path coverage
cross-entity invariant coverage

Statistics.label("final-state")
    .collect(model.status().name());

Statistics.label("trace-length")
    .collect(bucket(commands.size()));

Statistics.label("contains-duplicate")
    .collect(hasDuplicate(commands));

Normal journey: submit -> review -> approve -> close
Invalid early command: approve before review
Duplicate command: submit twice, approve twice
Conflict: assignee approves own case
Retry: same command ID repeated
Compensation: approve then rollback/void if allowed
Timeout: deadline expires before action

@Provide
Arbitrary<List<CaseCommand>> caseCommandTraces() {
    return Arbitraries.oneOf(
        validJourneys(),
        invalidTransitionJourneys(),
        duplicateJourneys(),
        conflictOfInterestJourneys(),
        timeoutJourneys(),
        randomLongJourneys()
    );
}

@Property(tries = 1_000)
void propertyName(@ForAll("traces") List<Command> trace) {
    Model model = Model.initial();
    Sut sut = newSut();

    for (Command command : trace) {
        Expected expected = model.next(command);
        Actual actual = sut.execute(command);

        assertEquivalent(expected, actual);
        assertGlobalInvariants(sut);

        model = expected.model();
    }
}

model update must be explicit
assert after every step, not only at end
global invariants checked repeatedly
command result compared, not only final state
trace reproducible

record Model(State state, List<EventType> events) {}

List<EventType> actualEvents = outbox.findTypesByAggregateId(caseId);
assertThat(actualEvents).containsExactlyElementsOf(model.events());

containsExactlyElementsOf

containsExactlyInAnyOrderElementsOf

successful mutation increments version
rejected business command does not increment version
technical failure does not commit version
stale write is rejected

long versionBefore = sut.version();
ActualResult actual = sut.execute(command);

if (actual.accepted()) {
    assertThat(sut.version()).isEqualTo(versionBefore + 1);
} else {
    assertThat(sut.version()).isEqualTo(versionBefore);
}

@Test
void staleVersionCannotOverwriteNewerState() {
    CaseRecord a = repository.get(id);
    CaseRecord b = repository.get(id);

    a.submit();
    repository.save(a);

    b.cancel();

    assertThatThrownBy(() -> repository.save(b))
        .isInstanceOf(OptimisticLockingFailure.class);
}

After command accepted, projection eventually reflects event.

ActualResult result = api.submitCase(request);
assertThat(result.accepted()).isTrue();

await().atMost(Duration.ofSeconds(5)).untilAsserted(() -> {
    CaseProjection p = projectionApi.get(result.caseId());
    assertThat(p.status()).isEqualTo(CaseStatus.SUBMITTED);
});

strongly consistent state
asynchronously derived projection
event log
external notification

TLA+/PlusCal for interleaving model
jcstress for low-level concurrency primitives
controlled integration tests for known races
model-based sequential tests for lifecycle behavior
production telemetry for duplicate/violation detection

fast evidence
expensive evidence
historical bug regression
exploratory generation

case starts DRAFT
submit creates review task
reviewer can request information
request information pauses SLA
response resumes SLA
approval closes review task
closed case cannot have open blocking tasks
appeal can be opened only after closed with appealable decision

record EnforcementModel(
    CaseStatus status,
    boolean reviewTaskOpen,
    boolean infoRequested,
    boolean slaPaused,
    boolean appealOpen,
    long version
) {
    EnforcementModel submit() { ... }
    EnforcementModel requestInfo() { ... }
    EnforcementModel receiveInfo() { ... }
    EnforcementModel approve() { ... }
    EnforcementModel close() { ... }
    EnforcementModel appeal() { ... }
}

boolean invariantHolds() {
    if (status == CLOSED && reviewTaskOpen) return false;
    if (infoRequested != slaPaused) return false;
    if (appealOpen && status != CLOSED) return false;
    return version >= 0;
}

@Property
void enforcementLifecycleFollowsModel(@ForAll("enforcementTraces") List<EnforcementCommand> trace) {
    EnforcementModel model = EnforcementModel.initial();
    EnforcementCase sut = fixture.newDraftCase();

    for (EnforcementCommand command : trace) {
        Step expected = model.step(command);
        Step actual = command.execute(sut);

        assertEquivalent(expected, actual);
        assertProductionInvariants(sut);

        model = expected.model();
    }
}

lifecycle rule -> model transition
legal/business invariant -> invariant assertion
historical defect -> fixed trace
unexpected generated failure -> regression test

Cmd1
Cmd2
DoThing
ChangeState

SubmitCase
AssignReviewer
RequestInformation
ReceiveInformation
ApproveCase
CloseCase
OpenAppeal

assertThat(x).isEqualTo(y);

assertThat(actual.status())
    .as("case status after %s", command)
    .isEqualTo(expected.status());

invalid transition accidentally accepted
rejected command increments version
duplicate command emits duplicate event
terminal state still allows mutation
side effect occurs before validation
retry changes result
case closed with open task
appeal allowed before final decision
stale update overwrites newer state
projection assumes event ordering that broker does not guarantee

seed
shrunk trace
command list
expected vs actual state
last successful step
SUT logs by correlation ID
outbox events
DB rows snapshot if relevant

./mvnw -Dtest=EnforcementModelPropertyTest   -Djqwik.seed=774219331   -Dtrace.file=target/failing-traces/774219331.json test

[ ] Domain has stateful behavior worth modeling.
[ ] Model is smaller than implementation.
[ ] Commands are named in business language.
[ ] Generator covers valid and invalid traces.
[ ] Oracle checks result and state.
[ ] Invariants are asserted after every step.
[ ] Side effects are modeled at semantic level.
[ ] Failing trace is reproducible.
[ ] Counterexamples become fixed regression tests.
[ ] Slow model tests are separated from fast PR suite.

state machine diagram
TLA+ counterexample
Alloy invalid structure
JML contract
business lifecycle rule

executable generated tests
shrunk failing traces
regression artifacts
CI evidence
living documentation

A model defines the expected world.
A trace explores behavior.
The SUT must follow the model.
Every counterexample becomes a test.