Struct CsModelRun 

pub struct CsModelRun<'def> { /* private fields */ }

Transition system model based on a ChannelSystem.

It is essentially a CS which keeps track of the Events produced by the execution and determining a set of predicates.

Trait Implementations

impl<'def> Clone for CsModelRun<'def>

fn clone(&self) -> CsModelRun<'def>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'def> Debug for CsModelRun<'def>

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

Formats the value using the given formatter.

impl<'def> TransitionSystem for CsModelRun<'def>

type Event = Event

The type of events produced by the execution of the system.

fn transition(&mut self) -> Option<Event>

Performs a (random) transition on the TransitionSystem and returns the raised Event, unless the execution is terminated and no further events can happen.

fn time(&self) -> Time

Current time of the TransitionSystem (for timed systems).

fn time_tick(&mut self)

Increase current time of the TransitionSystem (for timed systems).

fn labels(&self) -> impl Iterator<Item = bool>

The current values of the TransitionSystem’s labels.

fn state(&self) -> impl Iterator<Item = Val>

The current internal state of the TransitionSystem.

fn experiment<O: Oracle>( &mut self, duration: Time, oracle: O, running: Arc<AtomicBool>, ) -> RunOutcome

Runs a single execution of the TransitionSystem with a given Oracle and returns a RunOutcome.

fn trace<T, O: Oracle>(&mut self, duration: Time, oracle: O, tracer: T)

where T: Tracer<Self::Event>,

Runs a single execution of the TransitionSystem with a given Oracle and process the execution trace via the given Tracer.