Spaces:
Sleeping
Sleeping
""" | |
Gradio application for SFOSR (Semantic Formal Ontology Structure Representation) System. | |
Provides an interface to analyze, verify, and construct proofs using the SFOSR framework. | |
""" | |
import gradio as gr | |
import json | |
import os | |
from sfosr_core.sfosr_system import SFOSRSystem # Assuming sfosr_system.py is in sfosr_core | |
# --- Configuration --- | |
DB_PATH = "sfosr.db" # Assumes the database is in the root directory | |
# Check if DB exists, otherwise handle appropriately (e.g., log an error) | |
if not os.path.exists(DB_PATH): | |
print(f"Error: Database file not found at {DB_PATH}. Please ensure it exists.") | |
# In a real scenario, you might want to exit or provide a way to upload/create it. | |
sfosr_instance = None # Indicate that the system is not ready | |
else: | |
# --- Initialize SFOSR System --- | |
try: | |
sfosr_instance = SFOSRSystem(db_path=DB_PATH) | |
print("SFOSR System initialized successfully.") | |
except Exception as e: | |
print(f"Error initializing SFOSR System: {e}") | |
sfosr_instance = None # Indicate that the system failed to initialize | |
# --- Helper Functions for Gradio --- | |
def handle_system_unavailable(): | |
"""Returns an error message if the SFOSR system isn't ready.""" | |
return "SFOSR System is not available. Please check server logs.", "", "", "" | |
def process_input_json(json_string): | |
"""Safely parse input JSON string.""" | |
if not json_string: | |
return None, "Input JSON cannot be empty." | |
try: | |
data = json.loads(json_string) | |
if not isinstance(data, dict): | |
return None, "Input must be a valid JSON object (dictionary)." | |
if "vectors" not in data or not isinstance(data["vectors"], list): | |
return None, "Input JSON must contain a 'vectors' key with a list of vectors." | |
# Add more validation as needed (e.g., text key) | |
return data, None | |
except json.JSONDecodeError as e: | |
return None, f"Invalid JSON format: {e}" | |
except Exception as e: | |
return None, f"Error processing input: {e}" | |
def run_analysis_verification(input_json_str): | |
"""Gradio function to run analysis and verification.""" | |
if sfosr_instance is None: | |
return handle_system_unavailable() | |
input_data, error = process_input_json(input_json_str) | |
if error: | |
return f"Input Error: {error}", "", "", "" | |
try: | |
# Use the main process method which handles both analysis and verification | |
result = sfosr_instance.process(input_data) | |
# Format the output | |
analysis_summary = f"**Analysis Status:** {result.get('analysis', {}).get('status', 'N/A')}\n" \ | |
f"**Compilable:** {result.get('analysis', {}).get('is_compilable', 'N/A')}\n" \ | |
f"**Graph Metrics:** {result.get('analysis', {}).get('graph_metrics', {})}" | |
verification_summary = f"**Total Vectors Processed:** {result.get('verification', {}).get('total_vectors', 0)}\n" \ | |
f"**Valid Vectors:** {result.get('verification', {}).get('valid_count', 0)}\n" \ | |
f"**Compliance Rate:** {result.get('verification', {}).get('compliance_rate', 0.0):.2f}" | |
vector_details = result.get('verification', {}).get('vectors_data', {}) | |
# Optional: Add graph visualization logic here later | |
graph_output = "Graph visualization placeholder" | |
return analysis_summary, verification_summary, vector_details, graph_output | |
except Exception as e: | |
print(f"Error during SFOSR processing: {e}") # Log for debugging | |
return f"An error occurred: {e}", "", "", "" | |
def run_proof_construction(input_json_str, source_concept, target_concept): | |
"""Gradio function to run proof construction.""" | |
if sfosr_instance is None: | |
return handle_system_unavailable()[:1] + ("",) # Only return one value for proof status | |
input_data, error = process_input_json(input_json_str) | |
if error: | |
return f"Input Error: {error}", "" | |
if not source_concept or not target_concept: | |
return "Source and Target concepts cannot be empty.", "" | |
# Add the proof query to the input data | |
input_data["proof_query"] = { | |
"source": source_concept, | |
"target": target_concept | |
} | |
try: | |
# Use the main process method - it includes proof if query exists | |
result = sfosr_instance.process(input_data) | |
proof_result = result.get("proof") | |
if not proof_result: | |
# This might happen if the process function structure changes or proof wasn't run | |
return "Proof was not attempted or failed silently.", "" | |
proof_status = f"**Proof Status:** {proof_result.get('status', 'N/A')}\n" \ | |
f"**Is Valid:** {proof_result.get('is_valid', 'N/A')}" | |
if proof_result.get('reason'): | |
proof_status += f"\n**Reason:** {proof_result.get('reason')}" | |
proof_details = proof_result # Return the whole proof structure for now | |
return proof_status, proof_details | |
except Exception as e: | |
print(f"Error during SFOSR proof: {e}") # Log for debugging | |
return f"An error occurred: {e}", "" | |
# --- Gradio Interface Definition --- | |
with gr.Blocks(theme=gr.themes.Soft()) as demo: | |
gr.Markdown( | |
""" | |
# SFOSR: Semantic Formal Ontology Structure Representation | |
Interact with the SFOSR system to analyze, verify semantic structures, | |
and construct formal proofs based on input vectors. | |
Provide input data in the specified JSON format. | |
[Link to GitHub Repo - Placeholder] | |
""" | |
) | |
with gr.Tabs(): | |
with gr.TabItem("Analyze & Verify"): | |
with gr.Row(): | |
with gr.Column(scale=1): | |
gr.Markdown("### Input Data (JSON)") | |
input_json_av = gr.Textbox( | |
lines=15, | |
label="SFOSR JSON Input", | |
info="Paste the JSON containing 'text' (optional) and 'vectors' (required list).", | |
placeholder='{\n "text": "Example context...",\n "vectors": [\n {\n "id": "V1",\n "source": "ConceptA",\n "target": "ConceptB",\n "type": "Causality",\n "axis": "relationship",\n "justification": "A causes B based on evidence X."\n }\n // ... more vectors\n ],\n "instance_definitions": {\n "Inst1": {"is_a": "ConceptA", "label": "My Instance"}\n }\n}' | |
) | |
av_button = gr.Button("Run Analysis & Verification", variant="primary") | |
with gr.Column(scale=1): | |
gr.Markdown("### Analysis Summary") | |
analysis_output = gr.Markdown() | |
gr.Markdown("### Verification Summary") | |
verification_output = gr.Markdown() | |
gr.Markdown("### Vector Verification Details") | |
vector_details_output = gr.JSON(label="Vector Details") | |
gr.Markdown("### Concept Graph (Placeholder)") | |
graph_placeholder_output = gr.Textbox(label="Graph Info") # Placeholder | |
# Add examples later using gr.Examples | |
# gr.Examples( | |
# examples=[ | |
# [sample_json_1], | |
# [sample_json_2] | |
# ], | |
# inputs=input_json_av | |
# ) | |
with gr.TabItem("Construct Proof"): | |
with gr.Row(): | |
with gr.Column(scale=1): | |
gr.Markdown("### Input Data & Query (JSON)") | |
input_json_p = gr.Textbox( | |
lines=10, | |
label="SFOSR JSON Context", | |
info="Paste the JSON containing 'vectors' to be used as premises.", | |
placeholder='{\n "vectors": [\n {\n "id": "V1", "source": "A", "target": "B", "type": "Implication", "axis": "logic", "is_valid": true \n },\n {\n "id": "V2", "source": "B", "target": "C", "type": "Implication", "axis": "logic", "is_valid": true \n }\n ]\n}' | |
) | |
source_concept_input = gr.Textbox(label="Source Concept", info="The starting concept for the proof.") | |
target_concept_input = gr.Textbox(label="Target Concept", info="The concept to prove reachability for.") | |
p_button = gr.Button("Find Proof", variant="primary") | |
with gr.Column(scale=1): | |
gr.Markdown("### Proof Result") | |
proof_status_output = gr.Markdown() | |
gr.Markdown("### Proof Details / Path") | |
proof_details_output = gr.JSON(label="Proof Structure") | |
# Add examples later using gr.Examples | |
# --- Event Handlers --- | |
if sfosr_instance: # Only wire up buttons if the system initialized | |
av_button.click( | |
fn=run_analysis_verification, | |
inputs=[input_json_av], | |
outputs=[analysis_output, verification_output, vector_details_output, graph_placeholder_output] | |
) | |
p_button.click( | |
fn=run_proof_construction, | |
inputs=[input_json_p, source_concept_input, target_concept_input], | |
outputs=[proof_status_output, proof_details_output] | |
) | |
else: | |
# Display a persistent error if the system couldn't load | |
gr.Markdown("**Error: SFOSR System failed to initialize. Cannot run operations. Check logs.**") | |
# --- Launch the App --- | |
if __name__ == "__main__": | |
demo.launch() # Share=True for public link if needed |