TLA+ Visualiser

A cross-platform desktop application for visualizing TLA+ specifications. Import specs from GitHub URLs, run model checking, and explore state spaces with interactive visualizations.

Features

• GitHub Import: Import TLA+ specifications directly from GitHub URLs

  • File URLs: https://github.com/owner/repo/blob/branch/file.tla
  • Raw URLs: https://raw.githubusercontent.com/owner/repo/branch/file.tla
  • Repository URLs: https://github.com/owner/repo

• Interactive Visualizations:

  • State/transition graph with circular layout
  • Step-by-step trace viewer
  • Invariant/property dashboard

• Model Checking Integration:

  • Run TLC model checker
  • Parse and display results
  • Save/load run results

• Export Capabilities:

  • Export graphs as SVG/PNG
  • Export traces as JSON/Markdown
  • Save model checking runs

Tech Stack

• Language: C++20
• UI Framework: Qt 6 + QML
• Networking: libcurl
• Build System: CMake + Ninja
• Package Manager: Conan
• CI/CD: GitHub Actions with QEMU for multi-arch builds

Prerequisites

All Platforms

• CMake 3.22 or later
• Ninja build system
• Conan package manager
• Qt 6.5 or later
• C++20 compatible compiler

Platform-Specific

Linux:

sudo apt-get install qt6-base-dev qt6-declarative-dev libcurl4-openssl-dev cmake ninja-build
pip install conan

macOS:

brew install qt@6 curl cmake ninja
pip3 install conan

Windows:

• Install Qt 6 from https://www.qt.io/download
• Install CMake and Ninja via Chocolatey or directly
• Install Conan via pip

Building

1. Clone the Repository

git clone https://github.com/johndoe6345789/tla_visualiser.git
cd tla_visualiser

2. Install Dependencies with Conan

conan profile detect
conan install . --output-folder=build --build=missing

3. Configure with CMake

cmake -B build -G Ninja \
  -DCMAKE_BUILD_TYPE=Release \
  -DCMAKE_TOOLCHAIN_FILE=build/conan_toolchain.cmake

4. Build

cmake --build build --config Release

5. Run Tests

cd build
ctest --output-on-failure

6. Run the Application

./build/tla_visualiser

Usage

Importing a Specification

1. Launch the application
2. Click File → Import from GitHub...
3. Enter a GitHub URL:
   • File: https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998.tla
   • Repository: https://github.com/tlaplus/Examples
4. Click Import

Running Model Checker

1. After importing a spec, configure any options
2. Optionally specify a .cfg configuration file
3. Click Run Model Checker
4. View results in the different tabs

Exploring Results

• Graph View: Visual representation of state space
• Trace View: Step-by-step execution traces
• Invariants: Status of invariants and properties

Exporting

• Graph: File → Export Graph... (SVG/PNG)
• Trace: File → Export Trace... (JSON/Markdown)

Project Structure

tla_visualiser/
├── CMakeLists.txt          # Main build configuration
├── conanfile.txt           # Conan dependencies
├── src/                    # C++ source files
│   ├── main.cpp
│   ├── github_importer.cpp
│   ├── tlc_runner.cpp
│   ├── state_graph_model.cpp
│   └── trace_viewer_model.cpp
├── include/                # Header files
│   ├── github_importer.h
│   ├── tlc_runner.h
│   ├── state_graph_model.h
│   └── trace_viewer_model.h
├── qml/                    # QML UI files
│   ├── main.qml
│   ├── ImportView.qml
│   ├── GraphView.qml
│   ├── TraceView.qml
│   └── InvariantView.qml
├── tests/                  # Unit tests
│   ├── CMakeLists.txt
│   ├── test_github_importer.cpp
│   └── test_tlc_runner.cpp
└── .github/workflows/      # CI/CD workflows
    └── build.yml

Architecture

Components

1. GitHubImporter: Handles fetching specs from GitHub

   • URL parsing and validation
   • HTTP requests via libcurl
   • Local caching

2. TLCRunner: Manages TLC model checker execution

   • Process management
   • Output parsing
   • Result serialization

3. StateGraphModel: Qt model for state graph visualization

   • State/transition data
   • Layout calculation
   • QML integration

4. TraceViewerModel: Qt model for trace inspection

   • Step-by-step navigation
   • Variable display
   • Export functions

Design Patterns

• PIMPL: Used for implementation hiding and ABI stability
• Model-View: Qt's model/view architecture for UI
• Observer: Callbacks for async operations

Testing

The project includes unit tests for core components:

cd build
ctest --verbose

Individual tests:

./build/tests/test_github_importer
./build/tests/test_tlc_runner

CI/CD

GitHub Actions workflows automatically:

• Build on Linux (x64, arm64 with QEMU), macOS, and Windows
• Run all tests
• Upload build artifacts

Gated Tree Workflow

The project uses a gated tree workflow pattern to ensure code quality:

1. Lint Job: Fast pre-build checks (formatting, TODOs, CMake syntax)
2. Build Jobs: Platform-specific builds (Linux, macOS, Windows) that depend on lint
3. Gate Job: Final check that all required jobs passed

This ensures that:

• No code can be merged if lint checks fail
• All platforms must build successfully
• All tests must pass
• The gate provides a single "merge-ready" indicator

Workflow Simulation

Test the CI workflow locally before pushing:

# Run full workflow simulation
./simulate_workflow.sh

# Skip tests (faster iteration)
./simulate_workflow.sh --no-tests

# Debug build
./simulate_workflow.sh --debug

# Get help
./simulate_workflow.sh --help

Manual Workflow Triggers

You can manually trigger the workflow from GitHub Actions tab with custom parameters:

• Select specific platforms to build (linux, macos, windows)
• Toggle test execution
• Useful for testing workflow changes

Contributing

1. Fork the repository
2. Create a feature branch
3. Make your changes
4. Run tests
5. Submit a pull request

License

See LICENSE file for details.

Roadmap

Version 1.0 (Current)

• ✅ Basic GitHub import
• ✅ TLC integration stub
• ✅ State graph visualization
• ✅ Trace viewer
• ✅ Cross-platform support

Future Versions

• Enhanced graph layouts (force-directed, hierarchical)
• Real-time TLC output streaming
• Full JSON parsing for GitHub API
• Spec editing capabilities
• Custom themes and styling
• Plugin system

Known Limitations

• TLC must be installed separately and in PATH
• GitHub API calls are not authenticated (rate-limited)
• Large state spaces may impact performance
• Limited TLC output parsing (basic implementation)

Support

For issues, feature requests, or questions:

• GitHub Issues: https://github.com/johndoe6345789/tla_visualiser/issues
• Documentation: See docs/ directory

Acknowledgments

• TLA+ and TLC: Leslie Lamport and Microsoft Research
• Qt Framework: The Qt Company
• libcurl: Daniel Stenberg and contributors