tla_visualiser/docs/ARCHITECTURE.md

Architecture Overview

This document describes the architecture and design of TLA+ Visualiser.

High-Level Architecture

┌─────────────────────────────────────────────────────────┐
│                     QML UI Layer                        │
│  (ImportView, GraphView, TraceView, InvariantView)      │
└────────────────────┬────────────────────────────────────┘
                     │ Qt Signals/Slots
┌────────────────────▼────────────────────────────────────┐
│                Qt Models (QAbstractListModel)           │
│      StateGraphModel      TraceViewerModel              │
└──────────┬──────────────────────┬───────────────────────┘
           │                      │
┌──────────▼──────────┐  ┌────────▼─────────────────────┐
│  GitHubImporter     │  │      TLCRunner               │
│  - URL parsing      │  │  - Process management        │
│  - HTTP requests    │  │  - Output parsing            │
│  - Local caching    │  │  - Result serialization      │
└─────────────────────┘  └──────────────────────────────┘

Component Details

1. UI Layer (QML)

Purpose: Provides the user interface using Qt Quick/QML.

Components:

• main.qml: Application window, menu bar, tab navigation
• ImportView.qml: GitHub URL input and spec preview
• GraphView.qml: State/transition graph visualization
• TraceView.qml: Step-by-step trace inspection
• InvariantView.qml: Invariant status dashboard

Communication: Uses Qt's property binding and signal/slot mechanism to interact with C++ models.

2. Model Layer (Qt Models)

StateGraphModel

Responsibility: Provides data for state graph visualization.

Key Methods:

• loadFromResults(): Populate from TLC results
• getTransitions(): Return transition edges
• getStateDetails(): Get details for specific state

Data:

• States with positions (x, y coordinates)
• Transitions (edges between states)
• Layout calculated using circular algorithm

TraceViewerModel

Responsibility: Provides data for trace/counterexample viewing.

Key Methods:

• loadTrace(): Load a counterexample trace
• exportToJson(): Export trace as JSON
• exportToMarkdown(): Export trace as Markdown

Data:

• Sequence of trace steps
• Current step index
• Variable values at each step

3. Business Logic Layer

GitHubImporter

Responsibility: Fetch TLA+ specs from GitHub.

Features:

• URL Parsing: Regex-based parsing of GitHub URLs

  • File URLs: github.com/owner/repo/blob/branch/path
  • Raw URLs: raw.githubusercontent.com/owner/repo/branch/path
  • Repo URLs: github.com/owner/repo

• HTTP Communication: Uses libcurl for HTTP requests

  • Follows redirects
  • Sets User-Agent header
  • Error handling

• Local Caching: Saves fetched content to temp directory

  • Cache key: owner_repo_branch_filepath
  • Automatic cache lookup before fetching

Design Pattern: PIMPL (Pointer to Implementation)

• Public interface in header
• Private implementation in .cpp
• Hides libcurl details from API users

TLCRunner

Responsibility: Execute TLC model checker and parse results.

Features:

• Process Management: Runs TLC as external Java process

  • Async execution in separate thread
  • Cancellation support
  • Status callbacks

• Output Parsing: Parses TLC text output

  • State count extraction
  • Error message collection
  • Timing information

• Result Persistence: Save/load results

  • Text-based format (upgradable to JSON)
  • Deterministic runs

States:

• NotStarted
• Running
• Completed
• Failed
• Cancelled

Design Pattern: PIMPL + Observer (callbacks)

Data Flow

Import Flow

User enters URL
    ↓
ImportView captures input
    ↓
GitHubImporter.parseUrl()
    ↓
GitHubImporter.fetchFile()
    ├─→ Check cache
    └─→ HTTP request (libcurl)
    ↓
Content displayed in ImportView

Model Check Flow

User clicks "Run Model Checker"
    ↓
TLCRunner.startModelCheck()
    ↓
Spawn Java process (TLC)
    ↓
Parse output in background thread
    ↓
Update status via callback
    ↓
TLCRunner.getResults()
    ↓
StateGraphModel.loadFromResults()
TraceViewerModel.loadTrace()
    ↓
UI updates via Qt property bindings

Visualization Flow

User switches to Graph View
    ↓
