Struct PdlModel 

pub struct PdlModel {
    pub kripke: KripkeModel,
    pub n_programs: usize,
}

A PDL model: finite Kripke frame with named atomic programs.

Fields

kripke: KripkeModel

The Kripke model underlying the PDL model.

n_programs: usize

Number of atomic programs.

Implementations

impl PdlModel

pub fn new(kripke: KripkeModel, n_programs: usize) -> Self

Create a new PDL model.

pub fn reachable(&self, start: usize, prog: &PdlProgram) -> HashSet<usize>

Compute the set of worlds reachable from start by executing program prog.

pub fn box_program( &self, w: usize, prog: &PdlProgram, phi: &ModalFormula, ) -> bool

Evaluate [α]φ at world w: all successors via α satisfy φ.

pub fn diamond_program( &self, w: usize, prog: &PdlProgram, phi: &ModalFormula, ) -> bool

Evaluate ⟨α⟩φ at world w: some successor via α satisfies φ.

Trait Implementations

impl Clone for PdlModel

fn clone(&self) -> PdlModel

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PdlModel

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

Formats the value using the given formatter.