{% extends "base.html" %}

{% block title %}首页 - 形式化程序规范生成系统{% endblock %}

{% block content %}
<!-- Hero Section -->
<section class="hero-section">
    <div class="hero-container">
        <div class="hero-content">
            <h1 class="hero-title">
                <i class="fas fa-shield-alt"></i>
                形式化程序规范生成系统
            </h1>
            <p class="hero-subtitle">
                基于大型语言模型的C/C++程序形式化规范自动生成与验证
            </p>
            <p class="hero-description">
                本系统集成了先进的代码解析、智能规范生成和自动化验证技术，
                为开发者提供高效、可靠的形式化验证解决方案
            </p>
            <div class="hero-actions">
                <a href="{{ url_for('workspace_page') }}" class="btn btn-primary btn-lg">
                    <i class="fas fa-rocket"></i> 进入工作空间
                </a>
                <a href="{{ url_for('upload_page') }}" class="btn btn-secondary btn-lg">
                    <i class="fas fa-upload"></i> 上传代码
                </a>
            </div>
        </div>
        <div class="hero-image">
            <i class="fas fa-code"></i>
        </div>
    </div>
</section>

<!-- Quick Start Section -->
<section class="quickstart-section">
    <div class="container">
        <h2 class="section-title">快速开始</h2>
        <div class="quickstart-steps">
            <div class="step">
                <div class="step-number">1</div>
                <div class="step-content">
                    <h3>进入工作空间</h3>
                    <p>使用统一的工作空间界面进行所有操作</p>
                </div>
            </div>
            <div class="step-arrow">
                <i class="fas fa-arrow-right"></i>
            </div>
            <div class="step">
                <div class="step-number">2</div>
                <div class="step-content">
                    <h3>导入代码</h3>
                    <p>在工作空间中上传C/C++源代码文件或直接粘贴代码</p>
                </div>
            </div>
            <div class="step-arrow">
                <i class="fas fa-arrow-right"></i>
            </div>
            <div class="step">
                <div class="step-number">3</div>
                <div class="step-content">
                    <h3>配置分析</h3>
                    <p>在工作空间中配置验证参数和工作流程</p>
                </div>
            </div>
            <div class="step-arrow">
                <i class="fas fa-arrow-right"></i>
            </div>
            <div class="step">
                <div class="step-number">4</div>
                <div class="step-content">
                    <h3>实时监控</h3>
                    <p>在工作空间中实时查看分析进度和结果</p>
                </div>
            </div>
        </div>
        <div class="quickstart-action">
            <a href="{{ url_for('workspace_page') }}" class="btn btn-primary">
                <i class="fas fa-rocket"></i> 进入工作空间
            </a>
        </div>
    </div>
</section>

<!-- Features Section -->
<section class="features-section" id="features">
    <div class="container">
        <h2 class="section-title">核心功能</h2>
        <div class="features-grid">
            <div class="feature-card">
                <div class="feature-icon">
                    <i class="fas fa-th-large"></i>
                </div>
                <h3>统一工作空间</h3>
                <p>全新的6区域工作空间界面，集成所有功能于一体</p>
                <ul class="feature-list">
                    <li>2×3网格布局设计</li>
                    <li>实时WebSocket通信</li>
                    <li>统一状态管理</li>
                </ul>
            </div>

            <div class="feature-card">
                <div class="feature-icon">
                    <i class="fas fa-brain"></i>
                </div>
                <h3>LLM规范生成</h3>
                <p>基于DeepSeek V3模型自动生成符合CBMC规范的形式化说明</p>
                <ul class="feature-list">
                    <li>自动生成requires条件</li>
                    <li>智能ensures断言</li>
                    <li>循环不变式推导</li>
                </ul>
            </div>

            <div class="feature-card">
                <div class="feature-icon">
                    <i class="fas fa-shield-alt"></i>
                </div>
                <h3>CBMC验证集成</h3>
                <p>与CBMC深度集成，提供完整的形式化验证流程</p>
                <ul class="feature-list">
                    <li>内存安全验证</li>
                    <li>边界检查</li>
                    <li>溢出检测</li>
                </ul>
            </div>

            <div class="feature-card">
                <div class="feature-icon">
                    <i class="fas fa-dna"></i>
                </div>
                <h3>变异测试评估</h3>
                <p>通过变异测试评估生成规范的质量和稳定性</p>
                <ul class="feature-list">
                    <li>谓词变异</li>
                    <li>边界变异</li>
                    <li>逻辑变异</li>
                </ul>
            </div>
        </div>
    </div>
