pub struct PdrSession<'s, P: Phase> { /* private fields */ }Expand description
A PDR session branded with lifetime 's and phase P.
Zero-sized — all phase tracking is compile-time only.
Implementations§
Source§impl<'s, P: Phase> PdrSession<'s, P>
impl<'s, P: Phase> PdrSession<'s, P>
Sourcepub fn phase_name(&self) -> &'static str
pub fn phase_name(&self) -> &'static str
Current phase name.
Source§impl<'s> PdrSession<'s, Init>
impl<'s> PdrSession<'s, Init>
Sourcepub fn build_model(self) -> PdrSession<'s, Modeled>
pub fn build_model(self) -> PdrSession<'s, Modeled>
Load a transition system model. Consumes Init, produces Modeled.
Source§impl<'s> PdrSession<'s, Modeled>
impl<'s> PdrSession<'s, Modeled>
Sourcepub fn check_safe(self) -> PdrSession<'s, Safe>
pub fn check_safe(self) -> PdrSession<'s, Safe>
Check result: property is safe (inductive invariant found).
Sourcepub fn check_counterexample(self) -> PdrSession<'s, CounterexampleFound>
pub fn check_counterexample(self) -> PdrSession<'s, CounterexampleFound>
Check result: counterexample found.
Sourcepub fn check_exhausted(self) -> PdrSession<'s, Exhausted>
pub fn check_exhausted(self) -> PdrSession<'s, Exhausted>
Check result: frame budget exhausted.
Auto Trait Implementations§
impl<'s, P> Freeze for PdrSession<'s, P>
impl<'s, P> RefUnwindSafe for PdrSession<'s, P>where
P: RefUnwindSafe,
impl<'s, P> Send for PdrSession<'s, P>where
P: Send,
impl<'s, P> Sync for PdrSession<'s, P>where
P: Sync,
impl<'s, P> Unpin for PdrSession<'s, P>where
P: Unpin,
impl<'s, P> UnsafeUnpin for PdrSession<'s, P>
impl<'s, P> UnwindSafe for PdrSession<'s, P>where
P: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more