Trait stateright::Model [−][src]
pub trait Model: Sized { type State; type Action; fn init_states(&self) -> Vec<Self::State>; 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>; fn format_action(&self, action: &Self::Action) -> String
where
Self::Action: Debug, { ... } fn format_step(
&self,
last_state: &Self::State,
action: Self::Action
) -> Option<String>
where
Self::State: Debug, { ... } fn as_svg(&self, _path: Path<Self::State, Self::Action>) -> Option<String> { ... } fn next_steps(
&self,
last_state: &Self::State
) -> Vec<(Self::Action, Self::State)> { ... } fn next_states(&self, last_state: &Self::State) -> Vec<Self::State> { ... } fn properties(&self) -> Vec<Property<Self>> { ... } fn property(&self, name: &'static str) -> Property<Self> { ... } fn within_boundary(&self, _state: &Self::State) -> bool { ... } fn checker(self) -> CheckerBuilder<Self>
where
Self: Send + Sync + 'static,
Self::State: Hash + Send + Sync, { ... } }
Expand description
This is the primary abstraction for Stateright. Implementations model a
nondeterministic system’s evolution. If you are using Stateright’s actor framework,
then you do not need to implement this interface and can instead leverage
actor::Actor
and actor::ActorModel
.
You can instantiate a model CheckerBuilder
by calling Model::checker
.
Associated Types
Required methods
Provided methods
fn format_action(&self, action: &Self::Action) -> String where
Self::Action: Debug,
[src]
fn format_action(&self, action: &Self::Action) -> String where
Self::Action: Debug,
[src]Converts an action of this model to a more intuitive representation (e.g. for Explorer).
fn format_step(
&self,
last_state: &Self::State,
action: Self::Action
) -> Option<String> where
Self::State: Debug,
[src]
fn format_step(
&self,
last_state: &Self::State,
action: Self::Action
) -> Option<String> where
Self::State: Debug,
[src]Converts a step of this model to a more intuitive representation (e.g. for Explorer).
fn as_svg(&self, _path: Path<Self::State, Self::Action>) -> Option<String>
[src]
fn as_svg(&self, _path: Path<Self::State, Self::Action>) -> Option<String>
[src]fn next_steps(
&self,
last_state: &Self::State
) -> Vec<(Self::Action, Self::State)>
[src]
fn next_steps(
&self,
last_state: &Self::State
) -> Vec<(Self::Action, Self::State)>
[src]Indicates the steps (action-state pairs) that follow a particular state.
fn next_states(&self, last_state: &Self::State) -> Vec<Self::State>
[src]
fn next_states(&self, last_state: &Self::State) -> Vec<Self::State>
[src]Indicates the states that follow a particular state. Slightly more efficient than calling
Model::next_steps
and projecting out the states.
fn properties(&self) -> Vec<Property<Self>>
[src]
fn properties(&self) -> Vec<Property<Self>>
[src]Generates the expected properties for this model.
fn property(&self, name: &'static str) -> Property<Self>
[src]
fn property(&self, name: &'static str) -> Property<Self>
[src]Looks up a property by name. Panics if the property does not exist.
fn within_boundary(&self, _state: &Self::State) -> bool
[src]
fn within_boundary(&self, _state: &Self::State) -> bool
[src]Indicates whether a state is within the state space that should be model checked.
fn checker(self) -> CheckerBuilder<Self> where
Self: Send + Sync + 'static,
Self::State: Hash + Send + Sync,
[src]
fn checker(self) -> CheckerBuilder<Self> where
Self: Send + Sync + 'static,
Self::State: Hash + Send + Sync,
[src]Instantiates a CheckerBuilder
for this model.
Implementors
impl<A, C, H> Model for ActorModel<A, C, H> where
A: Actor,
H: Clone + Debug + Hash,
[src]
impl<A, C, H> Model for ActorModel<A, C, H> where
A: Actor,
H: Clone + Debug + Hash,
[src]fn as_svg(&self, path: Path<Self::State, Self::Action>) -> Option<String>
[src]
fn as_svg(&self, path: Path<Self::State, Self::Action>) -> Option<String>
[src]Draws a sequence diagram for the actor system.
type State = ActorModelState<A, H>
type Action = ActorModelAction<A::Msg>
fn init_states(&self) -> Vec<Self::State>
[src]
fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>)
[src]
fn next_state(
&self,
last_sys_state: &Self::State,
action: Self::Action
) -> Option<Self::State>
[src]
&self,
last_sys_state: &Self::State,
action: Self::Action
) -> Option<Self::State>
fn format_action(&self, action: &Self::Action) -> String
[src]
fn format_step(
&self,
last_state: &Self::State,
action: Self::Action
) -> Option<String> where
Self::State: Debug,
[src]
&self,
last_state: &Self::State,
action: Self::Action
) -> Option<String> where
Self::State: Debug,