Struct DropSelfLoops

Source

pub struct DropSelfLoops {}

Expand description

Preprocessor that drops self loops from the threshold automaton if the transition rule has no effect on the shared variables

This threshold automaton preprocessor removes self loops from the threshold automaton if the transition rule has no effect on the shared variables.

Such a self loop does not change the location of any process, nor does it change the valuations of any shared variables. Therefore, it can be safely removed from the threshold automaton.

Implementations§

Source §

impl DropSelfLoops

Source

pub fn new() -> Self

Create a new instance of the DropSelfLoop preprocessor

Trait Implementations§

Source §

impl Default for DropSelfLoops

Source §

fn default() -> Self

Returns the “default value” for a type. Read more

Source §

impl<T: ModifiableThresholdAutomaton, S: TargetSpec, C: ModelCheckerContext> Preprocessor<T, S, C> for DropSelfLoops

Source §

fn process(&self, ta: &mut T, _spec: &S, _ctx: &C)

Process the threshold automaton and attempt to simplify it

Auto Trait Implementations§

§

impl UnwindSafe for DropSelfLoops

Blanket Implementations§

Source §

impl<T> Any for T
where T: 'static + ?Sized,

Source §

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

Source §

impl<T> Borrow<T> for T
where T: ?Sized,

Source §

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

Source §

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source §

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

Source §

impl<T> From<T> for T

Source §

fn from(t: T) -> T

Returns the argument unchanged.

Source §

impl<T, U> Into for T
where U: From<T>,

Source §

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source §

impl<T> IntoEither for T

Source §

fn into_either(self, into_left: bool) -> Either<Self, Self>

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

Source §

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

§