Struct ChannelSystemRun 

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

Representation of a CS that can be executed transition-by-transition.

The structure of the CS cannot be changed, meaning that it is not possible to introduce new PGs or modifying them, or add new channels. Though, this restriction makes it so that cloning the ChannelSystem is cheap, because only the internal state needs to be duplicated.

Implementations

impl<'def> ChannelSystemRun<'def>

pub fn new(cs: &'def ChannelSystem) -> Self

Creates a new ChannelSystemRun which allows to execute the CS as defined.

The new instance borrows the ChannelSystem to refer to the CS definition without copying its data, so that spawning instances is (relatively) inexpensive.

See also ProgramGraphRun::new.

pub fn def(&self) -> &ChannelSystem

Returns a reference to the underlying ChannelSystem defining the execution.

pub fn time(&self) -> Time

Returns the current time of the CS.

pub fn program_graph( &self, pg_id: PgId, ) -> Result<&ProgramGraphRun<'_>, CsError>

Returns an immutable reference to the ProgramGraphRuns of the Channel System associated to the given PgId.

pub fn possible_transitions( &self, ) -> impl Iterator<Item = (PgId, Action, impl Iterator<Item = impl Iterator<Item = Location>>)>

Iterates over all transitions that can be admitted in the current state.

An admissible transition is characterized by the PG it executes on, the required action and the post-state (the pre-state being necessarily the current state of the machine). The (eventual) guard is guaranteed to be satisfied.

See also ProgramGraphRun::possible_transitions.

pub fn possible_transitions_pg( &self, pg_id: PgId, ) -> Result<impl Iterator<Item = (Action, impl Iterator<Item = impl Iterator<Item = Location>>)>, CsError>

Iterates over all transitions that can be admitted in the current state for the [ProgramGraph] associated to the given PgId.

An admissible transition is characterized by the PG it executes on, the required action and the post-state (the pre-state being necessarily the current state of the machine). The (eventual) guard is guaranteed to be satisfied.

See also ProgramGraphRun::possible_transitions.

pub fn nosync_possible_transitions_pg( &self, pg_id: PgId, ) -> Result<impl Iterator<Item = (Action, impl Iterator<Item = Location>)>, CsError>

Iterates over all transitions that can be admitted in the current state for the [ProgramGraph] associated to the given PgId, optimized for the special (but common) case in which the state of the PG is given by a single location.

An admissible transition is characterized by the PG it executes on, the required action and the post-state (the pre-state being necessarily the current state of the machine). The (eventual) guard is guaranteed to be satisfied.

See also ProgramGraphRun::nosync_possible_transitions.

pub fn transition( &mut self, pg_id: PgId, action: Action, post: &[Location], ) -> Result<Option<Event>, CsError>

Executes a transition on the given PG characterized by the argument action and post-state.

Fails if the requested transition is not admissible.

See also ProgramGraphRun::transition.

pub fn wait(&mut self, delta: Time) -> Result<(), CsError>

Tries waiting for the given delta of time. Returns error if any of the PG cannot wait due to some time invariant.

pub fn can_wait(&self, delta: Time) -> bool

Checks if it is possible to wait a given amount of time-units without violating the time invariants.

pub fn is_waiting(&self) -> bool

Returns true if there is any transition from the current state that will be unlocked at some point in the future.

Trait Implementations

impl<'def> Clone for ChannelSystemRun<'def>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'def> Debug for ChannelSystemRun<'def>

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

Formats the value using the given formatter.