StateGraphModel provides data
    ├─→ Node positions (calculated)
    ├─→ Edge list
    └─→ State details
    ↓
QML Canvas or GraphicsView renders
    ↓
User clicks node
    ↓
Model provides details for selected node

Design Patterns

PIMPL (Pointer to Implementation)

Used in: GitHubImporter, TLCRunner, StateGraphModel, TraceViewerModel

Benefits:

• Binary compatibility (ABI stability)
• Faster compilation (hidden dependencies)
• Implementation flexibility

Structure:

class MyClass {
public:
    MyClass();
    ~MyClass();
    void publicMethod();
private:
    class Impl;
    std::unique_ptr<Impl> pImpl;
};

Observer Pattern

Used in: TLCRunner callbacks

Benefits:

• Async notification
• Decoupling

Usage:

runner.setStatusCallback([](Status s) {
    // Handle status change
});

Model-View (Qt)

Used throughout for UI

Benefits:

• Separation of concerns
• Automatic updates
• Testable models

Factory Pattern (Future)

Could be used for:

• Different graph layout algorithms
• Export format handlers

Threading Model

Main Thread

• Qt event loop
• UI updates
• User interaction
• Model data access

Background Threads

• TLC execution (via std::thread)
• HTTP requests (via libcurl)

Synchronization: Qt signals/slots (thread-safe when queued)

Memory Management

• Smart Pointers: std::unique_ptr for PIMPL idiom
• Qt Parent-Child: QObjects use Qt's parent-child ownership
• RAII: Resources cleaned up in destructors
• No Manual new/delete: Prefer stack allocation or smart pointers

Error Handling

Current Strategy

• Return values (bool for success/failure)
• Empty returns for errors (empty string, empty vector)
• Error messages stored in result structures

Future Improvements

• Exception-based error handling
• Error codes enumeration
• Detailed error context

Dependencies

External Libraries

• Qt 6: UI framework, models, networking
• libcurl: HTTP requests
• C++ Standard Library: Containers, threading, filesystem

Dependency Management

• Conan: Package manager for libcurl
• CMake: Build system integration
• Find Modules: Qt6 via CMake's built-in finder

Extensibility Points

Adding New Visualizations

1. Create new QML view (e.g., TimelineView.qml)
2. Create corresponding Qt model (e.g., TimelineModel)
3. Add tab in main.qml
4. Load data from TLCRunner::RunResults

Adding New Import Sources

1. Create new importer class (e.g., GitLabImporter)
2. Implement common interface
3. Add UI option to select source
4. Integrate in ImportView

Adding New Export Formats

1. Add export method to model (e.g., exportToXML())
2. Add UI button/menu item
3. Implement serialization logic

Testing Strategy

Unit Tests

• GitHubImporter: URL parsing, cache operations
• TLCRunner: Status management, result saving
• Models: Data loading, transformations

Integration Tests (Future)

• End-to-end import flow
• TLC execution with sample specs
• Export functionality

UI Tests (Future)

• QML test framework
• Automated UI interaction

Performance Considerations

Current Optimizations

• Circular layout O(n) complexity
• Local caching to avoid redundant downloads
• Async TLC execution

Future Optimizations

• Lazy loading for large graphs
• Level-of-detail rendering
• Progressive result display
• Worker threads for layout calculation

Security Considerations

Current Measures

• No credential storage
• Read-only spec access
• Local cache in temp directory

Future Improvements

• GitHub token authentication (optional)
• HTTPS certificate validation
• Input sanitization for TLC invocation
• Sandboxed TLC execution

Build System

CMake Configuration

• Minimum version: 3.22
• C++20 standard requirement
• Qt6 modules: Core, Gui, Quick, Widgets
• Conan integration via toolchain file

Platform Support

• Linux: Native builds, ARM64 via QEMU
• macOS: Native builds (x86_64, arm64)
• Windows: MSVC and MinGW support

CI/CD

• GitHub Actions workflows
• Multi-platform builds
• Automated testing
• Artifact uploads

Future Architecture Improvements

1. Plugin System: Allow third-party visualizations
2. Async I/O: libuv or Boost.Asio for better performance
3. Database: SQLite for result persistence
4. Language Server: TLA+ LSP integration
5. Web Backend: Optional web UI via REST API