import { PredicateFormula } from '../../../types.js';
/**
* Model structure for predicate logic
*/
export interface PredicateModel {
domain: string[];
constants: Map<string, string>;
functions: Map<string, Map<string, string>>;
predicates: Map<string, Set<string>>;
}
/**
* Visualization options for model visualizer
*/
export interface ModelVisualizerOptions {
showDomain?: boolean;
showConstants?: boolean;
showFunctions?: boolean;
showPredicates?: boolean;
colorScheme?: 'default' | 'colorblind' | 'monochrome';
layout?: 'vertical' | 'horizontal' | 'compact';
}
/**
* Visualizer for predicate logic models
* Shows domain, constants, function interpretations, and predicate extensions
*/
export class ModelVisualizer {
private model: PredicateModel;
private options: ModelVisualizerOptions;
constructor(model: PredicateModel, options: ModelVisualizerOptions = {}) {
this.model = model;
this.options = {
showDomain: true,
showConstants: true,
showFunctions: true,
showPredicates: true,
colorScheme: 'default',
layout: 'vertical',
...options
};
}
/**
* Generate a visualization of the model
* @param format Output format
* @returns Visualization string
*/
visualize(format: 'html' | 'svg' | 'text' = 'html'): string {
switch (format) {
case 'html':
return this.generateHTMLVisualization();
case 'svg':
return this.generateSVGVisualization();
case 'text':
return this.generateTextVisualization();
default:
return this.generateHTMLVisualization();
}
}
/**
* Generate HTML visualization of the model
* @returns HTML string
*/
private generateHTMLVisualization(): string {
let html = '<div class="predicate-model-visualization">\n';
html += this.generateHTMLStyles();
if (this.options.layout === 'horizontal') {
html += '<div class="model-container horizontal">\n';
} else {
html += '<div class="model-container vertical">\n';
}
// Domain visualization
if (this.options.showDomain) {
html += this.generateDomainHTML();
}
// Constants visualization
if (this.options.showConstants) {
html += this.generateConstantsHTML();
}
// Functions visualization
if (this.options.showFunctions) {
html += this.generateFunctionsHTML();
}
// Predicates visualization
if (this.options.showPredicates) {
html += this.generatePredicatesHTML();
}
html += '</div>\n</div>';
return html;
}
/**
* Generate domain section HTML
* @returns HTML for domain visualization
*/
private generateDomainHTML(): string {
let html = '<div class="domain-section">\n';
html += '<h3>Domain</h3>\n';
html += '<div class="domain-container">\n';
this.model.domain.forEach((element, index) => {
html += `<div class="domain-element" style="background-color: ${this.getElementColor(index)}">${element}</div>\n`;
});
html += '</div>\n</div>\n';
return html;
}
/**
* Generate constants section HTML
* @returns HTML for constants visualization
*/
private generateConstantsHTML(): string {
let html = '';
if (this.model.constants.size > 0) {
html += '<div class="constants-section">\n';
html += '<h3>Constants</h3>\n';
html += '<div class="constants-container">\n';
this.model.constants.forEach((value, key) => {
const valueIndex = this.model.domain.indexOf(value);
html += `<div class="constant-item">\n`;
html += `<span class="constant-name">${key}</span> = \n`;
html += `<span class="constant-value" style="background-color: ${this.getElementColor(valueIndex)}">${value}</span>\n`;
html += '</div>\n';
});
html += '</div>\n</div>\n';
}
return html;
}
/**
* Generate functions section HTML
* @returns HTML for functions visualization
*/
private generateFunctionsHTML(): string {
let html = '';
if (this.model.functions.size > 0) {
html += '<div class="functions-section">\n';
html += '<h3>Functions</h3>\n';
this.model.functions.forEach((mapping, functionName) => {
html += `<div class="function-item">\n`;
html += `<h4>${functionName}</h4>\n`;
html += '<table class="function-table">\n';
html += '<thead><tr><th>Input</th><th>Output</th></tr></thead>\n';
html += '<tbody>\n';
mapping.forEach((output, input) => {
const outputIndex = this.model.domain.indexOf(output);
html += '<tr>\n';
html += `<td>${input}</td>\n`;
html += `<td style="background-color: ${this.getElementColor(outputIndex)}">${output}</td>\n`;
html += '</tr>\n';
});
html += '</tbody>\n</table>\n</div>\n';
});
html += '</div>\n';
}
return html;
}
/**
* Generate predicates section HTML
* @returns HTML for predicates visualization
*/
private generatePredicatesHTML(): string {
let html = '';
if (this.model.predicates.size > 0) {
html += '<div class="predicates-section">\n';
html += '<h3>Predicates</h3>\n';
this.model.predicates.forEach((extension, predicateName) => {
html += `<div class="predicate-item">\n`;
html += `<h4>${predicateName}</h4>\n`;
html += '<div class="predicate-extension">\n';
html += '<p>True for:</p>\n';
if (extension.size > 0) {
html += '<div class="predicate-true-tuples">\n';
extension.forEach(tuple => {
html += `<span class="tuple">${tuple}</span>\n`;
});
html += '</div>\n';
} else {
html += '<p class="empty-extension">∅ (empty set)</p>\n';
}
html += '</div>\n</div>\n';
});
html += '</div>\n';
}
return html;
}
/**
* Generate styles for HTML visualization
* @returns CSS style string
*/
private generateHTMLStyles(): string {
return `
<style>
.predicate-model-visualization {
font-family: Arial, sans-serif;
padding: 20px;
background-color: #f8f9fa;
border-radius: 10px;
box-shadow: 0 2px 4px rgba(0,0,0,0.1);
}
.model-container {
display: flex;
gap: 20px;
}
.model-container.vertical {
flex-direction: column;
}
.model-container.horizontal {
flex-direction: row;
flex-wrap: wrap;
}
.domain-section, .constants-section, .functions-section, .predicates-section {
border: 1px solid #dee2e6;
border-radius: 8px;
padding: 15px;
background-color: white;
margin-bottom: 15px;
}
h3 {
margin-top: 0;
color: #343a40;
border-bottom: 2px solid #343a40;
padding-bottom: 5px;
}
h4 {
margin-top: 15px;
color: #495057;
}
.domain-container {
display: flex;
flex-wrap: wrap;
gap: 10px;
margin-top: 10px;
}
.domain-element {
padding: 5px 10px;
border-radius: 5px;
border: 1px solid #ced4da;
color: white;
font-weight: bold;
min-width: 30px;
text-align: center;
}
.constants-container {
display: flex;
flex-direction: column;
gap: 8px;
margin-top: 10px;
}
.constant-item {
display: flex;
align-items: center;
gap: 10px;
}
.constant-name {
font-weight: bold;
min-width: 40px;
}
.constant-value {
padding: 3px 8px;
border-radius: 5px;
border: 1px solid #ced4da;
color: white;
font-weight: bold;
}
.function-table {
margin-top: 10px;
border-collapse: collapse;
width: 100%;
}
.function-table th, .function-table td {
border: 1px solid #dee2e6;
padding: 5px 10px;
text-align: center;
}
.function-table th {
background-color: #e9ecef;
}
.predicate-extension {
margin-top: 10px;
}
.predicate-true-tuples {
display: flex;
flex-wrap: wrap;
gap: 8px;
margin-top: 10px;
}
.tuple {
background-color: #28a745;
color: white;
padding: 3px 8px;
border-radius: 5px;
border: 1px solid #218838;
}
.empty-extension {
color: #6c757d;
font-style: italic;
}
</style>
`;
}
/**
* Generate SVG visualization of the model
* @returns SVG string
*/
private generateSVGVisualization(): string {
const width = 800;
const height = 600;
let y = 50;
const spacing = 20;
const elementSize = 30;
let svg = `<svg width="${width}" height="${height}" xmlns="http://www.w3.org/2000/svg">\n`;
svg += '<rect x="0" y="0" width="100%" height="100%" fill="#f8f9fa" rx="10" />\n';
// Domain visualization
if (this.options.showDomain) {
svg += `<text x="40" y="${y}" font-family="Arial" font-size="18" font-weight="bold">Domain</text>\n`;
y += 30;
let x = 40;
this.model.domain.forEach((element, index) => {
const color = this.getElementColor(index);
svg += `<rect x="${x}" y="${y}" width="${elementSize}" height="${elementSize}" fill="${color}" rx="5" />\n`;
svg += `<text x="${x + elementSize/2}" y="${y + elementSize/2 + 5}" text-anchor="middle" font-family="Arial" font-size="14" fill="white">${element}</text>\n`;
x += elementSize + 10;
});
y += elementSize + spacing;
}
// Constants visualization
if (this.options.showConstants && this.model.constants.size > 0) {
svg += `<text x="40" y="${y}" font-family="Arial" font-size="18" font-weight="bold">Constants</text>\n`;
y += 30;
let x = 40;
this.model.constants.forEach((value, key) => {
const valueIndex = this.model.domain.indexOf(value);
const color = this.getElementColor(valueIndex);
svg += `<text x="${x}" y="${y + 15}" font-family="Arial" font-size="14">${key} =</text>\n`;
x += 40;
svg += `<rect x="${x}" y="${y}" width="${elementSize}" height="${elementSize}" fill="${color}" rx="5" />\n`;
svg += `<text x="${x + elementSize/2}" y="${y + elementSize/2 + 5}" text-anchor="middle" font-family="Arial" font-size="14" fill="white">${value}</text>\n`;
x += elementSize + 30;
});
y += elementSize + spacing;
}
// Functions visualization
if (this.options.showFunctions && this.model.functions.size > 0) {
svg += `<text x="40" y="${y}" font-family="Arial" font-size="18" font-weight="bold">Functions</text>\n`;
y += 30;
this.model.functions.forEach((mapping, functionName) => {
svg += `<text x="60" y="${y}" font-family="Arial" font-size="16" font-weight="bold">${functionName}</text>\n`;
y += 25;
let x = 80;
mapping.forEach((output, input) => {
const outputIndex = this.model.domain.indexOf(output);
const color = this.getElementColor(outputIndex);
svg += `<text x="${x}" y="${y + 15}" font-family="Arial" font-size="14" text-anchor="middle">${input}</text>\n`;
svg += `<line x1="${x + 10}" y1="${y + 20}" x2="${x + 10}" y2="${y + 40}" stroke="#ced4da" stroke-width="1" />\n`;
svg += `<rect x="${x - 10}" y="${y + 40}" width="${elementSize}" height="${elementSize}" fill="${color}" rx="5" />\n`;
svg += `<text x="${x + 10}" y="${y + 60}" text-anchor="middle" font-family="Arial" font-size="14" fill="white">${output}</text>\n`;
x += elementSize + 20;
});
y += elementSize + 50;
});
y += spacing;
}
// Predicates visualization
if (this.options.showPredicates && this.model.predicates.size > 0) {
svg += `<text x="40" y="${y}" font-family="Arial" font-size="18" font-weight="bold">Predicates</text>\n`;
y += 30;
this.model.predicates.forEach((extension, predicateName) => {
svg += `<text x="60" y="${y}" font-family="Arial" font-size="16" font-weight="bold">${predicateName}</text>\n`;
y += 25;
if (extension.size > 0) {
let x = 80;
extension.forEach(tuple => {
svg += `<rect x="${x}" y="${y - 20}" width="${elementSize * 1.5}" height="${elementSize}" fill="#28a745" rx="5" />\n`;
svg += `<text x="${x + elementSize * 0.75}" y="${y - 5}" text-anchor="middle" font-family="Arial" font-size="14" fill="white">${tuple}</text>\n`;
x += elementSize * 1.5 + 10;
});
} else {
svg += `<text x="80" y="${y}" font-family="Arial" font-size="14" fill="#6c757d">∅ (empty set)</text>\n`;
}
y += elementSize + spacing;
});
}
svg += '</svg>';
return svg;
}
/**
* Generate text visualization of the model
* @returns Plain text string
*/
private generateTextVisualization(): string {
let text = 'Predicate Logic Model\n';
text += '===================\n\n';
// Domain
if (this.options.showDomain) {
text += 'Domain:\n';
text += '{ ' + this.model.domain.join(', ') + ' }\n\n';
}
// Constants
if (this.options.showConstants && this.model.constants.size > 0) {
text += 'Constants:\n';
this.model.constants.forEach((value, key) => {
text += ` ${key} = ${value}\n`;
});
text += '\n';
}
// Functions
if (this.options.showFunctions && this.model.functions.size > 0) {
text += 'Functions:\n';
this.model.functions.forEach((mapping, functionName) => {
text += ` ${functionName}:\n`;
mapping.forEach((output, input) => {
text += ` ${input} ↦ ${output}\n`;
});
text += '\n';
});
}
// Predicates
if (this.options.showPredicates && this.model.predicates.size > 0) {
text += 'Predicates:\n';
this.model.predicates.forEach((extension, predicateName) => {
text += ` ${predicateName}:\n`;
if (extension.size > 0) {
text += ' { ' + Array.from(extension).join(', ') + ' }\n';
} else {
text += ' ∅ (empty set)\n';
}
text += '\n';
});
}
return text;
}
/**
* Get color for domain element based on index
* @param index Element index
* @returns Color string
*/
private getElementColor(index: number): string {
if (this.options.colorScheme === 'monochrome') {
const gray = Math.floor(255 - (index * 40) % 200);
return `rgb(${gray}, ${gray}, ${gray})`;
} else if (this.options.colorScheme === 'colorblind') {
const colors = ['#0072B2', '#009E73', '#D55E00', '#CC79A7', '#F0E442'];
return colors[index % colors.length];
} else {
// Default color scheme
const hue = (index * 360 / 12) % 360;
return `hsl(${hue}, 70%, 50%)`;
}
}
/**
* Evaluate a formula in this model (simplified)
* @param formula Formula to evaluate
* @param assignment Variable assignment
* @returns Boolean value
*/
evaluateFormula(formula: PredicateFormula, assignment: Map<string, string>): boolean {
// This is a simplified implementation for demonstration
// A full implementation would need to handle all cases recursively
switch (formula.type) {
case 'predicate':
const predicateExtension = this.model.predicates.get(formula.name);
if (!predicateExtension) return false;
// Simple tuple string representation for now
const tuple = formula.args.map(arg =>
arg.type === 'variable' ? assignment.get(arg.name) || '' :
arg.type === 'constant' ? arg.name : ''
).join(',');
return predicateExtension.has(tuple);
default:
// For other formula types, return true as placeholder
return true;
}
}
/**
* Find a model that satisfies a formula (simplified)
* @param formula Formula to satisfy
* @returns Model if found, null otherwise
*/
static findModel(formula: PredicateFormula): PredicateModel | null {
// This is a placeholder for model finding algorithm
// A full implementation would be much more complex
const domain = ['a', 'b', 'c'];
const constants = new Map<string, string>();
const functions = new Map<string, Map<string, string>>();
const predicates = new Map<string, Set<string>>();
// Extract predicates from formula and create empty extensions
const extractedPredicates = this.extractPredicates(formula);
extractedPredicates.forEach(pred => {
predicates.set(pred, new Set<string>());
});
return {
domain,
constants,
functions,
predicates
};
}
/**
* Extract predicate names from a formula
* @param formula Formula to analyze
* @returns Array of predicate names
*/
private static extractPredicates(formula: PredicateFormula): string[] {
const predicates: string[] = [];
const extract = (f: PredicateFormula): void => {
if (f.type === 'predicate') {
if (!predicates.includes(f.name)) {
predicates.push(f.name);
}
} else if (f.type === 'unary') {
extract(f.operand);
} else if (f.type === 'binary') {
extract(f.left);
extract(f.right);
} else if (f.type === 'quantified') {
extract(f.formula);
}
};
extract(formula);
return predicates;
}
}