</section>

<!-- Workspace Benefits Section -->
<section class="workspace-benefits-section">
    <div class="container">
        <h2 class="section-title">工作空间优势</h2>
        <div class="benefits-grid">
            <div class="benefit-item">
                <div class="benefit-icon">
                    <i class="fas fa-tachometer-alt"></i>
                </div>
                <h4>实时监控</h4>
                <p>通过WebSocket实时推送，即时查看分析进度和结果</p>
            </div>
            <div class="benefit-item">
                <div class="benefit-icon">
                    <i class="fas fa-cogs"></i>
                </div>
                <h4>智能配置</h4>
                <p>可视化配置界面，支持多种验证参数和策略</p>
            </div>
            <div class="benefit-item">
                <div class="benefit-icon">
                    <i class="fas fa-chart-line"></i>
                </div>
                <h4>结果可视化</h4>
                <p>多标签页展示，清晰呈现验证结果和质量评估</p>
            </div>
            <div class="benefit-item">
                <div class="benefit-icon">
                    <i class="fas fa-history"></i>
                </div>
                <h4>操作历史</h4>
                <p>完整记录所有操作，支持回溯和调试</p>
            </div>
        </div>
        <div class="workspace-cta">
            <a href="{{ url_for('workspace_page') }}" class="btn btn-primary btn-lg">
                <i class="fas fa-rocket"></i> 立即体验工作空间
            </a>
        </div>
    </div>
</section>

<!-- Technology Stack Section -->
<section class="tech-section">
    <div class="container">
        <h2 class="section-title">技术栈</h2>
        <div class="tech-grid">
            <div class="tech-item">
                <i class="fab fa-python"></i>
                <h4>Python</h4>
                <p>核心开发语言</p>
            </div>
            <div class="tech-item">
                <i class="fas fa-flask"></i>
                <h4>Flask</h4>
                <p>Web框架</p>
            </div>
            <div class="tech-item">
                <i class="fas fa-robot"></i>
                <h4>DeepSeek V3</h4>
                <p>大语言模型</p>
            </div>
            <div class="tech-item">
                <i class="fas fa-cogs"></i>
                <h4>CBMC</h4>
                <p>验证工具</p>
            </div>
            <div class="tech-item">
                <i class="fas fa-file-code"></i>
                <h4>Clang</h4>
                <p>代码解析</p>
            </div>
            <div class="tech-item">
                <i class="fas fa-chart-line"></i>
                <h4>变异测试</h4>
                <p>质量评估</p>
            </div>
        </div>
    </div>
</section>

<!-- System Status Section -->
<section class="status-section">
    <div class="container">
        <h2 class="section-title">系统状态</h2>
        <div class="status-grid">
            <div class="status-item">
                <div class="status-indicator">
                    <i class="fas fa-circle text-success"></i>
                    <span class="status-text">Web服务</span>
                </div>
                <p class="status-detail">正常运行</p>
            </div>
            <div class="status-item">
                <div class="status-indicator">
                    <i class="fas fa-circle text-success"></i>
                    <span class="status-text">解析器</span>
                </div>
                <p class="status-detail">就绪</p>
            </div>
            <div class="status-item">
                <div class="status-indicator">
                    <i class="fas fa-circle text-warning"></i>
                    <span class="status-text">LLM服务</span>
                </div>
                <p class="status-detail">配置中</p>
            </div>
            <div class="status-item">
                <div class="status-indicator">
                    <i class="fas fa-circle text-success"></i>
                    <span class="status-text">CBMC验证</span>
                </div>
                <p class="status-detail">就绪</p>
            </div>
        </div>
    </div>
</section>
{% endblock %}

