Struct Constraints

pub struct Constraints<T: FsmTypes> {
    pub preconditions: HashMap<&'static str, Vec<(Pred<T>, String)>>,
    pub invariants: Vec<(Pred<T>, String)>,
    pub transitions: HashMap<(&'static str, &'static str), TransitionCheck<T>>,
}

Fields

preconditions: HashMap<&'static str, Vec<(Pred<T>, String)>>

invariants: Vec<(Pred<T>, String)>

transitions: HashMap<(&'static str, &'static str), TransitionCheck<T>>

Implementations

impl<T: FsmTypes> Constraints<T>

pub fn new() -> Constraints<T>

pub fn check_preconditions( &self, state: &'static str, ctx: &T::Context, ) -> Result<(), String>

pub fn check_invariants(&self, ctx: &T::Context) -> Result<(), String>

pub fn check_transition( &self, from: &'static str, to: &'static str, init_ctx: &T::Context, final_ctx: &T::Context, msg: &T::Msg, output: &Vec<T::Output>, ) -> Result<(), String>

Verify a transition result

from is the from state, to is the to state, init_ctx is the internal data state of the fsm before the transition final_ctx is the internal data state of the fsm after the transition msg is the message that caused the transition output is the output messages as a result of the transition

Returns an error string if the transition check fails