# Procedure: attempt, admissible transition, reached state

Accreditation from the first tutorials was a fact: an entry exists, the
researcher is admitted. But between the application and the entry lies
the case's course: the request composed, filed, examined, decided. Each
step has its conditions, and "filed" does not mean "the filing took
place". For this the core has the procedures profile
`law.procedure/0.1`. The corpus holds 98 procedures in 69
packages and 468 transitions (measured 05.09.2026 over `.law` text); the
complaint-examination procedure `ProizvodstvoPoZhalobe` in the
`complaints-106` package has seven states and six transitions.

This page's legal frame: an attempted procedural action is
a fact of the world and remains one even when no legal effect arose. The
profile tells three things apart, deriving none from another: the
attempt, the transition's admissibility, and the reached state.

An attempt carries a THIRD argument — the
carrier: the very event by which the attempt was undertaken. It carries
the `id` and the `time`, and time gives history its order: the
history fold reads one instance's attempts in ascending time, not in the
case's line order.

```law
language "law.core" version "0.2";
package tutorial.archive version "0.12.0";
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 committee_approved(app: Application) kind empirical;
relation committee_refused(app: Application) kind empirical;
relation accredited(p: Person) kind institutional;
```

## The automaton

An accreditation application passes four steps. Only a complete
application may be filed; examination starts on handover to the
committee; the committee either accredits or refuses, both outcomes
final.

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

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

The procedure parameter is the instance undergoing it: the single
variable visible to all transitions' guards. Exactly one state is
`initial`; `terminal` states have no outgoing transitions. A transition
requires `from` and `to`; the `when` guard is an ordinary formula over
the instance, and `Review` has none: there an attempt from the right
state suffices.

## What this lowers into

