Type Alias: CtlFormula

CtlFormula = { op: "true"; } | { op: "false"; } | { name: string; op: "atom"; } | { inner: CtlFormula; op: "not"; } | { left: CtlFormula; op: "and"; right: CtlFormula; } | { left: CtlFormula; op: "or"; right: CtlFormula; } | { left: CtlFormula; op: "implies"; right: CtlFormula; } | { inner: CtlFormula; op: "ag"; } | { inner: CtlFormula; op: "eg"; } | { inner: CtlFormula; op: "af"; } | { inner: CtlFormula; op: "ef"; } | { inner: CtlFormula; op: "ax"; } | { inner: CtlFormula; op: "ex"; } | { left: CtlFormula; op: "au"; right: CtlFormula; } | { left: CtlFormula; op: "eu"; right: CtlFormula; }

Defined in: src/types/temporal.ts:103

A CTL (Computation Tree Logic) formula tree.

Remarks

A recursive union discriminated by op. Unary operators carry an inner child; binary operators carry left and right children; atom names an atomic proposition that must match a KripkeState label.

`op`	meaning
`true` / `false`	⊤ / ⊥
`atom`	atomic proposition `name`
`not` / `and` / `or` / `implies`	propositional connectives
`ag` / `eg`	φ globally on every / some path
`af` / `ef`	φ eventually on every / some path
`ax` / `ex`	φ in every / some immediate successor
`au` / `eu`	A[φ U ψ] / E[φ U ψ] — φ until ψ on all / some paths

The pure-LTL operators (X/G/F/U/R) and μ-calculus fixpoints are rejected by the CTL checker with HTTP 400.

The formula is a plain JSON tree — it uses no tagged ValueDto serialization; every field is a scalar or a nested formula.

Example

// AG(red → AF green) — "every red light is eventually followed by green"
const formula: CtlFormula = {
  op: 'ag',
  inner: {
    op: 'implies',
    left: { op: 'atom', name: 'red' },
    right: { op: 'af', inner: { op: 'atom', name: 'green' } },
  },
};