Procedure: attempt, admissible transition, reached state

For LLMs9 sections

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.

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.

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.

$ 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:

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.

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.

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:

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:

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:

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:

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.

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/.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.