Skip to content

TESTING.md

Latest commit

 

History

History
456 lines (345 loc) · 11 KB

TESTING.md

File metadata and controls

456 lines (345 loc) · 11 KB

Testing Guide

This document describes how to run tests for the Hybrid Verification Framework and what they verify.

Table of Contents

  1. Running Tests
  2. Test Structure
  3. Test Coverage
  4. Writing New Tests
  5. Continuous Integration

Running Tests

Prerequisites

  • Python 3.7 or higher
  • All framework dependencies installed
  • Protocol configurations available (at minimum, examples/raft/config/raft.yaml)

Running All Tests

# From project root
python -m pytest tests/

# Or using unittest
python tests/test_framework_integration.py

# With verbose output
python tests/test_framework_integration.py -v

Running Specific Test Classes

# Test template loader only
python -m pytest tests/test_framework_integration.py::TestTemplateLoader -v

# Test code generation only
python -m pytest tests/test_framework_integration.py::TestCodeGeneration -v

# Test counterexample conversion only
python -m pytest tests/test_framework_integration.py::TestCounterexampleConversion -v

Running Individual Tests

# Test specific method
python -m pytest tests/test_framework_integration.py::TestTemplateLoader::test_load_protocol_config -v

Test Structure

Test Organization

Tests are organized in tests/test_framework_integration.py with the following test classes:

  1. TestTemplateLoader - Template and configuration loading
  2. TestCodeGeneration - Code generation tools
  3. TestCounterexampleConversion - Counterexample conversion
  4. TestPropertyAnalysis - Property analysis and synthesis
  5. TestProtocolAwareness - Protocol-specific functionality
  6. TestFrameworkScripts - Framework script integration
  7. TestDomainAgnosticFeatures - Generic/domain-agnostic features
  8. TestEndToEnd - End-to-end workflow tests

Test Data

Test data is stored in tests/test_data/:

  • Sample counterexamples
  • Test configuration files
  • Expected outputs

Test Coverage

Template Loader Tests

TestTemplateLoader verifies:

  • ✅ Listing available domain templates
  • ✅ Listing available property templates
  • ✅ Listing available protocol configurations
  • ✅ Loading domain templates
  • ✅ Loading property templates
  • ✅ Loading protocol configurations
  • ✅ Expanding property templates with variables

Example:

def test_load_protocol_config(self):
    """Test loading a protocol configuration"""
    config = self.loader.load_protocol_config('raft')
    self.assertIsInstance(config, dict)
    self.assertIn('protocol', config)
    self.assertIn('properties', config)
    self.assertEqual(config['protocol']['name'], 'Raft')

Code Generation Tests

TestCodeGeneration verifies:

  • ✅ Property generation (JSON, KLEE C, TLA+)
  • ✅ TLA+ specification generation
  • ✅ KLEE test harness generation
  • ✅ Generated files contain expected content

Example:

def test_generate_properties(self):
    """Test property generation"""
    generator = PropertyGenerator()
    result = generator.generate_properties('raft')
    self.assertIn('json', result)
    self.assertIn('klee', result)
    self.assertIn('tla', result)
    self.assertTrue(Path(result['json']).exists())

Counterexample Conversion Tests

TestCounterexampleConversion verifies:

  • ✅ KLEE to TLA+ conversion (generic mode)
  • ✅ TLA+ to KLEE conversion (generic mode)
  • ✅ Protocol-specific conversion
  • ✅ Conversion with protocol configuration

Example:

def test_convert_klee_to_tla_generic(self):
    """Test KLEE to TLA+ conversion in generic mode"""
    klee_cex = {
        'counterexample_id': 'test_001',
        'property': 'SafetyProperty',
        'assertion': 'klee_assert(condition)',
        'symbolic_values': {'num_rounds': 5}
    }
    result = convert_klee_to_tla(klee_cex)
    self.assertEqual(result['source'], 'KLEE')
    self.assertIn('tla_code', result)

Property Analysis Tests

TestPropertyAnalysis verifies:

  • ✅ Generic counterexample analysis
  • ✅ Protocol-specific analysis
  • ✅ Violation pattern identification
  • ✅ Property synthesis

Example:

def test_analyze_counterexample_generic(self):
    """Test counterexample analysis in generic mode"""
    cex_file = self.test_data_dir / 'test_cex.json'
    # ... create test file ...
    result = analyze_counterexample(str(cex_file))
    self.assertGreater(result['total_count'], 0)
    self.assertIn('analyses', result)

Protocol Awareness Tests

TestProtocolAwareness verifies:

  • ✅ Protocol configuration loading with all fields
  • ✅ Protocol-specific counterexample conversion
  • ✅ Protocol metadata validation

Example:

def test_protocol_config_loading(self):
    """Test loading protocol configuration with all required fields"""
    config = self.loader.load_protocol_config('raft')
    self.assertIn('protocol', config)
    self.assertEqual(config['protocol']['name'], 'Raft')
    self.assertIn('properties', config)
    self.assertIn('state_variables', config)

Framework Scripts Tests

TestFrameworkScripts verifies:

  • ✅ Counterexample converter accepts --protocol parameter
  • ✅ Analyze counterexample accepts protocol parameter
  • ✅ Script integration with protocol configuration

Example:

