pub enum LTLFormula {
Atom(String),
Not(Box<LTLFormula>),
And(Box<LTLFormula>, Box<LTLFormula>),
Or(Box<LTLFormula>, Box<LTLFormula>),
Globally(Box<LTLFormula>),
Finally(Box<LTLFormula>),
}Expand description
LTL formula representation
Variants§
Atom(String)
Atomic proposition
Not(Box<LTLFormula>)
Negation (¬φ)
And(Box<LTLFormula>, Box<LTLFormula>)
Conjunction (φ ∧ ψ)
Or(Box<LTLFormula>, Box<LTLFormula>)
Disjunction (φ ∨ ψ)
Globally(Box<LTLFormula>)
Globally (Gφ)
Finally(Box<LTLFormula>)
Finally (Fφ)
Implementations§
Source§impl LTLFormula
impl LTLFormula
Sourcepub fn parse(s: &str) -> AnalysisResult<Self>
pub fn parse(s: &str) -> AnalysisResult<Self>
Parse LTL formula from string (simplified)
Trait Implementations§
Source§impl Clone for LTLFormula
impl Clone for LTLFormula
Source§fn clone(&self) -> LTLFormula
fn clone(&self) -> LTLFormula
Returns a duplicate of the value. Read more
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source. Read moreSource§impl Debug for LTLFormula
impl Debug for LTLFormula
Source§impl<'de> Deserialize<'de> for LTLFormula
impl<'de> Deserialize<'de> for LTLFormula
Source§fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
Auto Trait Implementations§
impl Freeze for LTLFormula
impl RefUnwindSafe for LTLFormula
impl Send for LTLFormula
impl Sync for LTLFormula
impl Unpin for LTLFormula
impl UnsafeUnpin for LTLFormula
impl UnwindSafe for LTLFormula
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