Struct VerificationResult

Source

pub struct VerificationResult {
    pub verdict: Verdict,
    pub report: String,
    pub invariants: Vec<PInvariant>,
    pub discovered_invariants: Vec<String>,
    pub counterexample_trace: Vec<MarkingState>,
    pub counterexample_transitions: Vec<String>,
    pub elapsed_ms: u64,
    pub statistics: VerificationStatistics,
}

Expand description

Result of an SMT verification query.

Fields§

§verdict: Verdict§report: String§invariants: Vec<PInvariant>§discovered_invariants: Vec<String>§counterexample_trace: Vec<MarkingState>§counterexample_transitions: Vec<String>§elapsed_ms: u64§statistics: VerificationStatistics

Struct VerificationResult Copy item path

Fields§

Implementations§

impl VerificationResult

pub fn is_proven(&self) -> bool

pub fn is_violated(&self) -> bool

Trait Implementations§

impl Clone for VerificationResult

fn clone(&self) -> VerificationResult

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

impl Debug for VerificationResult

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

Auto Trait Implementations§

impl Freeze for VerificationResult

impl RefUnwindSafe for VerificationResult

impl Send for VerificationResult

impl Sync for VerificationResult

impl Unpin for VerificationResult

impl UnsafeUnpin for VerificationResult

impl UnwindSafe for VerificationResult

Blanket Implementations§

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

fn type_id(&self) -> TypeId

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

fn borrow(&self) -> &T

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

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

impl<T> CloneToUninit for Twhere T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

impl<T> From<T> for T

fn from(t: T) -> T

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

fn into(self) -> U

impl<T> ToOwned for Twhere T: Clone,

type Owned = T

fn to_owned(&self) -> T

fn clone_into(&self, target: &mut T)

impl<T, U> TryFrom<U> for Twhere U: Into<T>,

type Error = Infallible

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

impl<T, U> TryInto<U> for Twhere U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Struct VerificationResult

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

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

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

impl<T> CloneToUninit for T
where T: Clone,

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

impl<T> ToOwned for T
where T: Clone,

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

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,