Skip to content

examples-tests.md

Latest commit

 

History

History
124 lines (90 loc) · 5.52 KB

examples-tests.md

File metadata and controls

124 lines (90 loc) · 5.52 KB
Raw

This is a script for running choreo examples with quint.

This script requires txm to be installed:

npm install -g txm

NOTE: these tests only check that particular invocations succeed or fail. Tests marked as "should succeed" are expected to pass with the given invariants. Tests marked as "should fail" are expected to find counterexamples to the invariants.

All tests in the following cases are run as commands to bash.

Tendermint Examples

OK on tendermint valid module - run with invariants

cd examples/tendermint && quint run tendermint.qnt --main valid --invariant="agreement and validity and accountability" --max-samples=20

OK on tendermint valid module - test

cd examples/tendermint && quint test tendermint.qnt --main valid --max-samples=20

FAIL on tendermint no_agreement module - run with agreement (should find counterexample)

cd examples/tendermint && quint run tendermint.qnt --main no_agreement --invariant=agreement

OK on tendermint no_agreement module - run with accountability only

cd examples/tendermint && quint run tendermint.qnt --main no_agreement --invariant=accountability --max-samples=20

OK on tendermint no_agreement module - test

cd examples/tendermint && quint test tendermint.qnt --main no_agreement --max-samples=20

Alpenglow Examples

OK on alpenglow some_byz module - run with agreement

cd examples/alpenglow && quint run alpenglow.qnt --main some_byz --invariant agreement --max-samples 20

OK on alpenglow tests

cd examples/alpenglow && quint test alpenglow_tests.qnt

OK on alpenglow disagreement test

cd examples/alpenglow && quint test alpenglow.qnt --main too_many_byz

FAIL on alpenglow some_byz module - run with fastFinalizedWitness

cd examples/alpenglow && quint run alpenglow.qnt --main some_byz --invariant fastFinalizedWitness

FAIL on alpenglow some_byz_vp module - run with fastFinalizedWitness

cd examples/alpenglow && quint run alpenglow.qnt --main some_byz_vp --invariant fastFinalizedWitness

FAIL on alpenglow too_many_byz_1 module - run with agreement (should find counterexample)

cd examples/alpenglow && quint run alpenglow.qnt --main too_many_byz_1 --invariant agreement

FAIL on alpenglow too_many_byz module - run with agreement (should find counterexample)

cd examples/alpenglow && quint run alpenglow.qnt --main too_many_byz --invariant agreement

MonadBFT Examples

OK on monadbft instance - run with missing_tip_w

cd examples/monadbft && quint run instance.qnt --max-steps 50 --invariant missing_tip_w --hide monadbft::choreo::s --max-samples=20

Two Phase Commit Examples

OK on two_phase_commit - test

cd examples/two_phase_commit && quint test two_phase_commit.qnt --main two_phase_commit

OK on two_phase_commit - run with consistency

cd examples/two_phase_commit && quint run two_phase_commit.qnt --main two_phase_commit --invariant=consistency --max-samples=20

FAIL on two_phase_commit - wit_commit witness (should find counterexample)

cd examples/two_phase_commit && quint run two_phase_commit.qnt --main=two_phase_commit --invariant=wit_commit --max-steps=20 --max-samples=500

ATM Distributed Lock Examples

OK on atm_distributed_lock - test

cd examples/atm_distributed_lock && quint test atm_distributed.qnt --main atm_distributed

FAIL on atm_distributed_lock - canHaveConcurrentConflict witness (should find counterexample)

cd examples/atm_distributed_lock && quint run atm_distributed_witnesses.qnt --main=atm_distributed_witnesses --invariant=canHaveConcurrentConflict --max-steps=10 --max-samples=500

FAIL on atm_distributed_lock - canConflictThenCommit witness (should find counterexample)

cd examples/atm_distributed_lock && quint run atm_distributed_witnesses.qnt --main=atm_distributed_witnesses --invariant=canConflictThenCommit --max-steps=30 --max-samples=1000

Additional Verification Tests

OK on typecheck choreo

quint typecheck choreo.qnt

OK on run template

quint run template.qnt