Skip to main content

Scan

scan_core

Struct Scan 

Source 
pub struct Scan<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 properties is abstracted through the Oracle trait, to provide a unified interface.

Implementations§

Source§

impl<O> Scan<O>

Source

pub fn new(tsd: TransitionSystem, 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<O: Oracle + Clone> Scan<O>

Source

pub fn adaptive( &self, confidence: f64, precision: f64, ) -> Result<Report, ScanError>

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

Source

pub fn traces<T>(&self, runs: usize, path: PathBuf, model_data: &T::ModelData)
where T: Tracer,

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

Source§

impl<O> Scan<O>
where O: Oracle + Clone + Sync,

Source

pub fn par_adaptive( &self, confidence: f64, precision: f64, ) -> Result<Report, ScanError>

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

Source

pub fn par_traces<T>( &self, runs: usize, path: PathBuf, model_data: &T::ModelData, )
where T: Tracer, T::ModelData: Sync,

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

Trait Implementations§

Source§

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

Source§

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

Returns a duplicate of the value. Read more
1.0.0 (const: unstable) · Source§

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

Performs copy-assignment from source. Read more
Source§

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

Source§

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

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

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

§

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

§

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

§

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

§

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

§

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

§

impl<O> UnwindSafe for Scan<O>
where 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.