Struct mikino_api::check::CheckRes

pub struct CheckRes<'s> {
    pub okay: Set<&'s String>,
    pub cexs: Cexs<'s>,
}

Aggregrates properties that are considered “ok” and properties that have been falsified.

This type is used by induction (both in base and step), and BMC. Hence, the meaning of “ok” depends on the context. For instance, a property is “ok”

• in base if it holds in the initial states,
• in step if it is inductive,
• in BMC if no falsification has been found for it yet.

In one of these three contexts, a property “has been falsified” if it is not “ok”.

NB: A new CheckRes has all properties of the system considered “ok”.

Fields

okay: Set<&'s String>

Properties that are considered “ok”.

cexs: Cexs<'s>

Properties for which a counterexample has been found.

Implementations

impl<'s> CheckRes<'s>

pub fn new(sys: &'s Sys) -> Self

Constructor.

Produces a CheckRes where all the POs are “ok”.

pub fn all_falsified(&self) -> bool

True if all POs have been falsified.

pub fn has_falsifications(&self) -> bool

True if some POs have been falsified.

pub fn register_falsification(
    &mut self,
    po: &'s String,
    solver: &mut SFSolver
) -> Res<()>

Registers a falsification.

Errors

• when po does not belong to self.okay;
• when a falsification for po has already been registered.

Trait Implementations

impl<'s> Clone for CheckRes<'s>

fn clone(&self) -> CheckRes<'s>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'s> Debug for CheckRes<'s>

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

Formats the value using the given formatter.

impl<'sys> From<CheckRes<'sys>> for BaseRes<'sys>

fn from(res: CheckRes<'sys>) -> BaseRes<'_>

Converts to this type from the input type.

impl<'sys> From<CheckRes<'sys>> for StepRes<'sys>

fn from(res: CheckRes<'sys>) -> StepRes<'_>

Converts to this type from the input type.

impl<'sys> From<CheckRes<'sys>> for BmcRes<'sys>

fn from(res: CheckRes<'sys>) -> BmcRes<'_>

Converts to this type from the input type.