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

• DenseNatMap
  A map optimized for cases where each key corresponds with a unique entry in the range [0..self.len()] and vice versa (each number in that range corresponds with a unique key in the map). DenseNatMap<K, V> serves as a replacement for a similar Vec<V> pattern but provides additional type safety to distinguish indices derived from K1: Into<usize> versus some other K2: Into<usize>.
• 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.
• VectorClock
  A vector clock, which provides a partial causal order on events in a distributed sytem.