Skip to main content

Scan

scan_core

Struct Scan 

Source 
pub struct Scan<TsG, O> { /* private fields */ }
Expand description

The main type to interface with the verification capabilities of SCAN. Scan holds the model, properties and other data necessary to run the verification process. The type of models and properties is abstracted through the TransitionSystem and Oracle traits, to provide a unified interface.

Implementations§

Source§

impl<TsG, O> Scan<TsG, O>

Source

pub fn new(tsd: TsG, oracle: O) -> Self

Create new Scan object.

Source

pub fn running(&self) -> bool

Tells whether a verification task is currently running.

Source

pub fn successes(&self) -> u32

Returns the number of successful executions in the current verification run.

Source

pub fn failures(&self) -> u32

Returns the number of failed executions in the current verification run.

Source

pub fn violations(&self) -> Vec<u32>

Returns a vector where each entry contains the number of violations of the associated property in the current verification run.

Source§

impl<TsG: TransitionSystemGenerator, O: Oracle> Scan<TsG, O>

Source

pub fn adaptive(&self, confidence: f64, precision: f64, duration: Time)

Statistically verifies the provided TransitionSystem using adaptive bound and the given parameters.

Source

pub fn traces<'a, T>(&'a self, runs: usize, tracer: T, duration: Time)
where T: Clone + Tracer<<<TsG as TransitionSystemGenerator>::Ts<'a> as TransitionSystem>::Event>,

Produces and saves the traces for the given number of runs, using the provided Tracer.

Source§

impl<TsG, O> Scan<TsG, O>
where TsG: TransitionSystemGenerator + Sync, O: Oracle + Sync,

Source

pub fn par_adaptive(&self, confidence: f64, precision: f64, duration: Time)

Statistically verifies the provided TransitionSystem using adaptive bound and the given parameters, spawning multiple threads.

Source

pub fn par_traces<'a, T>(&'a self, runs: usize, tracer: T, duration: Time)
where T: Clone + Sync + Tracer<<<TsG as TransitionSystemGenerator>::Ts<'a> as TransitionSystem>::Event>,

Produces and saves the traces for the given number of runs, using the provided Tracer, spawning multiple threads.

Trait Implementations§

Source§

impl<TsG: Clone, O: Clone> Clone for Scan<TsG, O>

Source§

fn clone(&self) -> Scan<TsG, O>

Returns a duplicate of the value. Read more
1.0.0 · Source§

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

Performs copy-assignment from source. Read more
Source§

impl<TsG: Debug, O: Debug> Debug for Scan<TsG, O>

Source§

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

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

impl<TsG, O> Freeze for Scan<TsG, O>
where TsG: Freeze, O: Freeze,

§

impl<TsG, O> RefUnwindSafe for Scan<TsG, O>
where TsG: RefUnwindSafe, O: RefUnwindSafe,

§

impl<TsG, O> Send for Scan<TsG, O>
where TsG: Send, O: Send,

§

impl<TsG, O> Sync for Scan<TsG, O>
where TsG: Sync, O: Sync,

§

impl<TsG, O> Unpin for Scan<TsG, O>
where TsG: Unpin, O: Unpin,

§

impl<TsG, O> UnsafeUnpin for Scan<TsG, O>
where TsG: UnsafeUnpin, O: UnsafeUnpin,

§

impl<TsG, O> UnwindSafe for Scan<TsG, O>
where TsG: UnwindSafe, O: UnwindSafe,

Blanket Implementations§

Source§

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

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

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

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

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

Source§

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

Mutably borrows from an owned value. Read more
Source§

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

Source§

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

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

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

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> IntoEither for T

Source§

fn into_either(self, into_left: bool) -> Either<Self, Self>

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
Source§

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
Source§

impl<T> Pointable for T

Source§

const ALIGN: usize

The alignment of pointer.
Source§

type Init = T

The type for initializers.
Source§

unsafe fn init(init: <T as Pointable>::Init) -> usize

Initializes a with the given initializer. Read more
Source§

unsafe fn deref<'a>(ptr: usize) -> &'a T

Dereferences the given pointer. Read more
Source§

unsafe fn deref_mut<'a>(ptr: usize) -> &'a mut T

Mutably dereferences the given pointer. Read more
Source§

unsafe fn drop(ptr: usize)

Drops the object pointed to by the given pointer. Read more
Source§

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

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

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

Uses borrowed data to replace owned data, usually by cloning. Read more
Source§

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

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

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

Performs the conversion.
Source§

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

Source§

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

The type returned in the event of a conversion error.
Source§

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

Performs the conversion.