The surface below the authoring layers. You need it to build tooling around rules — an editor, a linter, a viewer — and
not to write one.
| Node type |
|
Formula |
The union of every node. |
FormulaKind |
Its discriminant. |
Atom |
A lifted proposition. |
Not, And, Or, Implies |
The boolean connectives. |
Always |
G, valid only at the root. |
Prev, Once, Historically, Since |
The past operators. |
Next, Eventually |
The two bounded-future operators. |
Quantified |
A CTL path quantifier. Static analysis only. |
|
|
FORMULA_KINDS |
Every kind, as an array. |
BOOLEAN_KINDS, PAST_KINDS, FUTURE_KINDS |
The three families the validator reasons with. |
subformulas(f) |
Every node in the tree, flattened. |
isPastDefinite(f) |
Whether the whole formula is decidable from what has already happened. |
firstFutureKind(f) |
The first future operator found, or nothing. |
containsAlways(f), containsQuantifier(f) |
The two structural questions the constructors ask. |
|
|
describeFormula(f) |
The printed form. This is what a report shows and what cause.subformula indexes into. |
renderFormula(f) |
The printed form plus the span of every node, keyed by path. |
RenderedFormula, FormulaSpan |
What renderFormula returns. |
describeMatcher(m) |
One proposition’s printed form. |
Attribution depends on the printer: a subterm that prints one way at the top level and another when nested breaks
highlighting. How it works is why.
|
|
formulaToJSON(f) |
The document form. Refuses a formula containing a custom predicate. |
parseFormula(document) |
Back again, through the same constructors, so it meets identical structural rules. |
formulaSchema |
JSON Schema (draft 2020-12) for the document form. |
fullFormulaSchema |
The schema including the CTL fragment. |
FormulaJson, AtomJson |
The document types. |
|
|
validateFormula(f) |
The structural rules, as a report rather than a throw. |
validateRules(rules) |
The same over a whole set. |
validateMatcher(m) |
A proposition’s own validity. |
lintRules(rules) |
Advice that never fails anything. |
lintNames(spec, available) |
Whether every tool and step the rule set names actually exists. |
Available |
{ tools?, steps? } — each optional, and only what is supplied is checked. |
NameSource |
A tool or step set in whatever shape you hold it: ids, the things themselves, mixed, or the guard’s record. |
NamedSubjects |
The parts of a spec it reads, structural so a MonitorSpec satisfies it. |
EXTREME_BOUND_THRESHOLD |
The window above which extreme-bound warns: 10,000. |
ValidationError |
What a constructor throws, naming the path. |
ValidationIssue, ValidationReport, ValidationWarning |
What the validators return. |
|
|
compileMatcher(m) |
A matcher into a predicate over events. |
parseMatcher(json) |
A matcher from its document form. |
isMatcher(v), isProp(v), toProp(v) |
Narrowing between the two proposition shapes. |
The transition, exposed for anything that needs to drive it directly — a viewer scrubbing a timeline, a test asserting
state size.
|
|
compileFormula(f) |
The flat program a formula becomes. |
initialState(program) |
Its starting state. |
stepAutomaton(program, state, event) |
One transition. |
resolveAutomaton(program, state, outcome) |
End-of-run resolution. |
evaluatePast(program, state) |
The past-definite part, read directly. |
inspectAutomaton(program, state) |
The open obligations, for diagnostics. |
Program, AutomatonState, AutomatonVerdict, StepOutcome, RunOutcome |
The types those use. |
The structural model CTL rules are checked against. Build
one without a workflow engine at all with graphFromDescription.
|
|
graphFromDescription(description) |
Nodes, edges and an initial node into a WorkflowGraph. |
withTerminalSelfLoops(graph) |
The totality convention CTL semantics requires. |
TERMINAL_SELF_LOOP |
The label those added edges carry, so a report can name the convention. |
WorkflowGraph, GraphDescription, GraphNode, GraphEdge, NodeId |
The graph types. |