69 lines
2.0 KiB
Go
69 lines
2.0 KiB
Go
package orm
|
|
|
|
import (
|
|
"testing"
|
|
|
|
sdk "github.com/cosmos/cosmos-sdk/types"
|
|
"github.com/stretchr/testify/require"
|
|
"pgregory.net/rapid"
|
|
)
|
|
|
|
func TestSequence(t *testing.T) {
|
|
rapid.Check(t, rapid.Run(&sequenceMachine{}))
|
|
}
|
|
|
|
// sequenceMachine is a state machine model of Sequence. It simply uses a uint64
|
|
// as the model of the sequence.
|
|
type sequenceMachine struct {
|
|
store sdk.KVStore
|
|
seq *Sequence
|
|
state uint64
|
|
}
|
|
|
|
// Init sets up the real Sequence, including choosing a random initial value,
|
|
// and intialises the model state
|
|
func (m *sequenceMachine) Init(t *rapid.T) {
|
|
// Create context and KV store
|
|
ctx := NewMockContext()
|
|
m.store = ctx.KVStore(sdk.NewKVStoreKey("test"))
|
|
|
|
// Create primary key table
|
|
seq := NewSequence(0x1)
|
|
m.seq = &seq
|
|
|
|
// Choose initial sequence value
|
|
initSeqVal := rapid.Uint64().Draw(t, "initSeqVal").(uint64)
|
|
err := m.seq.InitVal(m.store, initSeqVal)
|
|
require.NoError(t, err)
|
|
|
|
// Create model state
|
|
m.state = initSeqVal
|
|
}
|
|
|
|
// Check does nothing, because all our invariants are captured in the commands
|
|
func (m *sequenceMachine) Check(t *rapid.T) {}
|
|
|
|
// NextVal is one of the model commands. It checks that the next value of the
|
|
// sequence matches the model and increments the model state.
|
|
func (m *sequenceMachine) NextVal(t *rapid.T) {
|
|
// Check that the next value in the sequence matches the model
|
|
require.Equal(t, m.state+1, m.seq.NextVal(m.store))
|
|
|
|
// Increment the model state
|
|
m.state++
|
|
}
|
|
|
|
// CurVal is one of the model commands. It checks that the current value of the
|
|
// sequence matches the model.
|
|
func (m *sequenceMachine) CurVal(t *rapid.T) {
|
|
// Check the the current value matches the model
|
|
require.Equal(t, m.state, m.seq.CurVal(m.store))
|
|
}
|
|
|
|
// PeekNextVal is one of the model commands. It checks that the next value of
|
|
// the sequence matches the model without modifying the state.
|
|
func (m *sequenceMachine) PeekNextVal(t *rapid.T) {
|
|
// Check that the next value in the sequence matches the model
|
|
require.Equal(t, m.state+1, m.seq.PeekNextVal(m.store))
|
|
}
|