Everything on this page comes from @rhysbalevicius/ltl-core. The guides for these are
presets, patterns, combinators,
propositions and checks.
Complete rules named in English. Each returns a Rule with a generated id you can override.
|
|
Presets.requireBefore(action, prerequisite, options?) |
The action may not run before the prerequisite has returned. |
Presets.requireHumanBefore(action, options?) |
A completed human approval — a run.resume — must precede the action. |
Presets.neverAfter(first, second, options?) |
Once the first has run, the second never may. |
Presets.respondWithin(call, response, options?) |
Every call is answered within a window, defaulting to DEFAULT_WITHIN. |
| Type |
|
Rule |
An id, a description, a formula, and optionally a mode. |
ToolRef |
What a preset accepts in place of a tool: the tool itself, its name, a Matcher, or a Formula. |
PresetOptions |
{ id, description, mode }, accepted by every preset. |
RespondWithinOptions |
PresetOptions plus within. |
The Dwyer specification patterns. Each returns a Formula rather than a Rule.
|
|
Patterns.absence(what, options?) |
The event never occurs, optionally only after a scope opens. |
Patterns.precedence(enabler, guarded) |
The guarded event requires the enabler to have occurred. Enabler first. |
Patterns.response(trigger, response, options) |
Every trigger is followed by a response within a required window. |
DEFAULT_WITHIN |
The window presets use when none is given: 20. |
| Type |
|
AbsenceOptions |
{ scope }. |
PatternScope |
{ after } — where a scoped pattern starts applying. |
ResponseOptions |
{ within }. |
The operators. always is root-only, eventually requires within, and a future operator may not sit inside a past
one — each refusal throws a ValidationError naming the path.
|
|
LTL.always(f) |
G f. The root of every rule. |
LTL.not(f), LTL.and(…), LTL.or(…), LTL.implies(f, g) |
The boolean connectives. |
LTL.atom(m) |
Lifts a Matcher into a Formula. |
LTL.prev(f) |
Y f — held at the previous event; false at the first. |
LTL.once(f) |
O f — has held at some point up to now. |
LTL.historically(f) |
H f — has held at every event up to now. |
LTL.since(f, g) |
f S g. |
LTL.next(f) |
X f. |
LTL.eventually(f, { within }) |
F<=k f. The bound is mandatory. |
| Type |
|
FormulaInput |
What a combinator accepts: a Formula or a Matcher. |
EventuallyOptions |
{ within }. |
Everything that takes a name takes the thing itself, which is the form to prefer where the symbol is in scope — see
propositions.
|
|
Identified |
Anything carrying a string id: a tool, a step. Structural, so the engine never learns what a Mastra tool is. |
Ref |
string | Identified — a tool or step, named or passed. |
idOf(ref) |
The name an event will carry for it. |
isIdentified(value) |
Whether a value carries an id rather than being a proposition. Total, because nothing in the formula language has an id. |
Propositions and payload matchers.
|
|
P.toolCall(name?, payload?), P.toolResult(name?, payload?) |
Tool events. |
P.stepStart(name?, payload?), P.stepFinish(name?, payload?) |
Workflow step events. |
P.runSuspend(), P.runResume(), P.runFinish(), P.agentMessage() |
Run lifecycle events. |
P.eq, P.ne, P.gt, P.gte, P.lt, P.lte, P.oneOf, P.matches, P.exists |
Field matchers. |
P.custom(label, predicate) |
Arbitrary code. Not serializable, and opaque to analysis. |
| Type |
|
Matcher |
The compiled shape of a proposition. |
Prop |
A matcher or a custom predicate. |
PayloadMatchers |
The record a proposition’s payload argument takes. |
FieldMatcher, FieldMatcherOp |
One field’s comparison, and the operator names. |
JsonValue |
What eq, ne and oneOf compare against. |
Counting and repetition, which are not temporal properties. Each accepts tool, id, description and mode.
|
|
Checks.loop({ n }) |
The same call with the same arguments, n times in a row. |
Checks.duplicateCall({ window }) |
The same call again within a window. |
Checks.callBudget({ max }) |
More than max calls in a run. |
callSignature(event) |
The name-plus-argument-hash the three of them key on. |
| Type |
|
Check |
A check as the monitor sees it. tool carries what it is scoped to, so a rule set can be read rather than parsed out of its own label. |
CheckOptions |
The options every check shares. |
LoopOptions, DuplicateCallOptions, CallBudgetOptions |
Per-check options. |
Branching-time rules, for static analysis only.
createMonitor rejects a rule containing a quantifier.
|
|
CTL.AG, CTL.EF, CTL.AF, CTL.EG, CTL.AX, CTL.EX, CTL.AU, CTL.EU |
The path quantifiers. |
Reachability.alwaysReachable(step, options?) |
AG EF stepStart(step). |
Reachability.neverForeclosed(trigger, goal, options?) |
AG(stepStart(trigger) -> EF stepStart(goal)). |
| Type |
|
StepRef |
What a reachability preset accepts in place of a step: the step itself, its id, a Matcher, or a Formula. |
ReachabilityOptions |
{ id, description }. |
Quantified |
The quantified formula node. |
CtlOp, CtlUnaryOp, CtlBinaryOp |
The operator names. |
CTL_UNARY_OPS, CTL_BINARY_OPS |
Those names as arrays, for validation and tooling. |
QUANTIFIER_MESSAGE |
What createMonitor says when it meets one. |