# Default Configuration for Formal Specification Generation System

# System Information
system:
  name: "Formal Spec Generator"
  version: "0.1.0"
  description: "基于大型语言模型的形式化程序规范自动生成验证系统"
  author: "国防科大计算机学院22级软件工程小班刘卓小组"

# LLM Configuration (SiliconFlow DeepSeek V3.1)
llm:
  provider: "siliconflow"
  model: "deepseek-ai/DeepSeek-V3.1"
  base_url: "https://api.siliconflow.cn/v1"
  api_key: "${SILICONFLOW_API_KEY:-sk-xtzjxgjzqtxqjdpvzxxgkxgqkqjgkqjkqgqkqgkqgkqkqj}"
  timeout: 120
  max_retries: 3
  retry_delay: 1.0
  rate_limit_delay: 5.0
  max_concurrent_requests: 3

  # Generation Parameters
  temperature: 0.7
  max_tokens: 4096
  top_p: 0.95

  # Streaming Configuration
  streaming:
    enabled: true
    chunk_timeout: 30

  # Prompt Templates and Context
  prompts:
    system_role: "你是一个专业的形式化方法专家，擅长为C/C++程序生成CBMC兼容的形式化规范。"

    # Template selection based on function characteristics
    template_selection:
      complexity_thresholds:
        low: 20
        medium: 50
        high: 80
      domain_keywords:
        freertos: ["task", "queue", "semaphore", "timer", "freertos", "xTask", "xQueue"]
        network: ["socket", "connect", "send", "recv", "bind", "listen"]
        crypto: ["encrypt", "decrypt", "hash", "aes", "rsa", "sha", "hmac"]
        filesystem: ["file", "open", "read", "write", "close", "fopen", "fwrite"]

    # CBMC Syntax Reference
    cbmc_syntax: |
      CBMC Annotation Syntax:
      - \\requires(condition) - Preconditions
      - \\ensures(condition) - Postconditions
      - \\assigns(location) - Memory modification specification
      - \\valid(ptr) - Pointer validity
      - \\valid_read(ptr) - Readable memory
      - \\valid_write(ptr) - Writable memory
      - \\forall(type var : range; condition) - Universal quantifier
      - \\exists(type var : range; condition) - Existential quantifier
      - \\behavior name: ... \\complete behaviors; \\disjoint behaviors;

    # Quality Assessment
    quality_metrics:
      syntax_completeness: 0.9
      logical_consistency: 0.8
      domain_relevance: 0.85
      verifiability: 0.9

# CBMC Configuration
cbmc:
  path: "cbmc"
  min_version: "5.0"
  default_unwinding: 10
  default_timeout: 300

  # Verification Options
  options:
    pointer_check: true
    overflow_check: true
    bounds_check: true
    assertion_check: true
    div_by_zero_check: true
    undefined_shift_check: true
    signed_overflow_check: true

  # Memory Model
  memory_model: "precise"
  object_bits: 8

  # Output Control
  show_properties: true
  trace: true
  error_trace: true

# Web Server Configuration
web:
  host: "0.0.0.0"
  port: 8080
  debug: true
  threaded: true

  # File Upload
  max_file_size: "10MB"
  allowed_extensions: [".c", ".cpp", ".h", ".hpp"]
  upload_dir: "uploads"

  # Session
  secret_key: "your-secret-key-here"
  session_lifetime: 3600

# Logging Configuration
logging:
  level: "INFO"
  format: "%(asctime)s - %(name)s - %(levelname)s - %(message)s"

  # Component-specific log files
  log_files:
    parser: "logs/parser.log"
    llm_generation: "logs/llm_generation.log"
    cbmc_verification: "logs/cbmc_verification.log"
    error_analysis: "logs/error_analysis.log"
    mutation: "logs/mutation.log"
    system: "logs/system.log"

  # Rotation
  max_size: "10MB"
  backup_count: 5
  encoding: "utf-8"

# Verification Configuration
verification:
  max_concurrent: 3
  cache_enabled: true
  cache_ttl: 3600

  # Mutation Weights (heuristic selection)
  mutation_weights:
    predicate: 0.3      # 谓词变异: \forall ↔ \exists
    boundary: 0.25     # 边界变异: < ↔ <=, > ↔ >=
    logical: 0.2        # 逻辑变异: && ↔ ||, ==> ↔ <==
    array_bounds: 0.15  # 数组边界: 0 .. n-1 ↔ 0 .. n
    pointer_validity: 0.1  # 指针有效性: \valid(ptr) ↔ \valid_read(ptr)

