Macro ceetle_macros::ctl

ctl!() { /* proc-macro */ }

ctl

The ctl macro helps generating CTL formulas much easier than using the CTLFormula. This macro uses the following syntax:

f = True | False | Atom(p) | Not(f) | AG(f) | AF(f) | AX(f) | EG(f) | EF(f) | EX(f) | And(f,f) | Or(f,f) | Imply(f,f) | AU(f,f) | EU(f,f) where p is any value.

Examples

let f = ctl!(AX(Atom(5))); // Translates to "AX(5)"
let g = ctl!(And(Atom(1), AG(Atom(3)))); // Translates to "1 ∧ AG(3)"
let h = ctl!(Or(Imply(Atom(1), Atom(3)), EU(Atom(1), Atom(2)))); // Translates to "(1 → 3) ∨ E[1 U 2]""