The automaton is DATA, not a set of rules: the compiler produces
a `procedure` node, state and transition declaration-constants
under qualified `<P>/<Name>` names, the `AccreditationStep` carrier type
(this procedure's transitions do not name `on`), and the profile
predicate declarations.

```text
$ lawc expand 20-procedure.law.md --symbol Accreditation
procedure Accreditation (20-procedure.law.md:…)
  procedure    …#Accreditation
  type_decl    …#AccreditationStep
  symbol_decl  …#Accreditation/Draft … …#Accreditation/Refuse
  symbol_decl  …#procedure_instance … …#current_state
```

The command names the page file; on this page run it with the `.en.law.md` filename.

| Relation | Arity | Kind | Who establishes |
|---|---|---|---|
| `procedure_instance(app)` | 1 | empirical | case: the application exists |
| `attempted_transition(app, Submit, e)` | 3 | empirical | case: the attempt undertaken by event `e` |
| `valid_transition(app, Submit, e)` | 3 | institutional | history fold: attempt, source state, guard |
| `initial_state(app, Draft)` | 2 | institutional | fold: the stage declared initial |
| `entered_state(app, Submitted, e)` | 3 | institutional | fold: entered the stage BY exactly this event |
| `left_state(app, Draft, e)` | 3 | institutional | fold: the stage left by this event |
| `current_state(app, Submitted)` | 2 | institutional | fold: the case stands here NOW |

The former two-argument `entered_state` answered four questions at once —
"initial", "entered by this event", "standing now", "left" — and the
author could not separate them. Now each has its own predicate, and the
choice between them is a norm's choice: "while the application is in
draft" is `current_state`, while "the application was ever filed" is
`entered_state` with that attempt's carrier.

Two empirical inputs and institutional conclusions — that is the procedure frame. No one
derives an attempt: the case feeds it together with its carrier, like any
observed fact. No one feeds a state: the fold of history derives it —
attempts ordered by carrier time.

## Attempt and effect

The same filing attempt with a complete and an incomplete application.

| Facts beyond the instance | `entered_state(Submitted, e)` | `attempted_transition(Submit, e)` | `valid_transition(Submit, e)` |
|---|---|---|---|
| filing attempt, application complete | `TRUE_ONLY` | `TRUE_ONLY` | `TRUE_ONLY` |
| filing attempt, application incomplete | `NEITHER` | `TRUE_ONLY` | `NEITHER` |
| application complete, no attempt | `NEITHER` | `NEITHER` | `NEITHER` |

The first row is the test from this page, byte for byte:

```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-14T10:00:00+05:00 }) {
            id "assert-attempt-submit";
            origin case_input;
        }
    }
    evaluate truth(current_state(entity_ref("urn:tutorial:application1"), Submitted));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}
```

The test name reads: "A filing attempt with a complete application — the filing took place."

The `AccreditationStep` carrier is synthetic: this procedure's transitions
do not name `on`, and the profile gives them a step type by procedure name.
Both its fields are mandatory: without the `id` an event has no
identity, without the `time` no place in history, and the compiler
refuses `LDC-E1343`. The carrier time is 14 April. The history fold reads
ALL of the instance's attempts and orders them only relative to each
other: the case's `decision_time` and `legal_time` do not cut carrier
time off (one law for the whole history), and the case's record
order does not affect history — `time` gives the order.

The second row is the point of the page. Ivanova brought an incomplete
application and tried to file it. The attempt exists —
`attempted_transition` is established by the case and stays `TRUE_ONLY`.
There is no effect: no transition happened, no state reached. The answer
to "did the filing take place" is `NEITHER`, not `FALSE_ONLY`: the
profile does not claim the filing did not take place; it merely finds no
grounds to count it as having taken place. The third row is symmetric: a
complete application nobody filed does not become filed — a guard
without an attempt starts nothing.

## Where state comes from

| Facts | question | answer |
|---|---|---|
| instance declared | `initial_state(Draft)` | `TRUE_ONLY` |
| no instance declared, application complete, filing attempt | `current_state(Submitted)` | `NEITHER` |
| instance, committee approval, decision attempt without filing and review | `current_state(Accredited)` | `NEITHER` |
| instance, complete application, approval, filing, review, and decision attempts | `current_state(Accredited)` | `TRUE_ONLY` |
| the same full chain | `current_state(Draft)` | `NEITHER` |
| the same full chain | `entered_state(Draft, e)` | `NEITHER`: nothing entered `Draft` |
| the same full chain | `left_state(Draft, e_submit)` | `TRUE_ONLY` |

The initial state is "reached" by nothing: it is declared, and
`initial_state` reads the declaration at the instance. Without an
instance there is no initial state and hence no transition: second row.
The third is a jump attempt: the committee approved, a decision attempt
was undertaken, but the `UnderReview` source state was not reached, and
there is no transition. Step order is held by the source state's
reachedness AT the carrier's moment.

The last three rows are what the separated predicates are for. Before,
`entered_state` meant "ever entered", and after
accreditation `Draft` stayed "reached": returning to a state was
indistinguishable from never leaving it, while the "while the application
is in draft" norm had to be written through a case fact or `not_known`
over a later state. Now such a norm is written directly —
`current_state(app, Draft)` — and "ever entered" is asked with
`entered_state` carrying that very attempt. The initial stage was
"entered" by nothing: it has no carrier, and its question is
`initial_state`.

## A norm reads the reached state

A researcher's accreditation is an ordinary institutional fact, derived
by an ordinary norm from the reached state and the application-to-person
link.

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

| Facts | `accredited(Ivanova)` |
|---|---|
| Ivanova's application, full chain to decision | `TRUE_ONLY` |

So a procedure links to the rest of the package: its conclusions are
literals, norms read them, and the same norms may carry duties with terms
for each step, as in [the deadlines tutorial](/tutorials/deadlines/).

## Two outcomes from one state

| Facts | `current_state` |
|---|---|
| chain to review, committee refusal, refusal attempt | `Refused`: `TRUE_ONLY` |
| chain to review, approval and refusal, decision attempt EARLIER than refusal attempt | `Accredited`: `TRUE_ONLY`, `Refused`: `NEITHER` |

The second row is what changed with the event model. Before, the profile
knew no mutual exclusion of transitions at all: a case asserting approval
and refusal and both attempts reached BOTH terminal states at once,
because no order existed between attempts. Now there is order — carrier
time — and the history fold reads attempts in ascending order: `Grant`
took place from `UnderReview`, the instance stands in `Accredited`, and
for `Refuse` the `from UnderReview` condition no longer holds. The refusal
attempt remains a fact of the world (`attempted_transition` is
`TRUE_ONLY`) but yields no legal effect, and the proof node names
the cause: `from`.

This does not replace mutual exclusion: swap the carrier times and
refusal takes place, not accreditation. A norm indifferent to the
presentation order is still written with guards (`not committee_refused`
in `Grant`'s guard) or a constraint — and that is the act's norm,
not the profile.

## What the profile does not promise

Two earlier boundaries were removed; a third remains and is honestly
named here.

**`on Event` is now a condition, not a declared intention.** Before,
the event name did not reach CLIR: two procedures differing only by event
produced byte-identical CLIR, and `check` stayed green with an `LDC-E1323`
warning. Now the name must resolve into an event or action
declaration — else a refusal, not a warning:

```text
error LDC-E1344: переход: имя `AccreditationRequested` в клаузе `on` не
разрешается в объявление события §79 либо действия §80 — носителя такого
типа не существует, и переход не состоялся бы ни при какой истории (§160.1)
```

The diagnostic reads: "transition: the name `AccreditationRequested` in the `on` clause resolves into neither an event nor an action declaration — no carrier of such a type exists, and the transition would not have taken place under any history".

A declared event becomes the carrier TYPE: a transition with `on E`
carries an `E` instance in its attempt; one without `on` a synthetic
`<P>Step`, like `AccreditationStep` on this page.

**An event journal and a current state exist.** The `law_process` and
`law_process_run` tools read the `procedure` node — no more
restoring the automaton from the shape of produced ids — and run the
case's attempt journal through an ordinary `evaluate`. An
`ATTEMPT_WITHOUT_EFFECT` find in their report is the regular subject of
attempted actions, not a defect of the statute.

**Terminality lives in the node.** The `terminal` marker stopped being
a source property: it is a state field in the `procedure` node, and to a
tool over CLIR a lawful terminal shows as a terminal, not as
`SINK_STATE` in notes. Left outside the page's slice are parallel
branches and `join`: they exist in the language but have not yet
received their own page.

## Compiler refusals

Exactly one initial state. Remove `initial` from `Draft` and the
procedure does not lower at all, followed down by the norm that read its
constant:

```text
error LDC-E1311: процедура "Accreditation": ровно одно состояние обязано
быть `initial` (§160), объявлено 0
```

The diagnostic reads: 'procedure "Accreditation": exactly one state must be `initial`, 0 declared'.

A transition from a terminal state is a record under which terminality
would be a comment. Point `Submit` from `Accredited`:

```text
error LDC-E1313: переход "Submit" выходит из терминального состояния
"Accredited" — терминальность иначе была бы комментарием (§160)
```

The diagnostic reads: 'transition "Submit" leaves the terminal state "Accredited" — otherwise terminality would be a comment'.

Both refusals belong to the language. A state missing
from the procedure, and a transition without `from` or `to`, are
`LDC-E1312`:

```text
error LDC-E1312: переход "Review": состояние "Committee" не объявлено в
процедуре (§160)
```

The diagnostic reads: 'transition "Review": state "Committee" is not declared in the procedure'.

And `LDC-E1344` is already a refusal, not a warning: a variant with
`on AccreditationRequested` must NOT compile. Before, this place held
an `LDC-E1323` warning with a zero exit code, and the compiler's silence
would have cost the author false confidence that the event counted.

## Next

The track's A2 step closes here: source, definitions, presumptions,
time, terms, positions, readings, evidence, and procedure. Next is the
package-in-corpus step: several packages in one world, shared
computation as a dependency, tables, answer investigation, and acceptance.
Its pages await the package practicum and are not yet written.

The exercise for this page is [/tutorials/exercise-procedure/](/tutorials/exercise-procedure/).