Introduction

ctlver is a compiler-time CTL model checker I wrote while learning formal verification methods.

You can read about the CTL logic and its applications to formal verification on wikipedia: https://en.wikipedia.org/wiki/Computation_tree_logic.

Examples

/* define propositional variable */
using Start = decltype("start"_prop);
using Heat = decltype("heat"_prop);

/* define CTL formula */
using formula = decltype("AG(start -> AF(heat))"_CTL);

/* define Kripke model on which you want to check the formula against */
using model = KripkeModel<
    List<Node<0>, Node<1>, ...>, /* states */
    List<Node<0>, ...>,          /* initial states */
    List<
        Edge<Node<0>, Node<1>>,
        ...
    >,                           /* transition relation */
    DefaultDict<
        KV<Node<1>, List<Start>>,
        KV<Node<2>, List<Start, Heat>>,
        ...
    >                            /* labeling function */
>;

/* get states that satisfy the formula */
using satisfying_states = typename CTLCheck<model, formula>::Satisfy;