import { TemporalFormula, TemporalTrace } from '../types.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.validators.temporal;
export class TemporalValidator {
// Safety limits to prevent exponential explosion
private static readonly MAX_TRACE_LENGTH = 10;
private static readonly MAX_COUNTEREXAMPLE_ATTEMPTS = 10000;
private static readonly MAX_ATOMS = 5; // 5 atoms * 10 length = 50 bits = 2^50 possible traces (way too many)
/**
* Validate temporal formula against a trace
* Returns true if the formula holds in the trace
*/
validate(formula: TemporalFormula, trace: TemporalTrace): boolean {
return this.evaluateAt(formula, trace, 0);
}
/**
* Evaluate formula at a specific time point in the trace
*/
private evaluateAt(formula: TemporalFormula, trace: TemporalTrace, time: number): boolean {
// Bounds check
if (time < 0 || time >= trace.states.length) {
return false;
}
switch (formula.type) {
case 'atom':
return trace.states[time].propositions.get(formula.name) || false;
case 'negation':
return !this.evaluateAt(formula.operand, trace, time);
case 'and':
return this.evaluateAt(formula.left, trace, time) &&
this.evaluateAt(formula.right, trace, time);
case 'or':
return this.evaluateAt(formula.left, trace, time) ||
this.evaluateAt(formula.right, trace, time);
case 'implication':
return !this.evaluateAt(formula.left, trace, time) ||
this.evaluateAt(formula.right, trace, time);
case 'temporal':
return this.evaluateTemporal(formula, trace, time);
default:
logger.error('Unknown formula type in temporal evaluation');
return false;
}
}
/**
* Evaluate temporal operators
*/
private evaluateTemporal(
formula: { type: 'temporal'; operator: string; operands: TemporalFormula[] },
trace: TemporalTrace,
time: number
): boolean {
switch (formula.operator) {
case 'X': // Next
if (time + 1 >= trace.states.length) return false;
return this.evaluateAt(formula.operands[0], trace, time + 1);
case 'G': // Globally/Always
for (let t = time; t < trace.states.length; t++) {
if (!this.evaluateAt(formula.operands[0], trace, t)) {
return false;
}
}
return true;
case 'F': // Eventually/Finally
for (let t = time; t < trace.states.length; t++) {
if (this.evaluateAt(formula.operands[0], trace, t)) {
return true;
}
}
return false;
case 'U': // Until (strong)
for (let t = time; t < trace.states.length; t++) {
if (this.evaluateAt(formula.operands[1], trace, t)) {
// Check that operands[0] held at all times before t
for (let s = time; s < t; s++) {
if (!this.evaluateAt(formula.operands[0], trace, s)) {
return false;
}
}
return true;
}
}
return false;
case 'W': // Weak Until
// P W Q = (P U Q) ∨ G P
const strongUntil = this.evaluateTemporal({
type: 'temporal',
operator: 'U',
operands: formula.operands
}, trace, time);
const always = this.evaluateTemporal({
type: 'temporal',
operator: 'G',
operands: [formula.operands[0]]
}, trace, time);
return strongUntil || always;
case 'R': // Release
// P R Q = ¬(¬P U ¬Q)
const negP: TemporalFormula = { type: 'negation', operand: formula.operands[0] };
const negQ: TemporalFormula = { type: 'negation', operand: formula.operands[1] };
const untilFormula = this.evaluateTemporal({
type: 'temporal',
operator: 'U',
operands: [negP, negQ]
}, trace, time);
return !untilFormula;
default:
logger.error(`Unknown temporal operator: ${formula.operator}`);
return false;
}
}
/**
* Generate example traces for testing
*/
generateExampleTrace(atoms: Set<string>, length: number = 5): TemporalTrace {
const states = [];
for (let t = 0; t < length; t++) {
const propositions = new Map<string, boolean>();
// Generate some interesting patterns
for (const atom of atoms) {
if (atom === 'p') {
// p is true at even times
propositions.set(atom, t % 2 === 0);
} else if (atom === 'q') {
// q is true at times >= 2
propositions.set(atom, t >= 2);
} else if (atom === 'r') {
// r is true only at time 3
propositions.set(atom, t === 3);
} else {
// Random for others
propositions.set(atom, Math.random() > 0.5);
}
}
states.push({ time: t, propositions });
}
return { states };
}
/**
* Find counterexample trace if formula is not valid
* @throws Error if too many atoms or trace length exceeds limits
*/
findCounterexample(formula: TemporalFormula, maxLength: number = 10): TemporalTrace | null {
const atoms = this.extractAtoms(formula);
// Safety checks
if (atoms.size > TemporalValidator.MAX_ATOMS) {
throw new Error(
`Too many atomic propositions (${atoms.size}). Maximum allowed is ${TemporalValidator.MAX_ATOMS}. ` +
`This would generate ${Math.pow(2, atoms.size * maxLength)} traces, causing memory exhaustion.`
);
}
const cappedLength = Math.min(maxLength, TemporalValidator.MAX_TRACE_LENGTH);
if (maxLength > TemporalValidator.MAX_TRACE_LENGTH) {
logger.warn(`Trace length ${maxLength} exceeds limit. Capping at ${TemporalValidator.MAX_TRACE_LENGTH}`);
}
let attemptCount = 0;
// Try different trace lengths
for (let length = 1; length <= cappedLength; length++) {
// Try all possible valuations
const numTraces = Math.pow(2, atoms.size * length);
for (let traceNum = 0; traceNum < numTraces; traceNum++) {
attemptCount++;
// Safety timeout: prevent infinite-seeming loops
if (attemptCount > TemporalValidator.MAX_COUNTEREXAMPLE_ATTEMPTS) {
logger.warn(`Reached maximum counterexample attempts (${TemporalValidator.MAX_COUNTEREXAMPLE_ATTEMPTS})`);
return null;
}
const trace = this.generateTraceFromNumber(atoms, length, traceNum);
if (!this.validate(formula, trace)) {
return trace;
}
}
}
return null;
}
/**
* Extract atomic propositions from formula
*/
private extractAtoms(formula: TemporalFormula): Set<string> {
const atoms = new Set<string>();
const extract = (f: TemporalFormula) => {
switch (f.type) {
case 'atom':
atoms.add(f.name);
break;
case 'negation':
extract(f.operand);
break;
case 'and':
case 'or':
case 'implication':
extract(f.left);
extract(f.right);
break;
case 'temporal':
f.operands.forEach(op => extract(op));
break;
}
};
extract(formula);
return atoms;
}
/**
* Generate a specific trace from a number encoding
*/
private generateTraceFromNumber(atoms: Set<string>, length: number, num: number): TemporalTrace {
const atomArray = Array.from(atoms);
const states = [];
for (let t = 0; t < length; t++) {
const propositions = new Map<string, boolean>();
for (let i = 0; i < atomArray.length; i++) {
const bit = (num >> (t * atomArray.length + i)) & 1;
propositions.set(atomArray[i], bit === 1);
}
states.push({ time: t, propositions });
}
return { states };
}
/**
* Check common temporal properties
*/
checkProperties(trace: TemporalTrace): {
safety: string[];
liveness: string[];
fairness: string[];
} {
const result = {
safety: [] as string[],
liveness: [] as string[],
fairness: [] as string[]
};
// Extract all propositions
const allProps = new Set<string>();
trace.states.forEach(state => {
state.propositions.forEach((_, prop) => allProps.add(prop));
});
// Check safety properties (nothing bad happens)
for (const prop of allProps) {
const alwaysTrue = trace.states.every(state => state.propositions.get(prop));
const alwaysFalse = trace.states.every(state => !state.propositions.get(prop));
if (alwaysTrue) {
result.safety.push(`${prop} is always true`);
}
if (alwaysFalse) {
result.safety.push(`${prop} is always false`);
}
}
// Check liveness properties (something good eventually happens)
for (const prop of allProps) {
const eventuallyTrue = trace.states.some(state => state.propositions.get(prop));
const eventuallyFalse = trace.states.some(state => !state.propositions.get(prop));
if (eventuallyTrue && eventuallyFalse) {
result.liveness.push(`${prop} changes value`);
}
}
// Check fairness properties
for (const prop of allProps) {
const trueCount = trace.states.filter(state => state.propositions.get(prop)).length;
const ratio = trueCount / trace.states.length;
if (ratio > 0.4 && ratio < 0.6) {
result.fairness.push(`${prop} is fairly distributed`);
}
}
return result;
}
}
