[][src]Module stateright::util

Utilities such as HashableHashSet and HashableHashMap. Those two in particular are useful because the corresponding HashSet and HashMap do not implement Hash, meaning they cannot be used directly in models.

For example, the following is rejected by the compiler:

This example deliberately fails to compile
type MyState = HashSet<u64>;
impl Model for MyModel {
    type State = MyState;
    type Action = MyAction;
    fn init_states(&self) -> Vec<Self::State> { vec![MyState::new()] }
    fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {}
    fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State> {
        None
    }
}

let checker = MyModel.checker().check(1_000);
error[E0599]: no method named `check` found for struct `stateright::checker::Checker<main::MyModel>` in the current scope
...
    = note: the method `check` exists but the following trait bounds were not satisfied:
            `std::collections::HashSet<u64>: std::hash::Hash`

The error can be resolved by swapping HashSet with HashableHashSet:

type MyState = HashableHashSet<u64>;

Structs

HashableHashMap

A HashMap wrapper that implements Hash by sorting pre-hashed entries and feeding those back into the passed-in Hasher.

HashableHashSet

A HashSet wrapper that implements Hash by sorting pre-hashed entries and feeding those back into the passed-in Hasher.