import { TemporalFormula, TemporalOperator } from '../types.js';
export class TemporalParser {
/**
* Parse temporal logic formula
* Supports:
* - G (always/globally): G P
* - F (eventually/finally): F P
* - X (next): X P
* - U (until): P U Q
* - R (release): P R Q
* - W (weak until): P W Q
*/
parse(input: string): TemporalFormula {
const tokens = this.tokenize(input);
return this.parseFormula(tokens);
}
private tokenize(input: string): string[] {
// Normalize input
input = input.trim()
.replace(/\s+/g, ' ')
.replace(/always/gi, 'G')
.replace(/globally/gi, 'G')
.replace(/eventually/gi, 'F')
.replace(/finally/gi, 'F')
.replace(/next/gi, 'X')
.replace(/until/gi, 'U')
.replace(/release/gi, 'R')
.replace(/weak\s+until/gi, 'W')
.replace(/→/g, '->')
.replace(/⟶/g, '->')
.replace(/implies/gi, '->')
.replace(/∧/g, '&')
.replace(/and/gi, '&')
.replace(/∨/g, '|')
.replace(/or/gi, '|')
.replace(/¬/g, '!')
.replace(/not/gi, '!')
.replace(/□/g, 'G') // Box as always
.replace(/◇/g, 'F') // Diamond as eventually
.replace(/○/g, 'X'); // Circle as next
// Tokenize
const tokens: string[] = [];
let current = '';
for (const char of input) {
if (/[A-Z]/i.test(char) || /[a-z]/i.test(char) || /[0-9]/.test(char)) {
current += char;
} else {
if (current) {
tokens.push(current);
current = '';
}
if (char !== ' ') {
tokens.push(char);
}
}
}
if (current) {
tokens.push(current);
}
return tokens;
}
private parseFormula(tokens: string[]): TemporalFormula {
return this.parseImplication(tokens);
}
private parseImplication(tokens: string[]): TemporalFormula {
const left = this.parseOr(tokens);
if (tokens[0] === '-' && tokens[1] === '>') {
tokens.shift();
tokens.shift();
const right = this.parseImplication(tokens);
return {
type: 'implication',
left,
right
};
}
return left;
}
private parseOr(tokens: string[]): TemporalFormula {
const left = this.parseAnd(tokens);
if (tokens[0] === '|') {
tokens.shift();
const right = this.parseOr(tokens);
return {
type: 'or',
left,
right
};
}
return left;
}
private parseAnd(tokens: string[]): TemporalFormula {
const left = this.parseUntil(tokens);
if (tokens[0] === '&') {
tokens.shift();
const right = this.parseAnd(tokens);
return {
type: 'and',
left,
right
};
}
return left;
}
private parseUntil(tokens: string[]): TemporalFormula {
const left = this.parseUnary(tokens);
if (tokens[0] === 'U') {
tokens.shift();
const right = this.parseUntil(tokens);
return {
type: 'temporal',
operator: 'U' as TemporalOperator,
operands: [left, right]
};
} else if (tokens[0] === 'R') {
tokens.shift();
const right = this.parseUntil(tokens);
return {
type: 'temporal',
operator: 'R' as TemporalOperator,
operands: [left, right]
};
} else if (tokens[0] === 'W') {
tokens.shift();
const right = this.parseUntil(tokens);
return {
type: 'temporal',
operator: 'W' as TemporalOperator,
operands: [left, right]
};
}
return left;
}
private parseUnary(tokens: string[]): TemporalFormula {
if (tokens[0] === '!') {
tokens.shift();
const operand = this.parseUnary(tokens);
return {
type: 'negation',
operand
};
}
if (tokens[0] === 'G') {
tokens.shift();
const operand = this.parseUnary(tokens);
return {
type: 'temporal',
operator: 'G' as TemporalOperator,
operands: [operand]
};
}
if (tokens[0] === 'F') {
tokens.shift();
const operand = this.parseUnary(tokens);
return {
type: 'temporal',
operator: 'F' as TemporalOperator,
operands: [operand]
};
}
if (tokens[0] === 'X') {
tokens.shift();
const operand = this.parseUnary(tokens);
return {
type: 'temporal',
operator: 'X' as TemporalOperator,
operands: [operand]
};
}
return this.parseAtom(tokens);
}
private parseAtom(tokens: string[]): TemporalFormula {
const firstToken = tokens[0];
if (firstToken === '(') {
tokens.shift();
const formula = this.parseFormula(tokens);
const nextToken = tokens[0];
if (nextToken === ')') {
tokens.shift();
}
return formula;
}
const atom = tokens.shift();
if (!atom) {
throw new Error('Unexpected end of input');
}
return {
type: 'atom',
name: atom
};
}
}
