Struct Evaluator 

pub struct Evaluator<'m> { /* private fields */ }

Implementations

impl<'m> Evaluator<'m>

pub fn why_not( &self, name: &str, from: &State, to: &State, ) -> Result<Vec<Blocked>>

The actions that came closest to permitting from -> to, closest first.

Empty when the step is allowed. Every action other than the one taken fails at such a step, and reporting those would be noise rather than a diagnosis.

impl<'m> Evaluator<'m>

pub fn new(spec: &'m Spec, constants: BTreeMap<String, Value>) -> Result<Self>

Every declared constant must be given a value; a specification with a free constant has no determinate meaning at a state.

pub fn holds_at(&self, name: &str, state: &State) -> Result<bool>

Does the named state predicate hold at state?

pub fn step_allowed(&self, name: &str, from: &State, to: &State) -> Result<bool>

Is from -> to a step the named action permits?

pub fn value_of(&self, name: &str, state: &State) -> Result<Value>

pub fn eval_at( &self, expr: &'m Expr, from: &State, to: Option<&State>, ) -> Result<Value>

Trait Implementations

impl<'m> Debug for Evaluator<'m>

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

Formats the value using the given formatter.