ltl-core: monitoring

`createMonitor(spec)`

Builds a monitor from a rule set. Returns a Monitor.

const monitor = createMonitor({
  rules: [SEC_01],
  checks: [Checks.callBudget({ max: 8 })],
  onViolation: 'observe',
})

`MonitorSpec` field
`rules`	The rules.
`checks`	The native checks.
`onViolation`	A default mode for every rule that does not declare one.
`enforce`	Shorthand for abort everywhere. A rule’s own mode still wins.
`onPredicateError`	Called with the error, the rule id and the event when a custom predicate throws.

`Monitor` member
`peek(event)`	What this event would mean. Runs the transition and throws the state away.
`step(event)`	Commits the event and keeps the resulting state.
`finish(outcome, runId?)`	Resolves what is still open, for one run or for every run seen.
`release(runId)`	Drops a finished run’s state, so a long-lived guard stays bounded.
`rules`	The rule manifest, with the mode the engine would actually enforce.

`checkTrace(spec, events)`

Folds a fresh monitor over a list of events and returns the verdicts. The same fold a live run uses, which is why a test assertion and a runtime verdict mean the same thing.

const verdicts = checkTrace(SPEC, events)

Verdicts

Type
`VerdictEvent`	One verdict: the rule, the status, the mode, and the cause.
`VerdictStatus`	`satisfied`, `violated`, `pending`, `unresolved`. See the lattice.
`Leaning`	`satisfy` or `violate` — which way a `pending` obligation would fall. Present only on `pending`.
`VerdictCause`	`{ event, subformula }`. The subformula is always a substring of the rule’s printed form.
`VerdictRuleRef`	`{ id, description }`, carried on every verdict.
`Action`	`observe`, `deny`, `suspend`, `abort`. See enforcement modes.

Events

Type
`TraceEvent`	The one thing the engine reasons about. See the event model.
`TraceEventKind`	The eight kinds.
`TRACE_EVENT_KINDS`	Those kinds as an array.

Monitor internals

Exported because a tool that inspects a monitor needs them, not because a rule author does.


`MonitorState`	The whole monitor’s state, partitioned by `runId`.
`PropertyState`	One rule’s or check’s state within it.
`Transition`	The `(state, event) => { state, verdicts }` shape everything is built from.

`FORMAT_VERSION`

Stamped into every artifact ltl check writes. A reader should check it and say so when it does not recognise the value, rather than rendering half a document that looks authoritative. See artifacts.