# Quality Assessment
quality:
  # Evaluation Metrics
  metrics:
    accuracy: 0.8        # 准确性目标
    completeness: 0.75   # 完整性目标
    verifiability: 0.9   # 可验证性目标
    stability: 0.85      # 稳定性目标

  # Performance Thresholds
  max_generation_time: 30
  max_verification_time: 300
  max_memory_usage: "512MB"

# Specification Generation Configuration
specification:
  # Storage Settings
  storage:
    base_path: "specifications"
    format: "json"
    enable_versioning: true
    max_versions: 10
    cleanup_interval: 86400  # 24 hours

  # Validation Settings
  validation:
    enabled: true
    quality_thresholds:
      syntax: 0.9
      logic: 0.8
      completeness: 0.7
      overall: 0.75
    strict_mode: false
    auto_refine: true
    max_refinements: 3

  # Generation Modes
  generation:
    default_mode: "single"
    batch_size: 10
    enable_streaming: true
    timeout_per_function: 60

  # Domain-Specific Settings
  domains:
    freertos:
      handle_validation: true
      task_context: true
      interrupt_safety: true
    network:
      timeout_handling: true
      error_recovery: true
    crypto:
      side_channel_protection: true
      key_validation: true
    filesystem:
      resource_management: true
      error_handling: true

# Development Settings
development:
  mode: true
  test_mode: false
  show_debug_info: true
  mock_llm: false

  # Code Quality
  code_style:
    line_length: 88
    docstring_coverage: 0.8

  # Testing
  test_coverage_target: 0.8

# API Configuration
api:
  # API Server Settings
  host: "0.0.0.0"
  port: 8080
  debug: true

  # CORS Configuration
  cors:
    enabled: true
    origins: ["*"]
    methods: ["GET", "POST", "PUT", "DELETE", "OPTIONS"]
    headers: ["Content-Type", "Authorization"]

  # Rate Limiting
  rate_limiting:
    enabled: true
    requests_per_minute: 100
    burst_limit: 10

  # Authentication (to be implemented)
  authentication:
    enabled: false
    method: "session"  # session, jwt, api_key
    session_lifetime: 3600

  # WebSocket Configuration
  websocket:
    enabled: true
    max_connections: 1000
    connection_timeout: 300  # 5 minutes
    message_size_limit: "16MB"
    ping_interval: 25
    ping_timeout: 60

    # Room Configuration
    rooms:
      user_prefix: "user:"
      session_prefix: "session:"
      job_prefix: "job:"
      system_room: "system"

    # Event Handling
    events:
      enable_logging: true
      broadcast_system_events: true

  # Job Manager Configuration
  job_manager:
    storage_dir: "job_storage"
    max_concurrent: 5
    cleanup_interval: 3600  # 1 hour
    max_job_age_days: 7
    enable_persistence: true

    # Job Timeout Settings
    timeouts:
      upload: 300
      parsing: 600
      generation: 1800  # 30 minutes
      mutation: 900
      verification: 1800  # 30 minutes
      workflow: 3600  # 1 hour

  # API Response Settings
  responses:
    enable_debug_info: false
    include_traceback: false
    default_page_size: 20
    max_page_size: 100

  # File Upload Settings
  upload:
    max_file_size: "50MB"
    allowed_extensions: [".c", ".cpp", ".h", ".hpp", ".cc", ".cxx"]
    temp_directory: "temp_uploads"
    enable_virus_scan: false

  # Workflow Configuration
  workflow:
    default_mode: "single_function"  # single_function, batch_processing, iterative_refinement, comprehensive_analysis

    # Mode-specific Settings
    modes:
      single_function:
        max_functions: 1
        enable_mutation: true
        enable_verification: true

      batch_processing:
        max_functions: 50
        batch_size: 10
        concurrent_batches: 3

      iterative_refinement:
        max_iterations: 3
        quality_threshold: 0.8
        enable_auto_refine: true

      comprehensive_analysis:
        enable_full_analysis: true
        generate_report: true
        export_formats: ["json", "html", "pdf"]

    # Global Settings
    settings:
      enable_mutation: true
      enable_verification: true
      max_iterations: 3
      total_timeout: 3600
      step_timeout: 300
      error_tolerance: 3
      quality_threshold: 0.7

    # Output Settings
    output:
      save_intermediate: true
      generate_report: true
      export_formats: ["json", "html"]
      result_directory: "workflow_results"

    # Concurrency Control
    concurrency:
      max_concurrent_jobs: 3
      max_concurrent_operations: 10
      semaphore_timeout: 30