1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
; AleoBFT Library
;
; Copyright (C) 2024 Provable Inc.
;
; License: See the LICENSE file distributed with this library.
;
; Authors: Alessandro Coglio (www.alessandrocoglio.info)
; Eric McCarthy (bendyarm on GitHub)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ALEOBFT-STAKE2")
(include-book "states")
(include-book "events")
(include-book "initialization")
(include-book "transitions")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defxdoc+ definition
:parents (aleobft-stake2)
:short "Definition of the AleoBFT labeled state transition system."
:long
(xdoc::topstring
(xdoc::p
"We model the protocol as a labeled state transition system,
according to the standard definition of that notion in the literature.
We define the possible states of the system,
the possible events of the system,
the possible initial states,
and the possible transitions by which
an event takes a state to a new state
(the events `label' the transitions between states)."))
:order-subtopics (states
events
initialization
transitions))
|
