import { ModalFormula, ModalOperator, ModalSystem } from '../types.js';
/**
* Test utilities for modal logic testing
*/
// Formula creation helpers
export function createNecessity(operand: ModalFormula): ModalFormula {
return {
type: 'modal',
operator: '□',
operand
};
}
export function createPossibility(operand: ModalFormula): ModalFormula {
return {
type: 'modal',
operator: '◇',
operand
};
}
export function createVariable(name: string): ModalFormula {
return {
type: 'variable',
name
};
}
export function createNegation(operand: ModalFormula): ModalFormula {
return {
type: 'unary',
operator: '¬',
operand
} as any;
}
export function createImplication(left: ModalFormula, right: ModalFormula): ModalFormula {
return {
type: 'binary',
operator: 'implies',
left,
right
} as any;
}
export function createConjunction(left: ModalFormula, right: ModalFormula): ModalFormula {
return {
type: 'binary',
operator: 'and',
left,
right
} as any;
}
export function createDisjunction(left: ModalFormula, right: ModalFormula): ModalFormula {
return {
type: 'binary',
operator: 'or',
left,
right
} as any;
}
// Kripke frame generators
export interface TestFrame {
worlds: string[];
relations: Array<[string, string]>;
}
export function createReflexiveFrame(worldCount: number = 2): TestFrame {
const worlds = Array.from({ length: worldCount }, (_, i) => `w${i}`);
const relations: Array<[string, string]> = worlds.map(w => [w, w]);
return { worlds, relations };
}
export function createTransitiveFrame(): TestFrame {
return {
worlds: ['w0', 'w1', 'w2'],
relations: [
['w0', 'w1'],
['w1', 'w2'],
['w0', 'w2'] // transitive closure
]
};
}
export function createSymmetricFrame(): TestFrame {
return {
worlds: ['w0', 'w1'],
relations: [
['w0', 'w1'],
['w1', 'w0']
]
};
}
export function createEquivalenceFrame(): TestFrame {
const worlds = ['w0', 'w1', 'w2'];
const relations: Array<[string, string]> = [];
// Reflexive
for (const w of worlds) {
relations.push([w, w]);
}
// Symmetric and transitive (full mesh)
for (const w1 of worlds) {
for (const w2 of worlds) {
if (w1 !== w2) {
relations.push([w1, w2]);
}
}
}
return { worlds, relations };
}
// Pre-built test formulas
export const testFormulas = {
// T axiom: □P → P
tAxiom: createImplication(
createNecessity(createVariable('P')),
createVariable('P')
),
// K axiom: □(P → Q) → (□P → □Q)
kAxiom: createImplication(
createNecessity(
createImplication(createVariable('P'), createVariable('Q'))
),
createImplication(
createNecessity(createVariable('P')),
createNecessity(createVariable('Q'))
)
),
// S4 axiom: □P → □□P
s4Axiom: createImplication(
createNecessity(createVariable('P')),
createNecessity(createNecessity(createVariable('P')))
),
// S5 axiom: ◇P → □◇P
s5Axiom: createImplication(
createPossibility(createVariable('P')),
createNecessity(createPossibility(createVariable('P')))
),
// B axiom: P → □◇P
bAxiom: createImplication(
createVariable('P'),
createNecessity(createPossibility(createVariable('P')))
),
// D axiom: □P → ◇P
dAxiom: createImplication(
createNecessity(createVariable('P')),
createPossibility(createVariable('P'))
),
// Duality: □P ↔ ¬◇¬P
duality: {
left: createNecessity(createVariable('P')),
right: createNegation(createPossibility(createNegation(createVariable('P'))))
},
// Simple formulas
simpleNecessity: createNecessity(createVariable('P')),
simplePossibility: createPossibility(createVariable('Q')),
simpleVariable: createVariable('X')
};
// Assertion helpers
export function assertModalFormula(formula: any): asserts formula is ModalFormula {
if (!formula || typeof formula !== 'object') {
throw new Error('Formula must be an object');
}
if (!('type' in formula)) {
throw new Error('Formula must have a type property');
}
if (formula.type === 'modal') {
if (!('operator' in formula) || !('operand' in formula)) {
throw new Error('Modal formula must have operator and operand');
}
}
}
export function assertVariableFormula(formula: any, expectedName?: string): void {
assertModalFormula(formula);
if (formula.type !== 'variable') {
throw new Error(`Expected variable formula, got ${formula.type}`);
}
if (expectedName && 'name' in formula && formula.name !== expectedName) {
throw new Error(`Expected variable name ${expectedName}, got ${formula.name}`);
}
}
export function assertModalOperator(formula: any, expectedOperator: ModalOperator): void {
assertModalFormula(formula);
if (formula.type !== 'modal') {
throw new Error(`Expected modal formula, got ${formula.type}`);
}
if ('operator' in formula && formula.operator !== expectedOperator) {
throw new Error(`Expected operator ${expectedOperator}, got ${formula.operator}`);
}
}
// System axiom validators
export function getSystemAxioms(system: ModalSystem): ModalFormula[] {
const axioms: ModalFormula[] = [testFormulas.kAxiom];
switch (system) {
case 'T':
axioms.push(testFormulas.tAxiom);
break;
case 'S4':
axioms.push(testFormulas.tAxiom, testFormulas.s4Axiom);
break;
case 'S5':
axioms.push(testFormulas.tAxiom, testFormulas.s5Axiom);
break;
case 'B':
axioms.push(testFormulas.tAxiom, testFormulas.bAxiom);
break;
case 'D':
axioms.push(testFormulas.dAxiom);
break;
case 'K4':
axioms.push(testFormulas.s4Axiom);
break;
case 'KB':
axioms.push(testFormulas.bAxiom);
break;
case 'KD45':
axioms.push(testFormulas.dAxiom, testFormulas.s4Axiom, testFormulas.s5Axiom);
break;
}
return axioms;
}
