Vortex.Journal.Net

An operation of the DSL together with the answer it got: one entry of the free-monad trace with its result. The journal records these, so a replay reads the answer instead of asking again.

One step of a command: an operation the journal answers itself from the state, or an operation whose answer is already known because the world gave it (an outcome a reactor or an executor reports).

What a block submits: its calls, decided together or not at all.

The net a shell supplies for its operation type: the initial marking, each answered operation's consumed and produced tokens, the oracle for the operations the journal answers itself, and which operations are intents and outcomes of effects on the world, with the intent tokens told apart.

How the journal answers an operation it answers itself: a function of the state alone, so deciding is deterministic. Nothing when the state gives no answer, and the command is refused.

What an answered operation means for the world outside the journal. An effect on the world is two operations: an Intends that records the intent as a token, and later a Settles that consumes it with the outcome the world answered.

The tokens an operation consumes.

The tokens an operation produces.

An operation is enabled where the marking holds what it consumes.

The tokens an operation lacks to be enabled.

Fire an operation: consume its pre and produce its post. Total, with the difference truncated at zero; it means a step of the net only where the operation is enabled, and the journal only ever records such steps.

Every token an operation consumes or produces.

Two operations are independent when they touch no token in common, so either order of firing them gives the same marking.

The intent token an outcome settles, or none for any other operation.

The intent token an intent operation announces, or none.

The intent tokens of a marking.