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:

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().spawn_bfs().join();

error[E0277]: the trait bound `HashSet<u64>: Hash` is not satisfied

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.