Interface: TemporalModelCheckRequest

@kortexya/reasoninglayer / Temporal / TemporalModelCheckRequest

Interface: TemporalModelCheckRequest

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

Request to check a CTL formula against an explicit finite Kripke structure.

Remarks

Stateless and tenant-free: the model is supplied in full and checked in-process. initialStates must be a subset of the declared state IDs, and both endpoints of every transition must be declared in states.

Example

const request: TemporalModelCheckRequest = {
  states: [
    { id: 0, labels: ['red'] },
    { id: 1, labels: ['green'] },
  ],
  transitions: [{ from: 0, to: 1 }, { from: 1, to: 0 }],
  initialStates: [0],
  formula: { op: 'ef', inner: { op: 'atom', name: 'green' } },
};

Properties

formula

formula: CtlFormula

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

The CTL formula tree to check.

initialStates

initialStates: number[]

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

States from which checking begins. Must be non-empty.

states

states: KripkeState[]

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

States in the Kripke model. Must be non-empty with unique IDs.

transitions?

optional transitions: KripkeTransition[]

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

Transition relation. Both endpoints must appear in states.