System-states
States of the system.
The system consists of a number of validators,
some correct and some faulty.
We model the correctness or faultiness of each validator,
and the internal state of each validator.
We also model the state of the network that connects the validators,
in terms of messages in transit,
which have been sent but not received yet.
Subtopics
- Correct-addresses
- Set of the addresses of all the correct validators in the system.
- Update-validator-state
- Update the state of a correct validator in the system.
- Update-network-state
- Update the state of the network in the system.
- Validators-state
- Fixtype of states of a collection of validators.
- System-state
- Fixtype of system states.
- System-state-option
- Fixtype of optional system states.
- Get-validator-state
- Retrieve the state of a validator from the system.
- Faulty-addresses
- Set of the addresses of all the faulty validator in the system.
- Number-validators
- Number of validators in the system.
- Number-faulty
- Number of faulty validators in the system.
- Get-network-state
- Retrieve the state of the network in the system.
- All-addresses
- Set of the addresses of all the validators in the system.
- Number-correct
- Number of correct validators in the system.
