import { ModalLogic } from './modal.js';
describe('ModalLogic', () => {
let system: ModalLogic;
beforeEach(() => {
system = new ModalLogic();
});
describe('validate operation', () => {
test('validates formula in default system K', async () => {
const input = '□(P → Q) → (□P → □Q)';
const result = await system.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.message).toBeTruthy();
});
test('validates T axiom in system T', async () => {
system.setModalSystem('T');
const input = '(□P) → P';
const result = await system.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
});
test('validates argument', async () => {
const input = '□P, □(P → Q) therefore □Q';
const result = await system.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
});
});
describe('formalize operation', () => {
test('formalizes natural language to symbolic', async () => {
const input = 'it is necessary that P';
const result = await system.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.message).toBeTruthy();
});
});
describe('visualize operation', () => {
test('generates Kripke model visualization', async () => {
const input = '□P';
const result = await system.process('visualize', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.visualization).toBeDefined();
});
});
describe('solve operation', () => {
test('generates proof for valid argument', async () => {
system.setModalSystem('T');
const input = '□P therefore P';
const result = await system.process('solve', input, 'symbolic');
expect(result.status).toBe('success');
});
});
describe('setModalSystem', () => {
test('changes modal system', () => {
expect(() => system.setModalSystem('S5')).not.toThrow();
});
test('accepts all valid modal systems', () => {
const systems = ['K', 'T', 'D', 'B', 'K4', 'KB', 'S4', 'S5', 'KD45'];
systems.forEach(sys => {
expect(() => system.setModalSystem(sys as any)).not.toThrow();
});
});
});
describe('Integration tests', () => {
test('end-to-end: validate and solve', async () => {
system.setModalSystem('T');
const input = '□P, (□P) → P therefore P';
// Validate
const validateResult = await system.process('validate', input, 'symbolic');
expect(validateResult.status).toBe('success');
// Solve
const solveResult = await system.process('solve', input, 'symbolic');
expect(solveResult.status).toBe('success');
});
test('handles invalid formula gracefully', async () => {
const input = '□□□'; // Invalid formula
const result = await system.process('validate', input, 'symbolic');
expect(result.status).toBe('error');
expect(result.message).toBeDefined();
});
});
});
