Skip to content
KortexyaKortexyaReasoning Layer SDK

Interface: TemporalModelCheckResponse

@kortexya/reasoninglayer

@kortexya/reasoninglayer / TemporalModelCheckResponse

Interface: TemporalModelCheckResponse

Section titled “Interface: TemporalModelCheckResponse”

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

Result of a CTL model check.

Remarks

Section titled “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

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

Properties

Section titled “Properties”

counterexample?

Section titled “counterexample?”

optional counterexample?: CtlCounterExample

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

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

satisfied

Section titled “satisfied”

satisfied: boolean

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

true iff the formula holds in every listed initial state.

satisfyingInitialStates

Section titled “satisfyingInitialStates”

satisfyingInitialStates: number[]

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

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