import { ModalValidator } from './modalValidator.js';
import { ModalParser } from '../parsers/modalParser.js';
import {
testFormulas,
createNecessity,
createPossibility,
createVariable,
createImplication,
createNegation
} from '../test-utils/modalTestHelpers.js';
import { ModalSystem } from '../types.js';
describe('ModalValidator', () => {
let validator: ModalValidator;
let parser: ModalParser;
beforeEach(() => {
validator = new ModalValidator();
parser = new ModalParser();
});
describe('T Axiom Validation (□P → P)', () => {
test('T axiom is valid in system T', () => {
const isValid = validator.isValid(testFormulas.tAxiom, 'T');
expect(isValid).toBe(true);
});
test('T axiom is valid in system S4', () => {
const isValid = validator.isValid(testFormulas.tAxiom, 'S4');
expect(isValid).toBe(true);
});
test('T axiom is valid in system S5', () => {
const isValid = validator.isValid(testFormulas.tAxiom, 'S5');
expect(isValid).toBe(true);
});
test('T axiom is invalid in system K', () => {
const isValid = validator.isValid(testFormulas.tAxiom, 'K');
expect(isValid).toBe(false);
});
});
describe('K Axiom Validation (□(P → Q) → (□P → □Q))', () => {
test('K axiom is valid in system K', () => {
const isValid = validator.isValid(testFormulas.kAxiom, 'K');
expect(isValid).toBe(true);
});
test('K axiom is valid in all systems', () => {
const systems: ModalSystem[] = ['K', 'T', 'D', 'B', 'K4', 'KB', 'S4', 'S5', 'KD45'];
systems.forEach(system => {
const isValid = validator.isValid(testFormulas.kAxiom, system);
expect(isValid).toBe(true);
});
});
});
describe('S4 Axiom Validation (□P → □□P)', () => {
test('S4 axiom is valid in system S4', () => {
const isValid = validator.isValid(testFormulas.s4Axiom, 'S4');
expect(isValid).toBe(true);
});
test('S4 axiom is valid in system S5', () => {
const isValid = validator.isValid(testFormulas.s4Axiom, 'S5');
expect(isValid).toBe(true);
});
test('S4 axiom is invalid in system K', () => {
const isValid = validator.isValid(testFormulas.s4Axiom, 'K');
expect(isValid).toBe(false);
});
test('S4 axiom is invalid in system T', () => {
const isValid = validator.isValid(testFormulas.s4Axiom, 'T');
expect(isValid).toBe(false);
});
});
describe('D Axiom Validation (□P → ◇P)', () => {
test('D axiom is valid in system D', () => {
const isValid = validator.isValid(testFormulas.dAxiom, 'D');
expect(isValid).toBe(true);
});
test('D axiom is invalid in system K', () => {
const isValid = validator.isValid(testFormulas.dAxiom, 'K');
expect(isValid).toBe(false);
});
});
describe('B Axiom Validation (P → □◇P)', () => {
test('B axiom is valid in system B', () => {
const isValid = validator.isValid(testFormulas.bAxiom, 'B');
expect(isValid).toBe(true);
});
test('B axiom is valid in system S5', () => {
const isValid = validator.isValid(testFormulas.bAxiom, 'S5');
expect(isValid).toBe(true);
});
test('B axiom is invalid in system K', () => {
const isValid = validator.isValid(testFormulas.bAxiom, 'K');
expect(isValid).toBe(false);
});
});
describe('Duality Validation', () => {
test('validates □P equivalent to ¬◇¬P', () => {
const boxP = createNecessity(createVariable('P'));
const notDiamondNotP = createNegation(
createPossibility(createNegation(createVariable('P')))
);
const isValid1 = validator.isValid(boxP, 'K');
const isValid2 = validator.isValid(notDiamondNotP, 'K');
// Both should have same validity pattern
expect(isValid1).toBe(isValid2);
});
test('validates ◇P equivalent to ¬□¬P', () => {
const diamondP = createPossibility(createVariable('P'));
const notBoxNotP = createNegation(
createNecessity(createNegation(createVariable('P')))
);
const isValid1 = validator.isValid(diamondP, 'K');
const isValid2 = validator.isValid(notBoxNotP, 'K');
expect(isValid1).toBe(isValid2);
});
});
describe('Countermodel Generation', () => {
test('generates countermodel for invalid formula in K', () => {
const isValid = validator.isValid(testFormulas.tAxiom, 'K');
expect(isValid).toBe(false);
const countermodel = validator.getLastCountermodel();
expect(countermodel).toBeDefined();
if (countermodel) {
expect(countermodel.frame.worlds.length).toBeGreaterThan(0);
}
});
test('no countermodel for valid formula', () => {
const isValid = validator.isValid(testFormulas.kAxiom, 'K');
expect(isValid).toBe(true);
const countermodel = validator.getLastCountermodel();
expect(countermodel).toBeNull();
});
test('countermodel shows where formula fails', () => {
validator.isValid(testFormulas.tAxiom, 'K');
const countermodel = validator.getLastCountermodel();
if (countermodel) {
expect(countermodel.frame.valuation).toBeDefined();
expect(countermodel.frame.worlds).toBeDefined();
expect(countermodel.frame.accessibility).toBeDefined();
expect(countermodel.failingWorld).toBeDefined();
}
});
});
describe('Argument Validation', () => {
test('validates modus ponens in modal logic', () => {
const arg = parser.parseArgument('□P, □(P → Q) therefore □Q', 'symbolic', 'K');
const isValid = validator.isArgumentValid(arg);
expect(isValid).toBe(true);
});
test('validates necessitation rule', () => {
const arg = parser.parseArgument('P therefore □P', 'symbolic', 'K');
const isValid = validator.isArgumentValid(arg);
// This should be invalid without necessitation context
expect(isValid).toBe(false);
});
test('invalidates fallacious modal reasoning', () => {
const arg = parser.parseArgument('◇P therefore □P', 'symbolic', 'K');
const isValid = validator.isArgumentValid(arg);
expect(isValid).toBe(false);
});
test('validates T system argument', () => {
const arg = parser.parseArgument('□P therefore P', 'symbolic', 'T');
const isValid = validator.isArgumentValid(arg);
expect(isValid).toBe(true);
});
test('validates S4 system argument', () => {
const arg = parser.parseArgument('□P therefore □□P', 'symbolic', 'S4');
const isValid = validator.isArgumentValid(arg);
expect(isValid).toBe(true);
});
});
describe('Edge Cases', () => {
test('handles simple variable', () => {
const isValid = validator.isValid(createVariable('P'), 'K');
// A variable alone is satisfiable but not valid (not true in all models)
expect(isValid).toBe(false);
});
test('handles negated necessity', () => {
const formula = createNegation(createNecessity(createVariable('P')));
const isValid = validator.isValid(formula, 'K');
expect(isValid).toBe(false);
});
test('handles deeply nested modalities', () => {
const formula = createNecessity(
createPossibility(
createNecessity(
createVariable('P')
)
)
);
const isValid = validator.isValid(formula, 'K');
expect(isValid).toBeDefined();
});
test('handles complex propositional structure', () => {
const formula = createImplication(
createNecessity(createVariable('P')),
createPossibility(createVariable('Q'))
);
const isValid = validator.isValid(formula, 'K');
expect(isValid).toBeDefined();
});
});
});
