# Exercise 20. Withdrawing an application

An exercise for the [procedure](/tutorials/procedure/) page. The page's
accreditation procedure knows two ends: accreditation and refusal. An
applicant may withdraw a filed application, a third end.

**Setup.** Add a "withdrawn" terminal state and a transition into it from
the "filed" state upon a withdrawal statement. A filed and withdrawn
application yields `TRUE_ONLY` on the question "is the 'withdrawn' state
reached"; a withdrawal attempt without a statement yields `NEITHER`; withdrawing
a draft nobody filed is `NEITHER` too.

**Hint.** A transition has one source state. Withdrawal from "under
review" is a separate transition, absent here on purpose: the archive
rules speak of withdrawing a filed application and stay silent about one
under review.

Below is the solution. Try it yourself first.

## Solution

```law
language "law.core" version "0.2";
package tutorial.archive version "0.12.1";
namespace "urn:law:tutorial:archive";

entity Person;
entity Application;

relation application_of(app: Application, p: Person) kind empirical;
relation application_complete(app: Application) kind empirical;
relation applicant_withdrew(app: Application) kind empirical;
relation committee_approved(app: Application) kind empirical;
relation committee_refused(app: Application) kind empirical;
relation accredited(p: Person) kind institutional;
```

The procedure with a sixth state and a fifth transition:

```law
procedure Accreditation(app: Application) {
    state Draft initial;
    state Submitted;
    state UnderReview;
    state Accredited terminal;
    state Refused terminal;
    state Withdrawn terminal;

    transition Submit {
        from Draft;
        to Submitted;
        when application_complete(app);
    }
    transition Review {
        from Submitted;
        to UnderReview;
    }
    transition Withdraw {
        from Submitted;
        to Withdrawn;
        when applicant_withdrew(app);
    }
    transition Grant {
        from UnderReview;
        to Accredited;
        when committee_approved(app);
    }
    transition Refuse {
        from UnderReview;
        to Refused;
        when committee_refused(app);
    }
}

rule AccreditationGranted strict {
    for app: Application;
    for p: Person;
    when application_of(app, p) and current_state(app, Accredited);
    then accredited(p);
}
```

The first test is filing and withdrawal:

```law
test "отзыв поданной заявки — заявка отозвана" {
    given {
        context {
            decision_time @2026-04-15T09:00:00+05:00;
            knowledge_time @2026-04-15T09:00:00+05:00;
            legal_time @2026-04-15;
            timezone "Asia/Almaty";
        }
        assert procedure_instance(entity_ref("urn:tutorial:application1")) {
            id "assert-instance";
            origin case_input;
        }
        assert application_complete(entity_ref("urn:tutorial:application1")) {
            id "assert-complete";
            origin case_input;
        }
        assert attempted_transition(entity_ref("urn:tutorial:application1"), Submit,
                                    AccreditationStep { id: "urn:tutorial:application1#submit",
                                                        time: @2026-04-13T10:00:00+05:00 }) {
            id "assert-attempt-submit";
            origin case_input;
        }
        assert applicant_withdrew(entity_ref("urn:tutorial:application1")) {
            id "assert-withdrew";
            origin case_input;
        }
        assert attempted_transition(entity_ref("urn:tutorial:application1"), Withdraw,
                                    AccreditationStep { id: "urn:tutorial:application1#withdraw",
                                                        time: @2026-04-14T10:00:00+05:00 }) {
            id "assert-attempt-withdraw";
            origin case_input;
        }
    }
    evaluate truth(current_state(entity_ref("urn:tutorial:application1"), Withdrawn));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}
```

The test name reads: "Withdrawing a filed application — the application is withdrawn."

## Check

Three tests in `tests/50-exercise-procedure.lawtest`: withdrawing a filed
application, a withdrawal attempt without a statement, withdrawing
a draft. The third test shows how the procedure answers an attempt from
the wrong state: not with an error but with silence — the attempt exists,
no admissible transition does.

Worth knowing about the procedures profile here. States derive from
attempts and guards, a derivation rather than a history: two attempts
from one state over two different transitions yield two reached states.
The profile does not read the attempts' time order, and "withdraw after
review" is inexpressible here except as a separate transition from "under
review".

What the exercise teaches. A terminal state claims no transitions lead
further, and the compiler holds it: a transition from a terminal state is
a check-time refusal. A procedure's new end is a state plus transitions
into it, each from its own source state with its own guard from the text.