Skip to main content

TransitionSystem

scan_core

Trait TransitionSystem 

Source 
pub trait TransitionSystem {
    type Event;

    // Required methods
    fn transition(&mut self) -> Option<Self::Event>;
    fn time(&self) -> Time;
    fn time_tick(&mut self);
    fn labels(&self) -> impl Iterator<Item = bool>;
    fn state(&self) -> impl Iterator<Item = Val>;

    // Provided methods
    fn experiment<O: Oracle>(
        &mut self,
        duration: Time,
        oracle: O,
        running: Arc<AtomicBool>,
    ) -> RunOutcome { ... }
    fn trace<T, O: Oracle>(&mut self, duration: Time, oracle: O, tracer: T)
       where T: Tracer<Self::Event> { ... }
}
Expand description

Trait for types that can execute like a transition system.

Together with an Oracle, it provides a verifiable system.

Required Associated Types§

Source

type Event

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

Required Methods§

Source

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

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

Source

fn time(&self) -> Time

Current time of the TransitionSystem (for timed systems).

Source

fn time_tick(&mut self)

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

Source

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

The current values of the TransitionSystem’s labels.

Source

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

The current internal state of the TransitionSystem.

Provided Methods§

Source

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.

Source

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.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§