Interface: TemporalModelCheckResponse

@kortexya/reasoninglayer / Temporal / TemporalModelCheckResponse

Interface: TemporalModelCheckResponse

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

Result of a CTL model check.

Remarks

satisfied is true iff the formula holds in every listed initial state; satisfyingInitialStates reports exactly which ones it holds in.

counterexample is a best-effort diagnostic: it is present only when satisfied is false and the backend’s witness extractor could construct a trace for the failing formula shape. A witness whose kind the SDK does not recognise is omitted rather than surfaced untyped — satisfied and satisfyingInitialStates always carry the complete answer.

Example

const result: TemporalModelCheckResponse = await client.temporal.modelCheckCtl(request);
if (!result.satisfied) {
  console.log('fails from:', result.counterexample?.kind);
}

Properties

counterexample?

optional counterexample: CtlCounterExample

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

A counterexample witness from the first failing initial state, when one could be extracted.

satisfied

satisfied: boolean

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

true iff the formula holds in every listed initial state.

satisfyingInitialStates

satisfyingInitialStates: number[]

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

The subset of the requested initial states where the formula holds.