mirror of
https://github.com/tendermint/tendermint.git
synced 2026-02-10 14:00:33 +00:00
9ad6440bc0
* move from tendermint-rs but needs discussion * markdown lint * TODO links replaced * links * links * links lint * Update rust-spec/lightclient/supervisor/supervisor.md * Update rust-spec/lightclient/supervisor/supervisor.md * Update rust-spec/lightclient/supervisor/supervisor.md * Update rust-spec/lightclient/supervisor/supervisor.md * moved peer handling definitions to supervisor * polishing * rename * Update rust-spec/lightclient/supervisor/supervisor_001_draft.md * Update rust-spec/lightclient/supervisor/supervisor_001_draft.md * changes to maintain StateVerified again * ready for changes in verification * start of supervisor * module name * fixed * more details * supevisor completed. Now I have to add function to verification * ready for review * tla comment * removed issues * Update rust-spec/lightclient/supervisor/supervisor_001_draft.md * intro text fixed * indentation * Update rust-spec/lightclient/supervisor/supervisor_001_draft.md * comment to entry points Co-authored-by: Marko Baricevic <marbar3778@yahoo.com>
72 lines
1.7 KiB
Plaintext
72 lines
1.7 KiB
Plaintext
------------------------- MODULE supervisor_001_draft ------------------------
|
|
(*
|
|
This is the beginning of a spec that will eventually use verification and detector API
|
|
*)
|
|
|
|
EXTENDS Integers, FiniteSets
|
|
|
|
VARIABLES
|
|
state,
|
|
output
|
|
|
|
vars == <<state, output>>
|
|
|
|
CONSTANT
|
|
INITDATA
|
|
|
|
Init ==
|
|
/\ state = "Init"
|
|
/\ output = "none"
|
|
|
|
NextInit ==
|
|
/\ state = "Init"
|
|
/\ \/ state' = "EnterLoop"
|
|
\/ state' = "FailedToInitialize"
|
|
/\ UNCHANGED output
|
|
|
|
NextVerifyToTarget ==
|
|
/\ state = "EnterLoop"
|
|
/\ \/ state' = "EnterLoop" \* replace primary
|
|
\/ state' = "EnterDetect"
|
|
\/ state' = "ExhaustedPeersPrimary"
|
|
/\ UNCHANGED output
|
|
|
|
NextAttackDetector ==
|
|
/\ state = "EnterDetect"
|
|
/\ \/ state' = "NoEvidence"
|
|
\/ state' = "EvidenceFound"
|
|
\/ state' = "ExhaustedPeersSecondaries"
|
|
/\ UNCHANGED output
|
|
|
|
NextVerifyAndDetect ==
|
|
\/ NextVerifyToTarget
|
|
\/ NextAttackDetector
|
|
|
|
NextOutput ==
|
|
/\ state = "NoEvidence"
|
|
/\ state' = "EnterLoop"
|
|
/\ output' = "data" \* to generate a trace
|
|
|
|
NextTerminated ==
|
|
/\ \/ state = "FailedToInitialize"
|
|
\/ state = "ExhaustedPeersPrimary"
|
|
\/ state = "EvidenceFound"
|
|
\/ state = "ExhaustedPeersSecondaries"
|
|
/\ UNCHANGED vars
|
|
|
|
Next ==
|
|
\/ NextInit
|
|
\/ NextVerifyAndDetect
|
|
\/ NextOutput
|
|
\/ NextTerminated
|
|
|
|
InvEnoughPeers ==
|
|
/\ state /= "ExhaustedPeersPrimary"
|
|
/\ state /= "ExhaustedPeersSecondaries"
|
|
|
|
|
|
=============================================================================
|
|
\* Modification History
|
|
\* Last modified Sun Oct 18 11:48:45 CEST 2020 by widder
|
|
\* Created Sun Oct 18 11:18:53 CEST 2020 by widder
|