import { BaseLogicSystem } from './base.js';
import { TemporalParser } from '../parsers/temporalParser.js';
import { TemporalValidator } from '../validators/temporalValidator.js';
import {
LogicResult,
TemporalFormula,
TemporalTrace,
SolutionStep,
InputFormat
} from '../types.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.systems.temporal;
export class TemporalLogicSystem extends BaseLogicSystem {
private parser: TemporalParser;
private validator: TemporalValidator;
constructor() {
super();
this.parser = new TemporalParser();
this.validator = new TemporalValidator();
}
validate(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
// Generate test trace
const atoms = this.extractAtoms(formula);
const trace = this.validator.generateExampleTrace(atoms, 10);
const isValid = this.validator.validate(formula, trace);
return {
system: 'temporal',
message: `The formula ${input} is ${isValid ? 'satisfied' : 'not satisfied'} in the example trace.`,
details: {
system: 'temporal',
formalizedInput: input,
analysis: {
isValid,
fallacies: [],
explanation: this.generateExplanation(formula, trace, isValid),
counterexample: isValid ? undefined : this.formatTrace(trace)
}
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error validating temporal logic:', error);
return {
code: 'TEMPORAL_VALIDATION_ERROR',
message: error instanceof Error ? error.message : 'Failed to validate temporal formula',
system: 'temporal',
status: 'error' as const,
details: {
system: 'temporal'
}
} as LogicResult;
}
}
formalize(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
const formalized = this.formulaToString(formula);
return {
system: 'temporal',
message: 'Input formalized successfully.',
details: {
system: 'temporal',
formalizedInput: formalized,
originalInput: input
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error formalizing temporal logic:', error);
return {
code: 'TEMPORAL_FORMALIZATION_ERROR',
message: error instanceof Error ? error.message : 'Failed to formalize temporal input',
system: 'temporal',
status: 'error' as const,
details: {
system: 'temporal'
}
} as LogicResult;
}
}
visualize(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
const atoms = this.extractAtoms(formula);
const trace = this.validator.generateExampleTrace(atoms, 8);
const properties = this.validator.checkProperties(trace);
const visualization = this.generateTraceVisualization(formula, trace, properties);
return {
system: 'temporal',
message: 'Visualization generated successfully.',
details: {
system: 'temporal',
formalizedInput: input,
visualization
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error visualizing temporal logic:', error);
return {
code: 'TEMPORAL_VISUALIZATION_ERROR',
message: error instanceof Error ? error.message : 'Failed to visualize temporal formula',
system: 'temporal',
status: 'error' as const,
details: {
system: 'temporal'
}
} as LogicResult;
}
}
solve(input: string, format: InputFormat): LogicResult {
try {
const formula = this.parser.parse(input);
const steps = this.generateTemporalProof(formula);
return {
system: 'temporal',
message: 'Temporal proof generated successfully.',
details: {
system: 'temporal',
formalizedInput: input,
solution: {
steps,
conclusion: `Therefore, ${input} has been analyzed using temporal logic.`
}
},
status: 'success' as const
} as LogicResult;
} catch (error) {
logger.error('Error solving temporal logic:', error);
return {
code: 'TEMPORAL_SOLVING_ERROR',
message: error instanceof Error ? error.message : 'Failed to solve temporal formula',
system: 'temporal',
status: 'error' as const,
details: {
system: 'temporal'
}
} as LogicResult;
}
}
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;
}
private formulaToString(formula: TemporalFormula): string {
switch (formula.type) {
case 'atom':
return formula.name;
case 'negation':
return `¬${this.formulaToString(formula.operand)}`;
case 'and':
return `(${this.formulaToString(formula.left)} ∧ ${this.formulaToString(formula.right)})`;
case 'or':
return `(${this.formulaToString(formula.left)} ∨ ${this.formulaToString(formula.right)})`;
case 'implication':
return `(${this.formulaToString(formula.left)} → ${this.formulaToString(formula.right)})`;
case 'temporal':
if (formula.operands.length === 1) {
return `${formula.operator}${this.formulaToString(formula.operands[0])}`;
} else {
return `(${this.formulaToString(formula.operands[0])} ${formula.operator} ${this.formulaToString(formula.operands[1])})`;
}
default:
return '?';
}
}
private formatTrace(trace: TemporalTrace): string {
let result = 'Trace:\n';
trace.states.forEach(state => {
const props = Array.from(state.propositions.entries())
.filter(([_, value]) => value)
.map(([prop, _]) => prop)
.join(', ');
result += ` t${state.time}: {${props || '∅'}}\n`;
});
return result;
}
private generateExplanation(formula: TemporalFormula, trace: TemporalTrace, isValid: boolean): string {
const formulaStr = this.formulaToString(formula);
let explanation = `Evaluating ${formulaStr} over the trace:\n\n`;
explanation += this.formatTrace(trace);
explanation += '\n';
if (formula.type === 'temporal') {
switch (formula.operator) {
case 'G':
explanation += `G (Globally): The formula must hold at all time points.\n`;
break;
case 'F':
explanation += `F (Eventually): The formula must hold at some future time point.\n`;
break;
case 'X':
explanation += `X (Next): The formula must hold at the next time point.\n`;
break;
case 'U':
explanation += `U (Until): The first formula must hold until the second becomes true.\n`;
break;
}
}
explanation += `\nResult: ${isValid ? 'SATISFIED' : 'NOT SATISFIED'}`;
return explanation;
}
private generateTraceVisualization(
formula: TemporalFormula,
trace: TemporalTrace,
properties: any
): string {
let viz = `
Temporal Logic Trace Visualization
==================================
Formula: ${this.formulaToString(formula)}
Time-line Visualization:
`;
// Create timeline
const atoms = Array.from(this.extractAtoms(formula));
// Header
viz += '\nTime: ';
trace.states.forEach(state => {
viz += ` ${state.time} `;
});
viz += '\n' + '─'.repeat(trace.states.length * 5 + 6) + '\n';
// Each atom
atoms.forEach(atom => {
viz += `${atom}: `;
trace.states.forEach(state => {
viz += state.propositions.get(atom) ? ' ■ ' : ' □ ';
});
viz += '\n';
});
// Properties
viz += '\nTrace Properties:\n';
if (properties.safety.length > 0) {
viz += ` Safety: ${properties.safety.join(', ')}\n`;
}
if (properties.liveness.length > 0) {
viz += ` Liveness: ${properties.liveness.join(', ')}\n`;
}
if (properties.fairness.length > 0) {
viz += ` Fairness: ${properties.fairness.join(', ')}\n`;
}
// Temporal operators guide
viz += `
Temporal Operators:
G (□) - Globally/Always
F (◇) - Eventually/Finally
X (○) - Next
U - Until
R - Release
W - Weak Until
`;
return viz;
}
private generateTemporalProof(formula: TemporalFormula): SolutionStep[] {
const steps: SolutionStep[] = [];
let index = 1;
steps.push({
index: index++,
statement: `Given temporal formula: ${this.formulaToString(formula)}`,
rule: 'Given',
justification: 'Initial formula to analyze'
});
// Decompose the formula
this.decomposeFormula(formula, steps, index);
return steps;
}
private decomposeFormula(formula: TemporalFormula, steps: SolutionStep[], startIndex: number): number {
let index = startIndex;
switch (formula.type) {
case 'temporal':
switch (formula.operator) {
case 'G':
steps.push({
index: index++,
statement: `G φ means φ holds at all future time points`,
rule: 'Definition of G',
justification: 'Temporal semantics'
});
break;
case 'F':
steps.push({
index: index++,
statement: `F φ means φ holds at some future time point`,
rule: 'Definition of F',
justification: 'Temporal semantics'
});
break;
case 'X':
steps.push({
index: index++,
statement: `X φ means φ holds at the next time point`,
rule: 'Definition of X',
justification: 'Temporal semantics'
});
break;
case 'U':
steps.push({
index: index++,
statement: `φ U ψ means φ holds until ψ becomes true`,
rule: 'Definition of U',
justification: 'Temporal semantics'
});
break;
}
// Add temporal logic axioms
if (formula.operator === 'G' || formula.operator === 'F') {
steps.push({
index: index++,
statement: `F φ ≡ ¬G¬φ (duality)`,
rule: 'Temporal Duality',
justification: 'F and G are dual operators'
});
}
break;
case 'implication':
steps.push({
index: index++,
statement: `Analyzing implication: ${this.formulaToString(formula.left)} → ${this.formulaToString(formula.right)}`,
rule: 'Implication',
justification: 'Breaking down the implication'
});
break;
}
return index;
}
}
