Struct paralegal_policy::algo::ahb::AlwaysHappensBefore

pub struct AlwaysHappensBefore {
    reached: Trace,
    checkpointed: Vec<GlobalNode>,
    started_with: usize,
}

Statistics about the result of running crate::Context::always_happens_before that are useful to understand how the property failed.

The std::fmt::Display implementation presents the information in human readable form.

Note: Both the number of seen paths and the number of violation paths are approximations. This is because the traversal terminates when it reaches a node that was already seen. However it is guaranteed that if there are any violating paths, then the number of reaching paths reported in this struct is at least one (e.g. Self::holds is sound).

The stable API of this struct is Self::holds, Self::assert_holds and Self::is_vacuous. Otherwise the information in this struct and its printed representations should be considered unstable and for-human-eyes-only.

Fields

reached: Trace

How many paths terminated at the end?

checkpointed: Vec<GlobalNode>

How many paths lead to the checkpoints?

started_with: usize

How large was the set of initial nodes this traversal started with.

Implementations

impl AlwaysHappensBefore

pub fn report(&self, ctx: Arc<dyn HasDiagnosticsBase>)

Check this property holds and report it as diagnostics in the context.

Additionally reports if the property was vacuous or had no starting nodes.

pub fn holds(&self) -> bool

Returns true if the property that created these statistics holds.

pub fn assert_holds(&self) -> Result<()>

Fails if Self::holds is false.

pub fn is_vacuous(&self) -> bool

true if this policy applied to no paths. E.g. either no starting nodes or no path from them can reach the terminal or the checkpoints (the graphs are disjoined).

pub fn reached(&self) -> Result<Cow<'_, [(GlobalNode, GlobalNode)]>>

If the trace level is sufficient, return the pairing of start and end nodes that were found.

Trait Implementations

impl Display for AlwaysHappensBefore

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

Format the results of this combinator, using the def_info to print readable names instead of ids