{% block extra_css %}
<style>
.hero-section {
    background: linear-gradient(135deg, #667eea 0%, #764ba2 100%);
    color: white;
    padding: 80px 0;
}

.hero-container {
    max-width: 1200px;
    margin: 0 auto;
    display: grid;
    grid-template-columns: 1fr 1fr;
    gap: 60px;
    align-items: center;
}

.hero-title {
    font-size: 3rem;
    font-weight: bold;
    margin-bottom: 20px;
}

.hero-subtitle {
    font-size: 1.5rem;
    margin-bottom: 20px;
    opacity: 0.9;
}

.hero-description {
    font-size: 1.1rem;
    margin-bottom: 30px;
    opacity: 0.8;
    line-height: 1.6;
}

.hero-actions {
    display: flex;
    gap: 20px;
}

.hero-image {
    text-align: center;
}

.hero-image i {
    font-size: 15rem;
    opacity: 0.8;
}

.quickstart-section {
    background: #f8f9fa;
    padding: 60px 0;
}

.quickstart-steps {
    display: flex;
    justify-content: space-between;
    align-items: center;
    margin: 40px 0;
    max-width: 1000px;
    margin-left: auto;
    margin-right: auto;
}

.step {
    background: white;
    padding: 30px;
    border-radius: 10px;
    box-shadow: 0 4px 6px rgba(0,0,0,0.1);
    text-align: center;
    width: 180px;
}

.step-number {
    background: #667eea;
    color: white;
    width: 50px;
    height: 50px;
    border-radius: 50%;
    display: flex;
    align-items: center;
    justify-content: center;
    font-size: 1.5rem;
    font-weight: bold;
    margin: 0 auto 20px;
}

.step-arrow {
    color: #667eea;
    font-size: 2rem;
}

.features-section {
    padding: 80px 0;
}

.features-grid {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(300px, 1fr));
    gap: 30px;
    margin-top: 40px;
}

.feature-card {
    background: white;
    padding: 40px 30px;
    border-radius: 10px;
    box-shadow: 0 4px 6px rgba(0,0,0,0.1);
    text-align: center;
    transition: transform 0.3s ease;
}

.feature-card:hover {
    transform: translateY(-5px);
}

.feature-icon {
    font-size: 3rem;
    color: #667eea;
    margin-bottom: 20px;
}

.feature-list {
    list-style: none;
    padding: 0;
    margin-top: 20px;
    text-align: left;
}

.feature-list li {
    padding: 5px 0;
    position: relative;
    padding-left: 20px;
}

.feature-list li:before {
    content: "✓";
    position: absolute;
    left: 0;
    color: #28a745;
    font-weight: bold;
}

.tech-section {
    background: #f8f9fa;
    padding: 60px 0;
}

.tech-grid {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(150px, 1fr));
    gap: 30px;
    margin-top: 40px;
}

.tech-item {
    text-align: center;
    padding: 30px;
    background: white;
    border-radius: 10px;
    box-shadow: 0 2px 4px rgba(0,0,0,0.1);
}

.tech-item i {
    font-size: 3rem;
    color: #667eea;
    margin-bottom: 15px;
}

.status-section {
    padding: 60px 0;
}

.status-grid {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(200px, 1fr));
    gap: 30px;
    margin-top: 40px;
}

.status-item {
    background: white;
    padding: 30px;
    border-radius: 10px;
    box-shadow: 0 2px 4px rgba(0,0,0,0.1);
    text-align: center;
}

.status-indicator {
    display: flex;
    align-items: center;
    justify-content: center;
    gap: 10px;
    margin-bottom: 10px;
}

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

.workspace-benefits-section {
    background: #f8f9fa;
    padding: 80px 0;
}

.benefits-grid {
    display: grid;
    grid-template-columns: repeat(auto-fit, minmax(250px, 1fr));
    gap: 30px;
    margin: 40px 0;
}

.benefit-item {
    background: white;
    padding: 40px 30px;
    border-radius: 12px;
    box-shadow: 0 4px 12px rgba(0,0,0,0.1);
    text-align: center;
    transition: transform 0.3s ease;
}

.benefit-item:hover {
    transform: translateY(-5px);
}

.benefit-icon {
    font-size: 2.5rem;
    color: #667eea;
    margin-bottom: 20px;
}

.benefit-item h4 {
    color: #333;
    margin-bottom: 15px;
    font-size: 1.2rem;
}

.benefit-item p {
    color: #666;
    line-height: 1.6;
}

.workspace-cta {
    text-align: center;
    margin-top: 50px;
}

@media (max-width: 768px) {
    .hero-container {
        grid-template-columns: 1fr;
        text-align: center;
    }

    .hero-title {
        font-size: 2rem;
    }

    .quickstart-steps {
        flex-direction: column;
        gap: 20px;
    }

    .step-arrow {
        transform: rotate(90deg);
    }

    .hero-actions {
        justify-content: center;
    }

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

    .benefit-item {
        padding: 30px 20px;
    }
}
</style>
{% endblock %}