mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
64 lines
2.2 KiB
INI
64 lines
2.2 KiB
INI
\* Wave.cfg -- TLC / Apalache model checking configuration
|
|
\*
|
|
\* Run with TLC:
|
|
\* java -jar tla2tools.jar -config Wave.cfg MC_Wave
|
|
\*
|
|
\* Run with Apalache:
|
|
\* apalache-mc check --config=Wave.cfg MC_Wave.tla
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SPECIFICATION
|
|
\* --------------------------------------------------------------------------
|
|
|
|
SPECIFICATION Spec
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* CONSTANTS
|
|
\* --------------------------------------------------------------------------
|
|
|
|
CONSTANTS
|
|
N = MC_N
|
|
F = MC_F
|
|
K = MC_K
|
|
AlphaThreshold = MC_AlphaThreshold
|
|
Beta = MC_Beta
|
|
Values = MC_Values
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* STATE CONSTRAINT (bounds state space for tractable checking)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
CONSTRAINT StateConstraint
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* INVARIANTS (checked at every reachable state)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
INVARIANT MC_TypeOK
|
|
INVARIANT MC_Safety
|
|
INVARIANT MC_AgreementOnAccept
|
|
INVARIANT MC_ConfidenceBound
|
|
INVARIANT MC_DecisionConsistency
|
|
INVARIANT MC_PrefMatchesDecision
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* TEMPORAL PROPERTIES
|
|
\* --------------------------------------------------------------------------
|
|
|
|
\* Finalized decisions never change (action property)
|
|
PROPERTY MC_FinalizedStable
|
|
|
|
\* Liveness: every honest validator eventually finalizes.
|
|
\* This will produce counterexamples under nondeterministic scheduling
|
|
\* because roundDir can alternate forever, preventing beta consecutive
|
|
\* same-direction rounds. This is expected -- Snow liveness is probabilistic.
|
|
\* Uncomment to verify the counterexample exists:
|
|
\*
|
|
\* PROPERTY MC_Liveness
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SYMMETRY (reduces state space when Values has 2+ elements)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
\* SYMMETRY MC_Symmetry
|