Struct KripkeModel 

pub struct KripkeModel {
    pub num_worlds: usize,
    pub num_vars: usize,
    pub access: Vec<Vec<bool>>,
    pub val: Vec<Vec<bool>>,
}

A Kripke model for modal propositional logic.

A Kripke model M = (W, R, V) consists of:

• W: a set of worlds (indexed 0..n)
• R: an accessibility relation (as adjacency matrix)
• V: a valuation assigning truth values to atoms at each world

Fields

num_worlds: usize

Number of worlds.

num_vars: usize

Number of propositional variables.

access: Vec<Vec<bool>>

Accessibility relation: access[i][j] = world i can see world j.

val: Vec<Vec<bool>>

Valuation: val[w][p] = atom p is true at world w.

Implementations

impl KripkeModel

pub fn reflexive(num_worlds: usize, num_vars: usize) -> Self

Create a Kripke model with reflexive accessibility (for T axiom).

pub fn set_val(&mut self, world: usize, var: usize, truth: bool)

Set the valuation of variable var at world world.

pub fn set_access(&mut self, from: usize, to: usize)

Set the accessibility from world from to world to.

pub fn satisfies_at(&self, formula: &NnfFormula, world: usize) -> bool

Evaluate an NnfFormula at a given world (treating Box as necessity over accessible worlds).

pub fn is_reflexive(&self) -> bool

Check if the model is reflexive (for T axiom validity).

pub fn is_transitive(&self) -> bool

Check if the model is transitive (for S4 axiom validity).

pub fn is_symmetric(&self) -> bool

Check if the model is symmetric (for B axiom validity).

pub fn is_euclidean(&self) -> bool

Check if the model is Euclidean (for S5 axiom validity).

pub fn accessible_count(&self, world: usize) -> usize

Number of worlds accessible from a given world.