def test_counterexample_converter_protocol_param(self):
    """Test counterexample converter accepts --protocol parameter"""
    result = convert_counterexamples(
        klee_json_file=str(klee_file),
        output_dir=str(output_dir),
        protocol_name='raft'
    )
    self.assertEqual(result['protocol'], 'raft')

Domain-Agnostic Features Tests

TestDomainAgnosticFeatures verifies:

  • ✅ Generic violation pattern matching
  • ✅ Generic counterexample conversion (no protocol)
  • ✅ Pattern-based property identification

Example:

def test_generic_violation_patterns(self):
    """Test generic violation pattern matching"""
    cex = {
        'assertion': 'klee_assert(entities <= 1)',
        'message': 'Uniqueness property violated',
        'property': 'UniquenessViolation'
    }
    violation = identify_property_violation(cex)
    self.assertEqual(violation['violation_type'], 'Safety')
    self.assertEqual(violation['pattern'], 'multiple_entities_same_context')

End-to-End Tests

TestEndToEnd verifies:

  • ✅ Full workflow for Raft protocol
  • ✅ Hybrid verification workflow
  • ✅ Integration of all components

Example:

def test_full_workflow_raft(self):
    """Test full workflow for Raft protocol"""
    # 1. Load protocol configuration
    loader = TemplateLoader()
    config = loader.load_protocol_config('raft')
    
    # 2. Generate properties
    prop_gen = PropertyGenerator()
    prop_result = prop_gen.generate_properties('raft')
    
    # 3. Generate TLA+ spec
    tla_gen = TLASpecGenerator()
    tla_file = tla_gen.generate_spec('raft')
    
    # 4. Generate KLEE harness
    klee_gen = KLEETestGenerator()
    klee_file = klee_gen.generate_harness('raft')

Writing New Tests

Test File Structure

#!/usr/bin/env python3
import unittest
from pathlib import Path
import sys

sys.path.insert(0, str(Path(__file__).parent.parent))

class TestMyFeature(unittest.TestCase):
    """Test my feature"""
    
    def setUp(self):
        """Set up test fixtures"""
        self.test_data_dir = Path(__file__).parent / "test_data"
        self.test_data_dir.mkdir(exist_ok=True)
    
    def tearDown(self):
        """Clean up after tests"""
        # Clean up if needed
        pass
    
    def test_my_feature(self):
        """Test my feature functionality"""
        # Arrange
        # Act
        # Assert
        pass

Best Practices

  1. Use descriptive test names:

    def test_load_protocol_config_with_all_fields(self):
    """Test loading protocol configuration with all required fields"""

  2. Test both success and failure cases:

    def test_load_nonexistent_protocol(self):
    """Test loading non-existent protocol raises error"""
    with self.assertRaises(FileNotFoundError):
        self.loader.load_protocol_config('nonexistent')

  3. Clean up test data:

    def tearDown(self):
    import shutil
    if self.test_output_dir.exists():
        shutil.rmtree(self.test_output_dir)

  4. Use test data directory:

    def setUp(self):
    self.test_data_dir = Path(__file__).parent / "test_data"
    self.test_data_dir.mkdir(exist_ok=True)

  5. Test protocol-agnostic and protocol-specific:

    def test_generic_conversion(self):
    """Test generic conversion without protocol"""
    result = convert_klee_to_tla(klee_cex)
    # ...

def test_protocol_specific_conversion(self):
    """Test conversion with protocol configuration"""
    config = self.loader.load_protocol_config('raft')
    result = convert_klee_to_tla(klee_cex, config)
    # ...

Adding Test Data

Create test data files in tests/test_data/:

# Create test counterexample
cex_file = self.test_data_dir / 'test_cex.json'
with open(cex_file, 'w') as f:
    json.dump({
        'counterexamples': [{
            'counterexample_id': 'test_001',
            'property': 'SafetyProperty',
            'assertion': 'klee_assert(condition)'
        }]
    }, f)

Continuous Integration

GitHub Actions Example

Create .github/workflows/test.yml:

name: Tests

on: [push, pull_request]

jobs:
  test:
    runs-on: ubuntu-latest
    
    steps:
    - uses: actions/checkout@v2
    
    - name: Set up Python
      uses: actions/setup-python@v2
      with:
        python-version: '3.9'
    
    - name: Install dependencies
      run: |
        pip install -r requirements.txt
    
    - name: Run tests
      run: |
        python tests/test_framework_integration.py -v

Test Coverage

To measure test coverage:

# Install coverage tool
pip install coverage

# Run tests with coverage
coverage run -m pytest tests/

# Generate coverage report
coverage report

# Generate HTML report
coverage html

Troubleshooting

Common Test Failures

  1. FileNotFoundError:

    • Ensure test data files exist
    • Check file paths are correct

  2. ImportError:

    • Ensure sys.path includes project root
    • Check module names are correct

  3. AssertionError:

    • Check expected vs actual values
    • Verify test data is correct

  4. Protocol not found:

    • Ensure examples/raft/config/raft.yaml exists
    • Check protocol name spelling

Debugging Tests

# Add debug output
def test_my_feature(self):
    result = my_function()
    print(f"Result: {result}")  # Debug output
    self.assertIsNotNone(result)
# Run with verbose output
python -m pytest tests/ -v -s

# Run with debugger
python -m pdb tests/test_framework_integration.py

See Also