ceetle - 计算树逻辑验证器

一个用于在计算树逻辑中定义模型并验证其语义的Rust库。更多了解请参阅维基百科。

该库是被动维护的，这意味着不会添加其他功能，但是GitHub上的问题将被回答和解决。欢迎对这个库做出贡献和反馈！

示例

考虑下面的图。

为了在库中将它构建为一个模型，我们这样做

use ceetle::{HashedDiscreteModel, ctl, CTLFormula, verify};

let model = HashedDiscreteModel::new(HashMap::from_iter(vec![
    // (state, (atoms, transitions))
    ("s0", (vec!["p", "q"],      vec!["s1"])),
    ("s1", (vec!["p"],           vec!["s0", "s3"])),
    ("s2", (vec!["p", "q"],      vec!["s2"])),
    ("s3", (vec!["p", "r", "s"], vec!["s2"]))
]));

为了验证公式 $S_0\models \text{AG}(p)$，我们这样做

verify(&model, &"s0", &ctl!(AG(Atom("p")))); // Evaluates to true

为了验证公式 $S_0 \models \text{EF(AG}(p \land q))$，我们这样做

verify(&model, &"s0", &ctl!(EF(AG(And(Atom("p"), Atom("q")))))); // Evaluates to true