{% extends "base.html" %}

{% block title %}验证结果 - 形式化程序规范生成系统{% endblock %}

{% block content %}
<div class="results-container">
    <div class="results-header">
        <h1><i class="fas fa-chart-line"></i> 验证结果</h1>
        <div class="file-info">
            <span class="file-name">{{ uploaded_file.filename }}</span>
            <span class="file-size">{{ (uploaded_file.size / 1024) | round(2) }} KB</span>
            <a href="{{ url_for('upload_page') }}" class="btn btn-secondary">
                <i class="fas fa-plus"></i> 上传新文件
            </a>
        </div>
    </div>

    <!-- Results Summary -->
    <div class="results-summary">
        <div class="summary-cards">
            <div class="summary-card">
                <div class="card-icon success">
                    <i class="fas fa-check-circle"></i>
                </div>
                <div class="card-content">
                    <h3>解析成功</h3>
                    <p class="card-value">3 个函数</p>
                    <p class="card-detail">函数签名提取完成</p>
                </div>
            </div>

            <div class="summary-card">
                <div class="card-icon warning">
                    <i class="fas fa-exclamation-triangle"></i>
                </div>
                <div class="card-content">
                    <h3>验证状态</h3>
                    <p class="card-value">部分通过</p>
                    <p class="card-detail">2/3 断言验证成功</p>
                </div>
            </div>

            <div class="summary-card">
                <div class="card-icon info">
                    <i class="fas fa-code-branch"></i>
                </div>
                <div class="card-content">
                    <h3>变异测试</h3>
                    <p class="card-value">85%</p>
                    <p class="card-detail">规范稳定性评分</p>
                </div>
            </div>

            <div class="summary-card">
                <div class="card-icon primary">
                    <i class="fas fa-clock"></i>
                </div>
                <div class="card-content">
                    <h3>处理时间</h3>
                    <p class="card-value">12.5s</p>
                    <p class="card-detail">总耗时</p>
                </div>
            </div>
        </div>
    </div>

    <!-- Detailed Results Tabs -->
    <div class="results-tabs">
        <div class="tabs-container">
            <button class="tab-button active" onclick="showResultsTab(event, 'parsing')">
                <i class="fas fa-code"></i> 解析结果
            </button>
            <button class="tab-button" onclick="showResultsTab(event, 'specification')">
                <i class="fas fa-file-alt"></i> 生成规范
            </button>
            <button class="tab-button" onclick="showResultsTab(event, 'verification')">
                <i class="fas fa-shield-alt"></i> 验证结果
            </button>
            <button class="tab-button" onclick="showResultsTab(event, 'mutation')">
                <i class="fas fa-dna"></i> 变异测试
            </button>
            <button class="tab-button" onclick="showResultsTab(event, 'quality')">
                <i class="fas fa-star"></i> 质量评估
            </button>
        </div>
    </div>

    <!-- Tab Contents -->
    <div class="tab-contents">

        <!-- Parsing Results Tab -->
        <div id="parsing-tab" class="tab-content active">
            <div class="parsing-results">
                <h3>代码解析结果</h3>

                <div class="function-list">
                    {% for func in results.functions %}
                    <div class="function-item">
                        <div class="function-header">
                            <h4><i class="fas fa-function"></i> {{ func.name }}</h4>
                            <span class="complexity-badge {{ 'high' if func.complexity == '高' else 'medium' if func.complexity == '中等' else 'low' }}">
                                {{ func.complexity }}复杂度
                            </span>
                        </div>
                        <div class="function-signature">
                            <code>{{ func.signature }}</code>
                        </div>
                        <div class="function-details">
                            <div class="detail-group">
                                <h5>参数</h5>
                                <ul>
                                    {% for param in func.params %}
                                    <li><code>{{ param }}</code></li>
                                    {% endfor %}
                                </ul>
                            </div>
                            <div class="detail-group">
                                <h5>返回值</h5>
                                <p><code>{{ func.return_type }}</code></p>
                            </div>
                            {% if func.issues %}
                            <div class="detail-group issues">
                                <h5>潜在问题</h5>
                                <ul class="issue-list">
                                    {% for issue in func.issues %}
                                    <li class="issue-item">
                                        <i class="fas fa-exclamation-triangle warning"></i>
                                        {{ issue }}
                                    </li>
                                    {% endfor %}
                                </ul>
                            </div>
                            {% endif %}
                        </div>
                    </div>
                    {% endfor %}
                </div>
            </div>
        </div>

        <!-- Specification Results Tab -->
        <div id="specification-tab" class="tab-content">
            <div class="specification-results">
                <h3>生成的形式化规范</h3>

                <div class="spec-functions">
                    <div class="spec-function">
                        <div class="spec-header">
                            <h4>生成的形式化规范</h4>
                            <span class="spec-status success">
                                <i class="fas fa-check-circle"></i> 生成成功
                            </span>
                        </div>
                        <div class="spec-content">
                            <h5>前置条件 (Preconditions)</h5>
                            <pre><code class="language-c">{% for req in results.specification.preconditions %}
{{ req }}{% endfor %}</code></pre>

                            <h5>后置条件 (Postconditions)</h5>
                            <pre><code class="language-c">{% for ens in results.specification.postconditions %}
{{ ens }}{% endfor %}</code></pre>
                        </div>
                        <div class="spec-analysis">
                            <div class="analysis-item">
                                <span class="analysis-label">规范类型:</span>
                                <span>函数契约</span>
                            </div>
                            <div class="analysis-item">
                                <span class="analysis-label">前置条件:</span>
                                <span>{{ results.specification.preconditions|length }} 项</span>
                            </div>
                            <div class="analysis-item">
                                <span class="analysis-label">后置条件:</span>
                                <span>{{ results.specification.postconditions|length }} 项</span>
                            </div>
                        </div>
                    </div>

                </div>
            </div>
        </div>

        <!-- Verification Results Tab -->
        <div id="verification-tab" class="tab-content">
            <div class="verification-results">
                <h3>CBMC 验证结果</h3>

                <div class="verification-summary">
                    <div class="verification-stats">
                        <div class="stat-item">
                            <div class="stat-number">{{ results.specification.assertions|length }}</div>
                            <div class="stat-label">总断言数</div>
                        </div>
                        <div class="stat-item">
                            <div class="stat-number success">{{ results.specification.assertions|selectattr('status', 'equalto', 'PASS')|list|length }}</div>
                            <div class="stat-label">验证成功</div>
                        </div>
                        <div class="stat-item">
                            <div class="stat-number warning">{{ results.specification.assertions|selectattr('status', 'equalto', 'PARTIAL')|list|length }}</div>
                            <div class="stat-label">待确认</div>
                        </div>
                        <div class="stat-item">
                            <div class="stat-number danger">{{ results.specification.assertions|selectattr('status', 'equalto', 'FAIL')|list|length }}</div>
                            <div class="stat-label">验证失败</div>
                        </div>
                    </div>
                </div>

                <div class="verification-details">
                    <div class="verification-function">
                        <h4>验证断言结果</h4>
                        {% for assertion in results.specification.assertions %}
                        <div class="verification-item {{ 'success' if assertion.status == 'PASS' else 'danger' if assertion.status == 'FAIL' else 'warning' }}">
                            <div class="verification-status">
                                <i class="fas fa-{% if assertion.status == 'PASS' %}check-circle{% elif assertion.status == 'FAIL' %}times-circle{% else %}exclamation-triangle{% endif %}"></i>
                                {{ assertion.status }}
                            </div>
                            <div class="verification-description">
                                <strong>行 {{ assertion.line }}:</strong> {{ assertion.condition }}
                                <br>
                                <small>{{ assertion.message }}</small>
                            </div>
                        </div>
                        {% endfor %}
                    </div>
                </div>
            </div>
        </div>

        <!-- Mutation Testing Tab -->
        <div id="mutation-tab" class="tab-content">
            <div class="mutation-results">
                <h3>变异测试结果</h3>

                <div class="mutation-overview">
                    <div class="overview-cards">
                        <div class="overview-card">
                            <div class="card-value">15</div>
                            <div class="card-label">总变异数</div>
                        </div>
                        <div class="overview-card">
                            <div class="card-value success">13</div>
                            <div class="card-label">检测到的变异</div>
                        </div>
                        <div class="overview-card">
                            <div class="card-value warning">2</div>
                            <div class="card-label">存活变异</div>
                        </div>
                        <div class="overview-card">
                            <div class="card-value primary">86.7%</div>
                            <div class="card-label">变异得分</div>
                        </div>
                    </div>
                </div>

                <div class="mutation-details">
                    <div class="mutation-type">
                        <h4>谓词变异</h4>
                        <div class="mutation-item detected">
                            <div class="mutation-status">
                                <i class="fas fa-check-circle"></i> 已检测
                            </div>
                            <div class="mutation-description">
                                \forall -> \exists 变异被检测到
                            </div>
                        </div>
                        <div class="mutation-item survived">
                            <div class="mutation-status">
                                <i class="fas fa-times-circle"></i> 存活
                            </div>
                            <div class="mutation-description">
                                存在量词变异未被检测
                            </div>
                        </div>
                    </div>

                    <div class="mutation-type">
                        <h4>边界变异</h4>
                        <div class="mutation-item detected">
                            <div class="mutation-status">
                                <i class="fas fa-check-circle"></i> 已检测
                            </div>
                            <div class="mutation-description">
                                < -> <= 边界变异被检测
                            </div>
                        </div>
                        <div class="mutation-item detected">
                            <div class="mutation-status">
                                <i class="fas fa-check-circle"></i> 已检测
                            </div>
                            <div class="mutation-description">
                                > -> >= 边界变异被检测
                            </div>
                        </div>
                    </div>

                    <div class="mutation-type">
                        <h4>逻辑变异</h4>
                        <div class="mutation-item detected">
                            <div class="mutation-status">
                                <i class="fas fa-check-circle"></i> 已检测
                            </div>
                            <div class="mutation-description">
                                && -> || 逻辑变异被检测
                            </div>
                        </div>
                    </div>
                </div>
            </div>
        </div>

        <!-- Quality Assessment Tab -->
        <div id="quality-tab" class="tab-content">
            <div class="quality-results">
                <h3>质量评估报告</h3>

                <div class="quality-summary">
                    <div class="quality-score">
                        <div class="score-circle">
                            <div class="score-value">85</div>
                            <div class="score-label">综合评分</div>
                        </div>
                    </div>
                    <div class="quality-metrics">
                        <div class="metric">
                            <div class="metric-header">
                                <span class="metric-name">准确性</span>
                                <span class="metric-value">88%</span>
                            </div>
                            <div class="metric-bar">
                                <div class="metric-fill" style="width: 88%"></div>
                            </div>
                        </div>
                        <div class="metric">
                            <div class="metric-header">
                                <span class="metric-name">完整性</span>
                                <span class="metric-value">82%</span>
                            </div>
                            <div class="metric-bar">
                                <div class="metric-fill" style="width: 82%"></div>
                            </div>
                        </div>
                        <div class="metric">
                            <div class="metric-header">
                                <span class="metric-name">可验证性</span>
                                <span class="metric-value">91%</span>
                            </div>
                            <div class="metric-bar">
                                <div class="metric-fill" style="width: 91%"></div>
                            </div>
                        </div>
                        <div class="metric">
                            <div class="metric-header">
                                <span class="metric-name">稳定性</span>
                                <span class="metric-value">86%</span>
                            </div>
                            <div class="metric-bar">
                                <div class="metric-fill" style="width: 86%"></div>
                            </div>
                        </div>
                    </div>
                </div>

                <div class="quality-recommendations">
                    <h4>改进建议</h4>
                    <div class="recommendations-list">
                        <div class="recommendation-item">
                            <div class="recommendation-icon">
                                <i class="fas fa-lightbulb"></i>
                            </div>
                            <div class="recommendation-content">
                                <h5>增强边界条件处理</h5>
                                <p>建议添加更精确的边界条件检查，特别是对于指针操作的边界情况</p>
                            </div>
                        </div>
                        <div class="recommendation-item">
                            <div class="recommendation-icon">
                                <i class="fas fa-exclamation-circle"></i>
                            </div>
                            <div class="recommendation-content">
                                <h5>完善空指针检查</h5>
                                <p>当前规范对空指针的检查不够全面，建议增加更严格的验证条件</p>
                            </div>
                        </div>
                        <div class="recommendation-item">
                            <div class="recommendation-icon">
                                <i class="fas fa-check-double"></i>
                            </div>
                            <div class="recommendation-content">
                                <h5>优化循环不变式</h5>
                                <p>生成的循环不变式可以进一步优化，提高验证效率</p>
                            </div>
                        </div>
                    </div>
                </div>
            </div>
        </div>
    </div>

    <!-- Export Options -->
    <div class="export-section">
        <h3>导出选项</h3>
        <div class="export-buttons">
            <button class="btn btn-primary" onclick="exportResults(event, 'pdf')">
                <i class="fas fa-file-pdf"></i> 导出 PDF 报告
            </button>
            <button class="btn btn-primary" onclick="exportResults(event, 'json')">
                <i class="fas fa-file-code"></i> 导出 JSON 数据
            </button>
            <button class="btn btn-secondary" onclick="exportResults(event, 'xml')">
                <i class="fas fa-file-code"></i> 导出 XML 格式
            </button>
            <button class="btn btn-secondary" onclick="exportResults(event, 'txt')">
                <i class="fas fa-file-alt"></i> 导出文本报告
            </button>
        </div>
    </div>
