Struct ExecutionCollector 

pub struct ExecutionCollector { /* private fields */ }

Keeps the terminal executions grouped by outcome. Pass one to explore when you want the graphs, canonical keys or pending sends of each outcome, not just how many there were.

Under a parallel run the executions are collected in a nondeterministic order (the counts are still exact); compare canonical-key sets, not their order.

Implementations

impl ExecutionCollector

pub fn new() -> Self

pub fn full(&self) -> Vec<Execution>

The full executions collected so far.

pub fn blocked(&self) -> Vec<Execution>

The blocked executions (maximal consistent prefixes).

pub fn errors(&self) -> Vec<Execution>

The erroneous executions.

pub fn terminals(&self) -> Vec<Execution>

Full followed by blocked - the terminal executions the search must not duplicate.

pub fn full_count(&self) -> usize

pub fn blocked_count(&self) -> usize

pub fn error_count(&self) -> usize

pub fn terminal_count(&self) -> usize

Full + blocked, the terminal count.

pub fn full_keys(&self) -> Vec<String>

Canonical keys of the full executions.

pub fn terminal_keys(&self) -> Vec<String>

Canonical keys over full plus blocked, for the duplicate check.

pub fn error_keys(&self) -> Vec<String>

Canonical keys of the erroneous executions.

Trait Implementations

impl Debug for ExecutionCollector

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ExecutionCollector

fn default() -> ExecutionCollector

Returns the “default value” for a type.

impl Observer for ExecutionCollector

fn on_execution(&self, exec: &Execution, kind: ExecutionKind)

A terminal execution (full / blocked / error) was reached.

fn on_event_added(&self, _g: &ExecutionGraph, _e: EventId)

A fresh event e, maximal in insertion order, was added to g.

fn on_rf_choice(&self, _g: &ExecutionGraph, _r: EventId, _src: Option<EventId>)

Receive r was pointed at source src (None means no message) before a consistency check.

fn on_inconsistent(&self, _g: &ExecutionGraph)

A graph was found inconsistent and dropped.

fn on_backward_revisit( &self, _g: &ExecutionGraph, _r: EventId, _s: EventId, _deleted: &BTreeSet<EventId>, )

A backward revisit that sets rf(r) to s is about to run; deleted lists the events it removes (still including s).

fn on_revisit_rejected(&self, _g: &ExecutionGraph, _r: EventId, _s: EventId)

A candidate backward revisit setting rf(r) to s was rejected.

fn on_thread_blocked(&self, _g: &ExecutionGraph, _tid: Tid)

Thread tid is blocked on a receive with no message in g.