Module stateright::util
source · Expand description
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
- 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 similarVec
<V>
pattern but provides additional type safety to distinguish indices derived fromK1:
Into
<usize>
versus some otherK2: Into<usize>
. - A vector clock, which provides a partial causal order on events in a distributed sytem.