</div>

<script>
function showResultsTab(e, tabName) {
    // Hide all tabs
    document.querySelectorAll('.tab-content').forEach(content => {
        content.classList.remove('active');
    });

    // Remove active class from all buttons
    document.querySelectorAll('.tab-button').forEach(button => {
        button.classList.remove('active');
    });

    // Show selected tab
    document.getElementById(tabName + '-tab').classList.add('active');
    e.target.classList.add('active');

    // Re-run syntax highlighting
    Prism.highlightAll();
}

function exportResults(e, format) {
    // Simulate export functionality
    alert(`正在导出 ${format.toUpperCase()} 格式的报告...`);

    // In a real implementation, this would make an API call to generate and download the report
    setTimeout(() => {
        alert(`${format.toUpperCase()} 报告导出完成！`);
    }, 1500);
}

// Initialize the page
document.addEventListener('DOMContentLoaded', function() {
    // Add smooth scrolling
    document.querySelectorAll('a[href^="#"]').forEach(anchor => {
        anchor.addEventListener('click', function (e) {
            e.preventDefault();
            document.querySelector(this.getAttribute('href')).scrollIntoView({
                behavior: 'smooth'
            });
        });
    });

    // Initialize syntax highlighting
    Prism.highlightAll();
});
</script>
{% endblock %}

