		Search-engine friendly clone of the ACL2 documentation.

Events

Event

Fixtype of events.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:create-certificate → event-create-certificate
:receive-certificate → event-receive-certificate
:store-certificate → event-store-certificate
:advance-round → event-advance-round
:commit-anchors → event-commit-anchors
:timer-expires → event-timer-expires

The system evolves its state (see system-state) in response to the following events:

A validator creates a new certificate. Note that the certificate includes the author, i.e. it indicates the validator. This adds the certificate to the DAG of the validator, and broadcasts the certificate to all the correct validators (the latter point is discussed in more detail later).
A validator receives a certificate, from a message in the network, which is removed from the network and added to the buffer of the validator.
A validator stores a certificate into the DAG, moving it there from the buffer.
A validator advances its round.
A validator commits anchors.
A validator's timer expires.

Each event can only happen in certain states, e.g. a validator can generate a new certificate only if it has a quorum of preceding certificates in the DAG. If an event is possible, then the next state is uniquely determined by the current state and the event.

Subtopics

Event-case: Case macro for the different kinds of event structures.
Event-fix: Fixing function for event structures.
Eventp: Recognizer for event structures.
Event-equiv: Basic equivalence relation for event structures.
Event-store-certificate
Event-timer-expires
Event-receive-certificate
Event-create-certificate
Event-commit-anchors
Event-advance-round
Event-kind: Get the kind (tag) of a event structure.