Enum PdlProgram 

pub enum PdlProgram {
    Atomic(usize),
    Test(Box<ModalFormula>),
    Sequence(Box<PdlProgram>, Box<PdlProgram>),
    Choice(Box<PdlProgram>, Box<PdlProgram>),
    Star(Box<PdlProgram>),
}

A propositional dynamic logic program over a finite transition system.

Variants

Atomic(usize)

Atomic action (index into transition table)

Test(Box<ModalFormula>)

Test: φ? — succeeds at worlds satisfying φ

Sequence(Box<PdlProgram>, Box<PdlProgram>)

Sequential composition: α;β

Choice(Box<PdlProgram>, Box<PdlProgram>)

Non-deterministic choice: α ∪ β

Star(Box<PdlProgram>)

Kleene star (finite iteration): α*

Trait Implementations

impl Clone for PdlProgram

fn clone(&self) -> PdlProgram

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PdlProgram

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

Formats the value using the given formatter.

impl Eq for PdlProgram

impl PartialEq for PdlProgram

fn eq(&self, other: &PdlProgram) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for PdlProgram