{% block extra_css %}
<style>
.results-container {
    max-width: 1400px;
    margin: 0 auto;
    padding: 40px 20px;
}

.results-header {
    display: flex;
    justify-content: space-between;
    align-items: center;
    margin-bottom: 40px;
    padding-bottom: 20px;
    border-bottom: 2px solid #e9ecef;
}

.results-header h1 {
    font-size: 2.5rem;
    color: #333;
    margin: 0;
}

.file-info {
    display: flex;
    align-items: center;
    gap: 15px;
}

.file-name {
    font-weight: bold;
    color: #333;
}

.file-size {
    color: #666;
    font-size: 0.9rem;
}

.results-summary {
    margin-bottom: 40px;
}

.summary-cards {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(250px, 1fr));
    gap: 20px;
}

.summary-card {
    background: white;
    padding: 25px;
    border-radius: 10px;
    box-shadow: 0 2px 8px rgba(0,0,0,0.1);
    display: flex;
    align-items: center;
    gap: 20px;
}

.card-icon {
    width: 60px;
    height: 60px;
    border-radius: 50%;
    display: flex;
    align-items: center;
    justify-content: center;
    font-size: 1.5rem;
}

.card-icon.success { background: #d4edda; color: #28a745; }
.card-icon.warning { background: #fff3cd; color: #ffc107; }
.card-icon.info { background: #d1ecf1; color: #17a2b8; }
.card-icon.primary { background: #d4d4f8; color: #667eea; }

.card-content h3 {
    margin: 0 0 5px 0;
    font-size: 1.1rem;
    color: #333;
}

.card-value {
    font-size: 1.5rem;
    font-weight: bold;
    color: #333;
    margin: 5px 0;
}

.card-detail {
    color: #666;
    font-size: 0.9rem;
    margin: 0;
}

.results-tabs {
    margin-bottom: 30px;
}

.tabs-container {
    display: flex;
    background: #f8f9fa;
    border-radius: 10px;
    padding: 5px;
    gap: 5px;
}

.tab-button {
    background: none;
    border: none;
    padding: 15px 25px;
    border-radius: 8px;
    cursor: pointer;
    font-size: 1rem;
    color: #666;
    transition: all 0.3s ease;
    display: flex;
    align-items: center;
    gap: 8px;
}

.tab-button.active {
    background: #667eea;
    color: white;
}

.tab-button:hover:not(.active) {
    background: #e9ecef;
}

.tab-contents {
    background: white;
    border-radius: 10px;
    box-shadow: 0 2px 8px rgba(0,0,0,0.1);
    overflow: hidden;
}

.tab-content {
    display: none;
    padding: 30px;
}

.tab-content.active {
    display: block;
}

/* Parsing Results Styles */
.function-list {
    display: grid;
    gap: 25px;
}

.function-item {
    background: #f8f9fa;
    border-radius: 10px;
    padding: 25px;
    border-left: 4px solid #667eea;
}

.function-header {
    display: flex;
    justify-content: space-between;
    align-items: center;
    margin-bottom: 15px;
}

.function-header h4 {
    margin: 0;
    color: #333;
    display: flex;
    align-items: center;
    gap: 10px;
}

.function-location {
    color: #666;
    font-size: 0.9rem;
}

.function-signature {
    background: #fff;
    padding: 15px;
    border-radius: 5px;
    font-family: 'Courier New', monospace;
    margin-bottom: 15px;
}

.function-details {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(200px, 1fr));
    gap: 20px;
}

.detail-group h5 {
    margin: 0 0 10px 0;
    color: #333;
    font-size: 1rem;
}

.detail-group ul {
    margin: 0;
    padding-left: 20px;
}

.detail-group li {
    margin-bottom: 5px;
    color: #666;
}

/* Specification Results Styles */
.spec-functions {
    display: grid;
    gap: 30px;
}

.spec-function {
    background: #f8f9fa;
    border-radius: 10px;
    overflow: hidden;
}

.spec-header {
    background: #fff;
    padding: 20px;
    border-bottom: 1px solid #e9ecef;
    display: flex;
    justify-content: space-between;
    align-items: center;
}

.spec-header h4 {
    margin: 0;
    color: #333;
}

.spec-status {
    display: flex;
    align-items: center;
    gap: 5px;
    font-weight: bold;
}

.spec-status.success { color: #28a745; }
.spec-status.warning { color: #ffc107; }

.spec-content {
    padding: 20px;
    background: #fff;
}

.spec-analysis {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(150px, 1fr));
    gap: 15px;
    padding: 20px;
    background: #f8f9fa;
}

.analysis-item {
    text-align: center;
}

.analysis-label {
    font-weight: bold;
    color: #333;
    display: block;
    margin-bottom: 5px;
}

/* Verification Results Styles */
.verification-summary {
    margin-bottom: 30px;
}

.verification-stats {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(150px, 1fr));
    gap: 20px;
}

.stat-item {
    text-align: center;
    padding: 20px;
    background: #f8f9fa;
    border-radius: 10px;
}

.stat-number {
    font-size: 2rem;
    font-weight: bold;
    margin-bottom: 5px;
}

.stat-number.success { color: #28a745; }
.stat-number.warning { color: #ffc107; }
.stat-number.danger { color: #dc3545; }

.stat-label {
    color: #666;
    font-size: 0.9rem;
}

.verification-details {
    display: grid;
    gap: 25px;
}

.verification-function h4 {
    margin: 0 0 15px 0;
    color: #333;
}

.verification-item {
    display: flex;
    align-items: center;
    gap: 15px;
    padding: 15px;
    background: #f8f9fa;
    border-radius: 8px;
    margin-bottom: 10px;
}

.verification-item.success { border-left: 4px solid #28a745; }
.verification-item.warning { border-left: 4px solid #ffc107; }

.verification-status {
    font-weight: bold;
}

.verification-description {
    flex: 1;
    color: #333;
}

.verification-time {
    color: #666;
    font-size: 0.9rem;
}

/* Mutation Testing Styles */
.mutation-overview {
    margin-bottom: 30px;
}

.overview-cards {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(150px, 1fr));
    gap: 15px;
}

.overview-card {
    text-align: center;
    padding: 20px;
    background: #f8f9fa;
    border-radius: 10px;
}

.overview-card .card-value {
    font-size: 1.8rem;
    font-weight: bold;
    margin-bottom: 5px;
}

.card-value.success { color: #28a745; }
.card-value.warning { color: #ffc107; }
.card-value.primary { color: #667eea; }

.mutation-details {
    display: grid;
    gap: 20px;
}

.mutation-type h4 {
    margin: 0 0 15px 0;
    color: #333;
}

.mutation-item {
    display: flex;
    align-items: center;
    gap: 15px;
    padding: 15px;
    background: #f8f9fa;
    border-radius: 8px;
    margin-bottom: 10px;
}

.mutation-item.detected { border-left: 4px solid #28a745; }
.mutation-item.survived { border-left: 4px solid #dc3545; }

.mutation-status {
    font-weight: bold;
}

.mutation-description {
    flex: 1;
    color: #333;
}

/* Quality Assessment Styles */
.quality-summary {
    display: grid;
    grid-template-columns: 1fr 2fr;
    gap: 30px;
    margin-bottom: 40px;
}

.quality-score {
    text-align: center;
    padding: 30px;
    background: #f8f9fa;
    border-radius: 10px;
}

.score-circle {
    width: 150px;
    height: 150px;
    border-radius: 50%;
    background: conic-gradient(#667eea 0deg 306deg, #e9ecef 306deg 360deg);
    display: flex;
    align-items: center;
    justify-content: center;
    margin: 0 auto 15px;
    position: relative;
}

.score-circle::before {
    content: '';
    width: 120px;
    height: 120px;
    background: white;
    border-radius: 50%;
    position: absolute;
}

.score-value {
    font-size: 2.5rem;
    font-weight: bold;
    color: #667eea;
    position: relative;
    z-index: 1;
}

.score-label {
    color: #666;
    font-weight: bold;
    position: relative;
    z-index: 1;
}

.quality-metrics {
    display: grid;
    gap: 15px;
}

.metric {
    background: #f8f9fa;
    padding: 20px;
    border-radius: 10px;
}

.metric-header {
    display: flex;
    justify-content: space-between;
    align-items: center;
    margin-bottom: 10px;
}

.metric-name {
    font-weight: bold;
    color: #333;
}

.metric-value {
    font-weight: bold;
    color: #667eea;
}

.metric-bar {
    background: #e9ecef;
    height: 8px;
    border-radius: 4px;
    overflow: hidden;
}

.metric-fill {
    height: 100%;
    background: #667eea;
    transition: width 0.3s ease;
}

.quality-recommendations h4 {
    margin: 0 0 20px 0;
    color: #333;
}

.recommendations-list {
    display: grid;
    gap: 20px;
}

.recommendation-item {
    display: flex;
    gap: 15px;
    padding: 20px;
    background: #f8f9fa;
    border-radius: 10px;
}

.recommendation-icon {
    font-size: 1.5rem;
    color: #667eea;
    flex-shrink: 0;
}

.recommendation-content h5 {
    margin: 0 0 10px 0;
    color: #333;
}

.recommendation-content p {
    margin: 0;
    color: #666;
    line-height: 1.5;
}

/* Export Section */
.export-section {
    margin-top: 40px;
    padding: 30px;
    background: #f8f9fa;
    border-radius: 10px;
}

.export-section h3 {
    margin: 0 0 20px 0;
    color: #333;
}

.export-buttons {
    display: flex;
    gap: 15px;
    flex-wrap: wrap;
}

@media (max-width: 768px) {
    .results-header {
        flex-direction: column;
        gap: 20px;
        text-align: center;
    }

    .tabs-container {
        flex-direction: column;
    }

    .quality-summary {
        grid-template-columns: 1fr;
    }

    .export-buttons {
        justify-content: center;
    }
}
</style>
{% endblock %}