Trait ConcurrentStateMachine 

pub trait ConcurrentStateMachine {
    // Required methods
    fn rules(&self) -> Vec<ConcurrentRule<Self>>;
    fn invariants(&self) -> Vec<ConcurrentInvariant<Self>>;
}

Trait for defining a concurrent stateful test.

Implement this to define the rules (actions), their concurrency-group assignments, and the invariants of a model whose rules may run concurrently against the system under test. Use #[hegel::concurrent_state_machine] for a more ergonomic way to define concurrent state machines, and run_concurrent to run one.

Groups

At any moment exactly one group is current, and only rules belonging to the current group are handed out — so rules in the same group may run concurrently with each other, rules in different groups never overlap, and the current group changes only at the join points between rounds. Groups cannot express asymmetric overlap (“put may overlap get but not delete”); that expressiveness limit is deliberate.

A rule without a group annotation is assigned to a single shared anonymous group (ANONYMOUS_GROUP), so an unannotated machine is maximally concurrent: any rule may overlap with any other, and naming groups is how overlap gets restricted. In a machine that mixes annotated and unannotated rules, the unannotated rules form their own group and therefore never overlap with any named group’s rules — do not read “no group” as “unconstrained”; it is exactly backwards there.

Required Methods

fn rules(&self) -> Vec<ConcurrentRule<Self>>

The rules (actions) that worker threads may apply to this state machine, each with its concurrency-group assignment.

fn invariants(&self) -> Vec<ConcurrentInvariant<Self>>

Invariants, run on the main thread while the worker threads are parked: checked on the machine’s initial and final state, and sampled at the join points in between with probability 1 / stateful_step_count each.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors