pub struct ProtoSpec<State, Message, R> { /* private fields */ }Implementations§
Source§impl<State, Message, R> ProtoSpec<State, Message, R>
impl<State, Message, R> ProtoSpec<State, Message, R>
Sourcepub fn init(&mut self, from: State, msg: Message, to: State)
pub fn init(&mut self, from: State, msg: Message, to: State)
Add a transition that can be executed by the initiator.
Sourcepub fn resp(&mut self, from: State, msg: Message, to: State)
pub fn resp(&mut self, from: State, msg: Message, to: State)
Add a transition that can be executed by the responder.
pub fn sim_open(&mut self, from: State, msg: Message, to: State)
Sourcepub fn check(
&self,
initial: State,
local_msg: impl Fn(&Message) -> Option<State::Action>,
)
pub fn check( &self, initial: State, local_msg: impl Fn(&Message) -> Option<State::Action>, )
Check that the protocol implementation follows the spec.
The local_msg function turns the network message under test
into a local action so that the protocol can be tested.
Sourcepub fn assert_refines<S2, R2>(
&self,
other: &ProtoSpec<S2, Message, R2>,
surjection: impl Fn(&State) -> S2,
)
pub fn assert_refines<S2, R2>( &self, other: &ProtoSpec<S2, Message, R2>, surjection: impl Fn(&State) -> S2, )
Assert that this protocol refines the other protocol.
This means that this protocol has more states than the other protocol, thus the state projection must be a surjection.
Trait Implementations§
Auto Trait Implementations§
impl<State, Message, R> Freeze for ProtoSpec<State, Message, R>
impl<State, Message, R> RefUnwindSafe for ProtoSpec<State, Message, R>
impl<State, Message, R> Send for ProtoSpec<State, Message, R>
impl<State, Message, R> Sync for ProtoSpec<State, Message, R>
impl<State, Message, R> Unpin for ProtoSpec<State, Message, R>where
R: Unpin,
impl<State, Message, R> UnsafeUnpin for ProtoSpec<State, Message, R>
impl<State, Message, R> UnwindSafe for ProtoSpec<State, Message, R>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> FutureExt for T
impl<T> FutureExt for T
Source§fn with_context(self, otel_cx: Context) -> WithContext<Self>
fn with_context(self, otel_cx: Context) -> WithContext<Self>
Source§fn with_current_context(self) -> WithContext<Self>
fn with_current_context(self) -> WithContext<Self>
Source§impl<T> Instrument for T
impl<T> Instrument for T
Source§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
Source§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more